scientific article; zbMATH DE number 1341619

MaRDI QIDQ4263168zbMATH OpenFDO

Authors Peter Baumgartner, Norbert Eisinger, Ulrich Furbach

Publication date 13 June 2000

zbMATH Keywords

backtrack-free control regimesconnection calculuseffective search strategyproof confluenceproof procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1748570
• scientific article; zbMATH DE number 1950264
• A Non-clausal Connection Calculus
• Restricting backtracking in connection calculi

Cited in

(17)

• Consolution as a framework for comparing calculi
• Depth-first proof search without backtracking for free-variable clausal tableaux
• Machine learning guidance for connection tableaux
• Set of support, demodulation, paramodulation: a historical perspective
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• scientific article; zbMATH DE number 1612557 (Why is no real title available?)
• A Non-clausal Connection Calculus
• Restricting backtracking in connection calculi
• Connection Tableaux with Lazy Paramodulation
• scientific article; zbMATH DE number 64168 (Why is no real title available?)
• scientific article; zbMATH DE number 1950264 (Why is no real title available?)
• scientific article; zbMATH DE number 1748570 (Why is no real title available?)
• The disconnection method
• Multiplicativity of Connes’ calculus
• Computer Aided Verification
• The disconnection tableau calculus

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