Chapter 4 Proof Search

Linear logic as introduced by Girard and presented in the previous chapter is a rich system for the formalization of reasoning involving state. It conservatively extends intuitionistic logic and can therefore also serve as the logical basis for general constructive mathematics. Searching for proofs in such an expressive logic is difficult, and one should not expect silver bullets. Depending on the problem, proof search in linear logic can have a variety of applications. In the domain of planning problems (see Section 2.4) searching for a proof means searching for a plan. In the domain of concurrent computation (see Petri nets in Section 3.2 or the π-calculus in Section 3.6) searching for a proof means searching for possible computations. In the domain of logic programming (which we investigate in detail in Chapter??), searching for a proof according to a fixed strategy is the basic paradigm of computation. In the domain of functional programming and type theory (which we investigate in Chapter??), searching for a proof means searching for a program satisfying a given specification. Each application imposes different requirements on proof search, but there are underlying basic techniques which recur frequently. In this chapter we take a look at some basic techniques, to be exploited in subsequent chapters. 4.1 Bottom-Up Proof Search and Inversion The literature is not in agreement on the terminology, but we refer to the process of creating a derivation from the desired judgment on upward as bottom-up proof search. A snap-shot of a bottom-up search is a partial derivation, with undecided judgments at the top. Our goal is to derive all remaining judgments, thereby completing a proof. We proceed by selecting a judgment which remains to be derived and an inference rule with which it might be inferred. We also may need to determine exactly how the conclusion of the rule matches the judgment. For example, in the ⊗R rule we need to decide how to split the linear hypotheses betwee