SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Proof Search in First-order Linear Logic and other Cut-free Sequent Calculi
 by Dr. Patrick Lincoln & Dr. Natarajan Shankar.

We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Her brand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for first order MALL is in NEXPTIME, and first-order MLL is in NP. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy