A confluent connection calculus

DOI10.1007/3-540-48660-7_30MaRDI QIDQ4263168zbMATH OpenFDO

Authors Peter Baumgartner, Norbert Eisinger, Ulrich Furbach

Publication date 13 June 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48660-7_30

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: A confluent connection calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263168)