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

DOI10.1016/S0747-7171(03)00026-9zbMath1019.03006MaRDI QIDQ1404980

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)

Related Items

The model evolution calculus as a first-order DPLL method, The disconnection tableau calculus, Towards a unified model of search in theorem-proving: subgoal-reduction strategies

Uses Software

• SETHEO
• HARP

Cites Work

• Ordered tableaux: Extensions and applications
• The disconnection method
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item