scientific article; zbMATH DE number 1552524

MaRDI QIDQ4524784zbMATH OpenFDO

Authors Peter Baumgartner, Ulrich Furbach

Publication date 29 July 2001

zbMATH Keywords

proof theoryautomated theorem provingtableau calculusconnection tableauxrestart model elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Hyper tableaux
• scientific article; zbMATH DE number 1748583
• scientific article; zbMATH DE number 1841823
• scientific article; zbMATH DE number 1088202
• Proof and model generation with disconnection tableaux

Cited in

(10)

• Semantically-guided goal-sensitive reasoning: model representation
• scientific article; zbMATH DE number 1841823 (Why is no real title available?)
• scientific article; zbMATH DE number 834568 (Why is no real title available?)
• Hyper tableaux
• scientific article; zbMATH DE number 1552523 (Why is no real title available?)
• Model elimination and connection tableau procedures
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Set of support, demodulation, paramodulation: a historical perspective
• scientific article; zbMATH DE number 1748583 (Why is no real title available?)
• Introducing general redundancy criteria for clausal tableaux, and proposing resolution tableaux

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 Q4524784)