Focused Inverse Method for Linear Logic

摘要

Linear logic presents a unified framework for describing and reasoning about stateful systems. Because of its view of hypotheses as resources, it supports such phenomena as concurrency, external and internal choice, and state transitions that are common in such domains as protocol verification, concurrent computation, process calculi and games. It accomplishes this unifying view by providing logical connectives whose behavior is closely tied to the precise collection of resources. The interaction of the rules for multiplicative, additive and exponential connectives gives rise to a wide and expressive array of behaviors. This expressivity comes with a price: even simple fragments of the logic are highly complex or undecidable. Various approaches have been taken to produce automated reasoning systems for fragments of linear logic. This thesis addresses the need for automated reasoning for the complete set of connectives for first-order intuitionistic linear logic (circle multiply, 1,-o, &, Top, circle plus, 0, (exclamation point), Universal quantifier, Existential quantifier), which removes the need for any idiomatic constructions in smaller fragments and instead allows direct logical expression. The particular theorem proving technique used is a novel combination of a variant of Maslov's inverse method using Andreoli's focused derivations in the sequent calculus as the underlying framework. The goal of this thesis is to establish the focused inverse method as the premier means of automated reasoning in linear logic. To this end, the technical claims are substantiated with an implementation of a competitive first-order theorem prover for linear logic as of this writing, the only one of its kind.