Semantically guided first-order theorem proving using hyper-linking

DOI10.1007/3-540-58156-1_14zbMath1433.68540OpenAlexW1764789126MaRDI QIDQ5210771

Heng Chu, David Alan Plaisted

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Related Items

History and Prospects for First-Order Automated Deduction, On the practical value of different definitional translations to normal form, Semantically guided first-order theorem proving using hyper-linking

Uses Software

• OTTER
• SATCHMO

Cites Work

• Eliminating dublication with the hyper-linking strategy
• Challenge problems in elementary calculus
• A structure-preserving clause form translation
• Hierarchical deduction
• Seventy-five problems for testing automatic theorem provers
• Non-Horn clause logic programming without contrapositives
• A semantic backward chaining proof system
• A method for simultaneous search for refutations and models by equational constraint solving
• A Proof Method for Quantification Theory: Its Justification and Realization
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• Semantically guided first-order theorem proving using hyper-linking
• A Computing Procedure for Quantification Theory
• Conditional term rewriting and first-order theorem proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item