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 (3)

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Semantically guided first-order theorem proving using hyper-linking