Tools for the investigation of sustructural, intermediate and paraconsistent logics

Abstract

Non-classical logics have gained importance in many fields of computer science, engineering and philosophy. They are often employed in applications of artificial intelligence, knowledge representation and formal verification; e.g., when it comes to reasoning in presence of vague information or inconsistencies. There are already many non-classical logics and, due to the increasing demand for such logics, new ones are introduced frequently. Non-classical logics are often introduced or described by adding Hilbert axioms to well-known systems. The usefulness of these logics however strongly depends on the availability of analytic calculi for them. Analytic calculi are deductive systems in which proof search proceeds by a step-wise decomposition of the formulas to be proved. Such calculi play a paramount role for computational proof search and are also key to establishing essential properties for the formalized logics, like consistency or decidability. Unfortunately, introducing an analytic calculus for a particular logic often requires significant efort: a suitable framework for the calculus has to be chosen and adequate inference rules reecting the characteristic properties of the considered logic have to be provided. Finally, soundness, completeness and analyticity of the defined calculus must be proved. Since these steps are usually tailored to the specific logic at hand and often difficult to establish, many important logics still lack an analytic calculus. Systematic and algorithmic procedures to generate analytic calculi are therefore highly desirable. This thesis presents (theoretical and engineering) tools for the investigation of substructural, intermediate and paraconsistent propositional logics. The main contributions are: (c1) systematic procedures for the automated generation of analytic calculi, (c2) a further exploitation of the analytic calculi to establish important properties for the formalized logics, and (c3) the introduction of the framework TINC (Tools for the Investigation of Non-Classical logics) to provide computer support for the contributions (c1) and (c2). More precisely, for substructural logics we use the analytic hypersequent calculi generated by the procedure in [2] to check whether the corresponding logics are standard complete, i.e. they have a semantics with truth values in [0; 1] (c2).