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

Diderik Batens, Dagmar Provijn

Abstract


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:

PDF

Refbacks

  • There are currently no refbacks.