A Knuth-Bendix-like ordering for orienting combinator equations

DOI10.1007/978-3-030-51074-9_15MaRDI QIDQ2096451zbMATH OpenOpenAlexFDO

Authors Ahmed Bhayat, Giles Reger

Publication date 9 November 2022

Full work available at URL https://doi.org/10.1007/978-3-030-51074-9_15

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Enumerating orientations of ordered sets
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion
• Combinatorial polar orderings and recursively orderable arrangements
• A Combinatorial Approach to Complexity Theory via Ordinal Hierarchies
• scientific article; zbMATH DE number 1047721
• scientific article; zbMATH DE number 1555978
• An upper bound on the derivational complexity of Knuth-Bendix orderings.
• Automating the Knuth Bendix ordering
• The recursive structure of some ordering problems
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties

Cites work

• A combinator-based superposition calculus for higher-order logic
• A Higher-Order Iterative Path Ordering
• A Lambda-Free Higher-Order Recursive Path Order
• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• Extensional paramodulation for higher-order logic and its effective implementation Leo-III
• Hammer for Coq: automation for dependent type theory
• scientific article; zbMATH DE number 5318491 (Why is no real title available?)
• scientific article; zbMATH DE number 67454 (Why is no real title available?)
• LEO-II and Satallax on the Sledgehammer test bench
• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Paramodulation-based theorem proving
• Perpetual reductions in -calculus
• Polymorphic higher-order recursive path orderings
• Satallax: An Automatic Higher-Order Prover
• Substitution tree indexing
• Superposition with lambdas
• Term indexing
• The Computability Path Ordering: The End of a Quest
• The higher-order prover \textsc{Leo}-II
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Translating higher-order clauses to first-order clauses

Cited in

(3)

• A combinator-based superposition calculus for higher-order logic
• Set of support, demodulation, paramodulation: a historical perspective
• The 10th IJCAR automated theorem proving system competition -- CASC-J10

Describes a project that uses

Uses Software

• Satallax
• Sledgehammer
• GitHub

This page was built for publication: A Knuth-Bendix-like ordering for orienting combinator equations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096451)