The procedure in outline:

START Are any gaps open? NO YES END Pick one; note its proxi- mate argument; and note all rules that apply Do any rules apply? NO YES Mark gap as a dead end; and confirm a counter- example Pick one (prefer- ring a rule that closes gaps) and apply it

Rules for closing gaps:

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

Rules for developing gaps:

kind of sentence rule for resources
(i.e., exploitation rule)		 rule for goals
(i.e., planning rule)

conjunction

 Ext Cnj
negation ⎰
⎱		 of atomic sent. none ⎱
⎰		 RAA
of non-atomic sent. CR (when the goal is ⊥)

atomic sentence

 none IP

⊤ or ⊥

 none none