Pushing the search paths in the proofs. A study in proof heuristics

Diderik Batens, Dagmar Provijn


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 Gamma |- A.

Full Text:



  • There are currently no refbacks.