TY - JOUR T1 - Pushing the Search Paths in the Proofs. A Study in Proof Heuristics JF - Logique et Analyse Y1 - 2001 A1 - Batens, Diderik A1 - Provijn, Dagmar AB -

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 vdash B and a positive test for Gamma vdash A.

VL - 44 SP - 113–134 ER -