scientific article; zbMATH DE number 1113998

MaRDI QIDQ4375764zbMATH OpenFDO

Authors Geoffrey D. Alexander, David A. Plaisted

Publication date 13 July 1998

zbMATH Keywords

search space complexitytheorem-proving strategies

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Recommendations

• The search efficiency of theorem proving strategies
• scientific article; zbMATH DE number 1037485
• Eliminating dublication with the hyper-linking strategy

Cited in

(11)

• Efficient SAT-based proof search in intuitionistic propositional logic
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• scientific article; zbMATH DE number 1037485 (Why is no real title available?)
• First-order Answer Set Programming as Constructive Proof Search
• The 481 ways to split a clause and deal with propositional variables
• scientific article; zbMATH DE number 1414298 (Why is no real title available?)
• The search efficiency of theorem proving strategies
• Automated Reasoning with Analytic Tableaux and Related Methods
• Improved Propositional Extension Rule
• Refinements to depth-first iterative-deepening search in automatic theorem proving

Describes a project that uses

Uses Software

• TPTP

This page was built for publication:

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