Proof search strategies in linear logic
Tanel Tammet · 1993
Linear logic is a refinement of classical logic introducedby J.-Y.Girard to provide means for keeping track of re-sources - two assumptions of a formula A are distin-guished from a single assumption of A. Although linearlogic is not the first attempt for developing resource-oriented logics (relevance logic and Lambek calculusbeing well-known examples), it is by now the most-investigated one. Since its introduction linear logic hasenjoyed increasing attention both from proof theoristsand computer scientists.The multiplicative fragment of linear logic is claimedto be a system of communication without problems ofsynchronization. In addition to possible applications toparallelism, linear logic can be seen as a formalism forsharing analysis (with another teminology, also the prob-lem of storage reuse, in-place update, etc) and strictnessanalysis, two important research areas in functional pro-gramming community.In this paper (for details see the full version: [Tam-met 93]) we will concentrate on problems of automatedtheorem proving in full propositional first-order linearlogic. We will investigate general search strategies andways for modifying standard deduction rules in linearlogic to make it more suitable for automated proof search,both for top-down and bottom-up directions. Thepresented modifications are motivated by experimentsperformed with our theorem prover. We will describethe implementations and performed experiments for bothsearch directions.