Principles of entailment can be applied in concert by using the graphical idea of a tree—and in more than one way. Tree-form proofs provide a natural notation for applying the valid patterns of argument Cnj and Ext. Alternatively, we can consider principles of entailment that state conditions for the validity of arguments that have conjunctions as conclusions or as premises. These, too, can be combined in a tree as a sequent proof to show an argument is valid. A sequent proof can also be thought of as a tree whose growth traces the conditions that must hold for the argument at its root to be valid.

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. Derivations also have a tree structure displayed in a system of vertical scope lines which indicate the resources and goals relevant to various parts of the derivation.

The laws of entailment appear as rules for exploiting resources, planning for goals, and closing gaps. There are rules for each of the patterns of argument that figure in tree-form proofs. The key rules for conjunction are Extraction (Ext) and Conjunction (Cnj). Quod Erat Demonstrandum (QED) is used to close a gap when its goal is among its resources, and the symbol ● (a filled circle) marks a closed gap.

When a derivation is developed, numbers are used along with the labels for rules to record both the order of the development and the connection between the premises and conclusions of the rules.

The branching structure of tree-form proofs is replicated in derivations by the system of cross-references provided by stage numbers. And the branching structure of sequent proofs lies in the way gaps develop, something indicated by the order of stage numbers and the arrangement of scope lines. This structure, together with the proximate argument of each gap (formed from its active resources and its goal), forms an argument tree.

Principles of entailment for other logical forms will be associated with further rules. Those for ⊤ and ⊥ are the rules Ex Nihilo Verum (ENV) and Ex Falso Quodlibet (EFQ), which figure in derivations as rules for closing gaps.

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.