Conditional term rewriting and first-order theorem proving

DOI10.1007/3-540-56393-8_19OpenAlexW1540452401MaRDI QIDQ5881190

Shie-Jue Lee, Geoffrey D. Alexander, Heng Chu, David Alan Plaisted

Publication date: 9 March 2023

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

Full work available at URL: https://doi.org/10.1007/3-540-56393-8_19

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Semantically guided first-order theorem proving using hyper-linking

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Hierarchical deduction
• Non-Horn clause logic programming without contrapositives
• A simplified problem reduction format
• Non-resolution theorem proving
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• A Computing Procedure for Quantification Theory