Partial redundancy in saturation

DOI10.1007/978-3-031-99984-0_28MaRDI QIDQ6869929zbMATH 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_28

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

• A comprehensive framework for saturation theorem proving
• A modular formalization of superposition in Isabelle/HOL
• Basic paramodulation
• Consider only general superpositions in completion procedures
• Critical pair criteria for completion
• 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 1688812 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 1754649 (Why is no real title available?)
• scientific article; zbMATH DE number 1759379 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• On restrictions of ordered paramodulation with simplification
• On using ground joinable equations in equational theorem proving
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Paramodulation-based theorem proving
• Proving termination with multiset orderings
• Redundancy criteria for constrained completion
• Regularization in Spider-style strategy discovery and schedule construction
• Resolution theorem proving
• Simple LPO constraint solving methods
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Stepping stones in the TPTP world
• Superposition for full higher-order logic
• Superposition with Delayed Unification
• Term Rewriting and All That
• Theorem proving with ordering and equality constrained clauses
• Things to know when implementing KBO
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Unnecessary inferences in associative-commutative completion procedures
• Using forcing to prove completeness of resolution and paramodulation

This page was built for publication: Partial redundancy in saturation

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