A new proof search method for linear logic
In Lect. Notes Pure Appl. Math. 180, 97-124 (1996; Zbl 0868.03025), \textit{J.-Y. Girard} introduced a new syntax for proof-nets of multiplicative and additive Linear Logic (MALL): boxes for the additives are removed, and a correctness criterion (in the Danos-Regnier style) making use of ``boolean weights is given. The notion of superimposition (of formulas, links, subproof-nets) is very complex, not well understood, and tighly linked to the additive connective \(\&\): this makes the theory of MALL proof-nets very difficult. However, provability in MALL is decidable (in fact PSPACE-complete), as proven by \textit{P. Lincoln, J. Mitchell, A. Scedrov} and \textit{N. Shankar} [Ann. Pure Appl. Logic 56, No. 1-3, 239-311 (1992; Zbl 0768.03003)]. This paper proposes a nice variant of Girard's correctness criterion for cut-free proof-nets, which yields a proof search method for MALL. The author first gives an algorithm to build a (cut-free) proof-structure (in the sense of Girard) from a given sequent. He then introduces his variant of the correctness criterion for cut-free proof-nets, and shows it can be checked in polynomial time (in the size of the proof-structure). The main novelty in the criterion is the notion of ``inductive empire of a formula, in terms of which the now standard acyclicity and connectedness condition can be expressed. For the entire collection see [Zbl 0892.00029].
- Linear strategy for Boolean ring based theorem proving
- The additive multiboxes
- Softness of MALL proof-structures and a correctness criterion with Mix
- New uses of linear arithmetic in automated theorem proving by induction
- An even closer integration of linear arithmetic into inductive theorem proving
- Proof discovery in LK system by analogy
- A new correctness criterion for MLL proof nets
- Resource management in linear logic proof search revisited
- Proof nets for unit-free multiplicative-additive linear logic
- A linear algorithm for MLL proof net correctness and sequentialization
This page was built for publication: A new proof search method for linear logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4217606)
