A Knuth-Bendix-like ordering for orienting combinator equations

DOI10.1007/978-3-030-51074-9_15OpenAlexW3039231562MaRDI QIDQ2096451

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)

Related Items (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

Uses Software

• Satallax
• Sledgehammer
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Perpetual reductions in \(\lambda\)-calculus
• Hammer for Coq: automation for dependent type theory
• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• LEO-II and Satallax on the Sledgehammer test bench
• A combinator-based superposition calculus for higher-order logic
• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• Translating higher-order clauses to first-order clauses
• Satallax: An Automatic Higher-Order Prover
• A Lambda-Free Higher-Order Recursive Path Order
• The Computability Path Ordering: The End of a Quest
• Polymorphic higher-order recursive path orderings
• Substitution tree indexing
• A Higher-Order Iterative Path Ordering
• Superposition with lambdas

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