3.5.3. A procedure

The common features of the thinking used at each stage in the development of this derivation can be captured in a procedure that can be applied repeatedly to guide the development of any derivation. Restarting the procedure introduces a new stage in the derivation, and the procedure will be restarted one final time after the last stage in order to confirm that the derivation has reached its end.

1. Choose an open gap. Find all the open gaps of the derivation. If there are none, the derivation is closed and you are done. If there is more than one, pick one to work on (it does not matter which).
2. Identify its proximate argument. Find the goal and the active resources of the gap you are working on; and, for each of these, identify the kind of sentence it is—that is, decide whether it is ⊤, ⊥, a conjunction, a negation, or an atomic sentence.
3. Check for closure. Check whether the gap can be closed using one of the rules in the following table:

   Rules for closing gaps

   rule	conditions for applying it
   QED	the goal is among the resources
   Nc	the goal is ⊥, and there are sentences φ and ¬ φ among the resources
   ENV	the goal is ⊤
   EFQ	⊥ is a resource

   If the conditions for applying one of these rules are met, apply the rule, and start again at step 1.
4. Choose a sentence to work on. Find which, if any, of the goal and active resources has a rule that may be applied at this stage. That is, for each of these sentences check whether a basic rule (outlined in the table below) applies to a resource or goal of that sort and check whether any additional requirements are met.

   Exploitation and planning rules

   kind of sentence			rule for this sentence as a resource	as a goal
   conjunction			Ext	Cnj
   negated	⎧ ⎨ ⎩	non-atomic sent.	CR (when the goal is ⊥)	RAA
   		atomic sentence	none
   atomic sentence			none	IP
   ⊤ or ⊥			none	none

   If there is no sentence to which a rule can be applied, you have reached a dead-end open gap; mark it as such and you are done. If there is more than one sentence to which a rule may be applied, pick one to work on (it does not matter which).
5. Apply a rule. Apply the rule you have identified to the sentence you have found, and start again at step 1.

The choice of a gap or sentence to work on does not matter in the sense that whether a gap eventually closes or reaches a dead end does not depend on the way such a choice is made. Of course, such a choice can make a difference for the length of the derivation; but the difference will often amount to only one stage or a line or two.

This procedure describes a way of applying the rules; and, even though it allows some choice, it is more restrictive than the rules alone. For example, it forces you to close a gap you are working on if that is possible even if the rules would also allow you to develop the gap further. In that case, it simply enforces good sense, but it is also restrictive in one way that can length a derivation: no allowance is made for the option of exploiting a resource in more than one gap at once (i.e., in the same stage of development). Consequently, you should regard this procedure as merely a rough guide that may be supplemented by shortcuts when you see that they are possible. Such shortcuts include the use of available but inactive resources with rules like QED and the use of non-basic rules like Adj and LFR.