Depth-first proof search without backtracking for free-variable clausal tableaux

DOI10.1016/S0747-7171(03)00026-9MaRDI QIDQ1404980zbMATH OpenFDO

Authors Bernhard Beckert

Publication date 25 August 2003

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

free-variable calculidepth-first proof searchdeterministic proof procedurefairness strategyfree-variable clausal tableaux

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1552522
• Clausal intuitionistic logic II. tableau proof procedures
• A Bottom-Up Approach to Clausal Tableaux
• Logics in Artificial Intelligence
• scientific article; zbMATH DE number 1765699

Cites work

• scientific article; zbMATH DE number 1341619 (Why is no real title available?)
• scientific article; zbMATH DE number 1552522 (Why is no real title available?)
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• Ordered tableaux: extensions and applications
• The disconnection method

Cited in

(6)

• A Bottom-Up Approach to Clausal Tableaux
• Refinements to depth-first iterative-deepening search in automatic theorem proving
• The disconnection tableau calculus
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• The model evolution calculus as a first-order DPLL method
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies

Describes a project that uses

Uses Software

• HARP
• SETHEO

This page was built for publication: Depth-first proof search without backtracking for free-variable clausal tableaux

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