Proof by consistency in conditional equational theories

DOI10.1007/3-540-54317-1_91OpenAlexW1911974211MaRDI QIDQ5881278

Eddy Bevers, Johan Lewi

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_91

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, A general framework to build contextual cover set induction provers, Induction using term orderings, On the connection between narrowing and proof by consistency, On notions of inductive validity for first-order equational clauses, Induction = I-axiomatization + first-order consistency.

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Conditional rewrite rules
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• A strong restriction of the inductive completion procedure
• Semantic confluence tests and completion methods