Term ordering diagrams

DOI10.1007/978-3-031-99984-0_29MaRDI QIDQ6869928zbMATH OpenFDO

Authors Márton Hajdu, Laura Kovács, Andrei Voronkov

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_29

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• Deciding the confluence of ordered term rewrite systems
• Faster, higher, stronger: E 2.3
• Ground joinability and connectedness in the superposition calculus
• scientific article; zbMATH DE number 1754649 (Why is no real title available?)
• scientific article; zbMATH DE number 1759379 (Why is no real title available?)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Making higher-order superposition work
• Orienting rewrite rules with the Knuth-Bendix order.
• Paramodulation-based theorem proving
• Practical algorithms for deciding path ordering constraint satisfaction.
• Simple LPO constraint solving methods
• Stepping stones in the TPTP world
• Subsumption demodulation in first-order theorem proving
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Things to know when implementing KBO

This page was built for publication: Term ordering diagrams

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