Title: Automated generation of analytic calculi for involutive logics
Other Titles: Automatische Generierung analytischer Kalküle für involutative Logiken
Language: English
Authors: Ymeri, Ardit 
Qualification level: Diploma
Keywords: proof theory; analytic calculi; involutive logics; Prolog; tools
Advisor: Ciabattoni, Agata 
Issue Date: 2019
Number of Pages: 86
Qualification level: Diploma
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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-133953
Library ID: AC15562567
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Apr 5, 2021


checked on Apr 5, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.