Handout for derivations workshop on §3.5 (to PDF format)
The procedure in outline:
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 |