scientific article; zbMATH DE number 1552523

zbMath0966.03013MaRDI QIDQ4524783

Reinhold Letz

Publication date: 3 July 2001

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

zbMATH Keywords

classical logicautomated deductionstructural restrictionscontrol structureconnection tableauxproof search methodsclausal tableauxsearch pruninggeneralization of unificationinter-tableaux pruning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items (6)

Semantically-guided goal-sensitive reasoning: model representation ⋮ The disconnection tableau calculus ⋮ Liberalized variable splitting ⋮ Craig interpolation with clausal first-order tableaux ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Set of support, demodulation, paramodulation: a historical perspective

This page was built for publication: