3.5.1. Approaching derivations

If we set aside the rules LFR and Adj, the general advice for starting and continuing derivations is to do anything the rules permit you to do. That is, any rule that can be applied to a goal or active resource of any gap is a legitimate way of proceeding. Some choices may lead to longer derivations than others; but the safety of the rules insures that you can never go off in the wrong direction, and their progressiveness insures that you will always move some distance toward the end.

The rules other than LFR and Adj are shown in the following tables. The one on the left shows the exploitation rules for resources and the planning rules for goals. The simplest way of approaching derivations is to apply these rules as often as possible using the rules from the right-hand table to close gaps whenvever possible.

Rules for developing gaps
for resources for goals
conjunction
φ ∧ ψ 		Ext Cnj
negation
¬ φ 		CR
(if φ is not atomic
and the goal is ⊥) 		RAA
atomic
sentence 		IP
Rules for closing gaps
when to close rule
the goal is also
a resource 		QED
sentences φ and ¬φ are
resources & the goal is ⊥ 		Nc
⊤ is the goal ENV
⊥ is a resource EFQ

The further rules LFR and Adj can be used to simplify derivations in some cases but they are never needed; and, when a gap will not close, they may simply delay the inevitable dead end. For this reason, the rules in the tables above are labeled basic rules and are counted as part of the basic system of derivations.

Glen Helman 03 Aug 2010