3.5.1. Approaching derivations

The general rule 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 differences in length that result from different choices of rules are likely to be greatest in valid arguments. When arguments are not valid, you may well have to apply all possible rules. The differences between derivations will then result only from the order in which the rules are applied (though such differences can make for significant differences in length).

The basic rules we have accumulated 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 rules LFR and Adj are not shown. They 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 are labeled basic rules and are counted as part of the basic system of derivations.

Glen Helman 23 Sep 2005