A Knuth-Bendix-like ordering for orienting combinator equations
From MaRDI portal
Publication:2096451
DOI10.1007/978-3-030-51074-9_15OpenAlexW3039231562MaRDI QIDQ2096451
Publication date: 9 November 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_15
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
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