scientific article; zbMATH DE number 1341619

zbMath0937.03016MaRDI QIDQ4263168

Peter Baumgartner, Norbert Eisinger, Ulrich Furbach

Publication date: 13 June 2000

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

proof proceduresconnection calculusbacktrack-free control regimeseffective search strategyproof confluence

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

The disconnection tableau calculus, Depth-first proof search without backtracking for free-variable clausal tableaux, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\), Set of support, demodulation, paramodulation: a historical perspective