%0 Journal Article %J Logique et Analyse %D 2001 %T Pushing the Search Paths in the Proofs. A Study in Proof Heuristics %A Batens, Diderik %A Provijn, Dagmar %X
Introducing techniques deriving from dynamic proofs in proofs for propositional classical logic is shown to lead to a proof format that enables one to push search paths into the proofs themselves. The resulting goal directed proof format is shown to provide a decision method for A1, ..., An B and a positive test for A.
%B Logique et Analyse %V 44 %P 113–134 %G eng