Goal-Driven Reasoning in First-Order Logic
Claes Strannegård · 2006
A complete, subformula-preserving proof system for goal-driven reasoning in first-order logic is pre-sented. The proof system is a transition system and its proofs are (linear and local) computations in the transistion system. Thus the proof system fits into a standard framework for modeling problem-solving in cognitive psychology.