Automated generation of analytic calculi for involutive logics

Abstract

During the last decades there have been an increasing demand for non-classical logics. Unlike classical logic, they are often capable of reasoning in situations with inconsistent or vague information. Of particular interest in computer science are substructural logics, which are axiomatic extensions of full Lambek Calculus FL. Their name is due to the fact that when expressed as sequent calculi, they lack some of the structural rules (exchange, weakening and contraction). The family of substructural logics encompasses a wide set of nonclassical logics such as intuitionistic, linear, fuzzy, intermediate logics, and more. A common way of defining a nonclassical logic is by adding Hilbert axioms to well known systems. The applicability of a logic depends heavily on the existence of a corresponding analytic calculus, i.e. a deductive system where the proof search is performed by stepwise decomposition of the formulas to be proved. Analytic calculi are suitable for being implemented in computational proof search algorithms and for establishing mathematical properties of a logic such as consistency or decidability. Typically, an analytic calculus for a logic is obtained in two steps: i) finding the calculus that represent the features of the logic and showing that it is sound and complete, ii) showing that the calculus is analytic by providing a proof of the cut elimination theorem. These steps often require a laborious investigation, and therefore computer support tools for introducing analytic calculi are very desirable. In this thesis we implement a tool called InvAxiomCalc, which offers automatic generation of analytic calculi for a wide range of axiomatic extensions of Multiplicative Additive Linear Logic (MALL), i.e. a fragment of classical linear logic without exponentials. InvAxiomCalc accepts an axiom in the language of MALL and generates, if possible, a paper written in LaTeX with the analytic calculus of MALL extended with the input axiom.