These principles, too, can be combined in a tree as to show an argument is valid. Such a tree—an argument tree—traces the conditions that must hold for the argument at its root to be valid, but it can also be seen as a guide for finding conclusion trees.

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 conclusion trees. 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 conclusion trees is replicated in derivations by the system of cross-references provided by stage numbers. And the branching structure of argument trees 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.