Semantically guided first-order theorem proving using hyper-linking

DOI10.1007/3-540-58156-1_14MaRDI QIDQ5210771zbMATH OpenOpenAlexFDO

Authors Heng Chu, David A. 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)

Recommendations

• Ordered semantic hyper-linking
• Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
• Parallelization of a hyper-linking-based theorem prover
• Eliminating dublication with the hyper-linking strategy
• scientific article; zbMATH DE number 4072438

Cites work

• A Computing Procedure for Quantification Theory
• A method for simultaneous search for refutations and models by equational constraint solving
• A Proof Method for Quantification Theory: Its Justification and Realization
• A semantic backward chaining proof system
• A structure-preserving clause form translation
• Challenge problems in elementary calculus
• Conditional term rewriting and first-order theorem proving
• Eliminating dublication with the hyper-linking strategy
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• Hierarchical deduction
• scientific article; zbMATH DE number 3904002 (Why is no real title available?)
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 695096 (Why is no real title available?)
• scientific article; zbMATH DE number 3332500 (Why is no real title available?)
• Non-Horn clause logic programming without contrapositives
• Otter 2.0
• Semantically guided first-order theorem proving using hyper-linking
• Seventy-five problems for testing automatic theorem provers

Cited in

(9)

• Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
• Ordered semantic hyper-linking
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• History and prospects for first-order automated deduction
• scientific article; zbMATH DE number 1954191 (Why is no real title available?)
• On the practical value of different definitional translations to normal form
• Semantically guided first-order theorem proving using hyper-linking
• Semantic Guidance for Saturation Provers
• Automated Reasoning with Analytic Tableaux and Related Methods

Describes a project that uses

Uses Software

• OTTER
• SATCHMO

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210771)