The simplest way of combining principles of entailment uses two graphical ideas, an analysis tree, which reflects the way arguments following the pattern conjunction can be combined to conclude a complex conjunction from its ultimate components, and an exploitation chain, which reflects the way arguments following the pattern extraction can be combined to move from a conjunction to its components. The adequacy of this approach to entailment concerning conjunction can be shown by considering principles of entailment stating conditions for the validity of arguments that have conjunctions as conclusions or as premises. Tree-form proofs can be elaborated to make the link between exploitation chains and analysis trees explicit by using an argument whose conclusion is its premise, a pattern which we will label by the Latin phrase quod erat demonstrandum. And patterns of argument, also with Latin names, can be added to capture the properties of ⊤ (ex nihilo verum) and ⊥ (ex falso quodlibet).
In fact, we will use a different, more compact notation for combining principles of entailment—a kind of natural deduction system that we will refer as a system of derivations. This notation presents the project of showing that an entailment holds as the task of closing a gap between its conclusion, which serves as a goal, and its premises, which serve as resources. As we narrow the initial gap (and others that result from it), we develop the derivation. The branching structure of tree-form proofs is represented in part by a system of vertical scope lines and in part by numerical annotations.
The laws of entailment appear as rules for exploiting resources, planning for goals, and closing gaps. There are rules corresponding to each of the patterns of argument that figure in tree-form proofs: Extraction (Ext), Conjunction (Cnj), Quod Erat Demonstrandum (QED), Ex Nihilo Verum (ENV), and Ex Falso Quodlibet (EFQ). The abbreviations shown here are used along with numerical annotations to record the history of the development of a derivation, and the symbol ● (a black circle) marks a closed gap.
We keep track of changes in the information contained in goals and resources by using the scope lines of a derivation to tell in which gaps given resources are available and in which gaps available resources are still active.