Completion of first-order clauses with equality by strict superposition

DOI10.1007/3-540-54317-1_89OpenAlexW1539329516MaRDI QIDQ5881276

Harald Ganzinger, Leo Bachmair

Publication date: 9 March 2023

Published in: Conditional and Typed Rewriting Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-54317-1_89

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Inductive theorem proving by consistency for first-order clauses ⋮ Reduction techniques for first-order reasoning ⋮ On fairness of completion-based theorem proving strategies ⋮ On narrowing, refutation proofs and constraints ⋮ Order-sorted completion: The many-sorted way ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Abstract canonical presentations ⋮ A completion procedure for conditional equations ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis

Cites Work

• Completion-time optimization of rewrite-time goal solving
• The Concept of Demodulation in Theorem Proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item