scientific article; zbMATH DE number 1341619

MaRDI QIDQ4263168zbMATH OpenFDO

Authors Peter Baumgartner, Norbert Eisinger, Ulrich Furbach

Publication date 13 June 2000

zbMATH Keywords

proof proceduresconnection calculusbacktrack-free control regimeseffective search strategyproof confluence

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

(16)

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

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)