scientific article; zbMATH DE number 1341619

zbMATH Open0937.03016MaRDI QIDQ4263168FDOQ4263168

Authors: Peter Baumgartner, Norbert Eisinger, Ulrich Furbach 

Publication date: 13 June 2000

Title of this publication is not available (Why is that?)

Recommendations

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

zbMATH Keywords

proof proceduresconnection calculusbacktrack-free control regimeseffective search strategyproof confluence

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (15)

• Set of support, demodulation, paramodulation: a historical perspective
• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• The disconnection method
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Multiplicativity of Connes’ calculus
• Connection Tableaux with Lazy Paramodulation
• Title not available (Why is that?)
• The disconnection tableau calculus
• 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)