Systematic proof theory for non-classical logics : advances and implementation

Abstract

Nichtklassische Logiken nahmen in den letzten Jahren in vielen Gebieten, vor allem in der Informatik, der Künstlichen Intelligenz oder der Wissensrepräsentation, an Bedeutung zu. Mittlerweile existiert bereits eine große Anzahl nützlicher und interessanter nichtklassischer Logiken, wie beispielsweise die Familie der intermediären Logiken, Fuzzy-Logiken oder Substrukturelle Logiken. Zudem führen Wissenschaftler verschiedener Fachbereiche weiterhin neue Logiken ein, um ihre Anforderungen zu erfüllen.<br />Nichtklassische Logiken definiert man üblicherweise, indem man Hilbert-Axiome zu bereits bekannten Systemen hinzufügt. Die Nützlichkeit dieser Logiken hängt jedoch stark von der Verfügbarkeit sogenannter analytischer Kalküle ab, in welchen Beweise durch schrittweises Zerlegen der Formeln geführt werden. Den analytischen Kalkül einer Logik definiert man durch die Wahl eines passenden Formalismus, sowie das Festlegen geeigneter Regeln zur Formalisierung der Logik. Zusätzlich müssen Korrektheit, Vollständigkeit und Schnittelimination des definierten Kalküls bewiesen werden. Mit der Definition neuer Logiken wächst daher auch die Anzahl solcher Beweise und eine automatisierte Prozedur zur Einführung analytischer Kalküle in systematischer Weise wäre somit erstrebenswert.<br />In dieser Diplomarbeit erweiterten wir eine systematische Prozedur, die Hilbert-Axiome in äquivalente analytische Kalküle umformt, auf die Familie der Axiome (Bdk) mit k >=1. Diese Axiome sind insbesondere interessant, da die Erweiterung intuitionistischer Logik mit dem Axiom (Bd2) die einzige interpolierbare, intermediäre Logik ist, auf die man die Prozedur nicht anwenden kann. Um die Prozedur auf diese Axiome auszuweiten, definierten wir zunächst einen neuen Formalismus, den Nichtkommutativen Hypersequenzkalkül, und erstellten geeignete Regeln entsprechend den Axiomen (Bdk). Für diese Regeln bewiesen wir Korrektheit, Vollständigkeit und Schnittelimination. Zusätzlich entwickelten wir einen Algorithmus auf Basis der systematischen Prozedur und implementierten diesen in PROLOG.<br />

Non-classical logics are logics different from classical, boolean logic. They encompass, amongst others, the family of intermediate, fuzzy, and substructural logics. During the past few years, these logics have gained importance, especially in many fields of computer science, artificial intelligence, and knowledge representation.<br />By now, there are many useful and interesting non-classical logics and practitioners in various fields keep on introducing new logics to fulfill their needs.<br />Non-classical logics are usually defined by adding Hilbert axioms to known systems. The usefulness of these logics, however, heavily depends on the availability of analytic calculi for them, i.e., of calculi where the derivations proceed by step-wise decomposition of the formulas that should be proved. An analytic calculus for a logic is usually defined by first choosing a suitable formalism and then providing the right rules for formalizing the logic. Furthermore, soundness, completeness and cut-elimination for the defined calculus have to be proved. This leads to the introduction of a large number of such proofs and papers which increases with the definition of new logics. An automated procedure to introduce analytic calculi in a systematic way would therefore be very desirable.<br />In this thesis we extended the scope of a new systematic procedure, which translates Hilbert axioms into equivalent analytic calculi, to capture the family of axioms known as (Bdk) with k >=1. These axioms are especially interesting as intuitionistic logic extended with (Bd2) is the only interpolable intermediate logic to which the procedure does not apply to. To adapt the procedure to these axioms, we introduced a new formalism, called Non-Commutative Hypersequent Calculus, and identified suitable rules corresponding to (Bdk). For these rules we provided uniform proofs of soundness, completeness and cut-elimination. In addition to this theoretical investigation, the systematic procedure has been translated into an algorithm which was implemented in PROLOG.<br />