|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||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.
|Library ID:||AC15562567||Organisation:||E185 - Institut für Computersprachen||Publication Type:||Thesis
|Appears in Collections:||Thesis|
Show full item record
Files in this item:
|Ymeri Ardit - 2019 - Automated generation of analytic calculi for involutive...pdf||727.02 kB||Adobe PDF|
checked on Apr 5, 2021
checked on Apr 5, 2021
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.