The search efficiency of theorem proving strategies

DOI10.1007/3-540-58156-1_5zbMath1433.68561OpenAlexW1520527482MaRDI QIDQ5210762

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_5

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Non-Horn clause logic programming, Contradiction separation based dynamic multi-clause synergized automated deduction, Partition-based logical reasoning for first-order and propositional theories, Situational Calculus, linear connection proofs and STRIPS-like planning: An experimental comparison, The design of the CADE-13 ATP system competition, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Set of support, demodulation, paramodulation: a historical perspective, Evaluating general purpose automated theorem proving systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• Depth-first iterative-deepening: An optimal admissible tree search
• The intractability of resolution
• Non-Horn clause logic programming without contrapositives
• A simplified problem reduction format
• On a bound for the complexity of terms in the resolution method
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• Proving refutational completeness of theorem-proving strategies
• Using resolution for deciding solvable classes and building finite models
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Automatic Theorem Proving With Renamable and Semantic Resolution
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Computing Procedure for Quantification Theory