Computational Logic
projects

Cut-elimination is one of the most important techniques in proof theory. Roughly speaking, eliminating cuts from a proof generates a new proof without lemmas, which essentially consists of the syntactic material of the proven theorem. Since its introduction in 1934, sequent calculus has been one of the preferred deductive frameworks to formalize and reason about logics. However, this framework is not capable of handling all interesting and useful logics. To this end, a large range of variants and extensions of Gentzen sequent calculi have been introduced in the last few decades. Among them, hypersequent calculi have been shown shown to be a rather elegant and simple framework for ``logic engineering'' that applies to a wide range of nonclassical logics arising in several areas of mathematics, philosophy and computer science.

The aim of the proposed project is a semantic characterization of cut-elimination in sequent and hypersequent calculi, i.e. he definition of syntactic and semantic criteria that, when satisfied by such calculi guarantee a certain kind of cut-elimination and, when not satisfied, provides counterexamples. The central idea is to answer the following questions: Which are the natural properties that rules have to satisfy in order to preserve cut-elimination? Is there a uniform method to prove (or disprove) cut-elimination for a wide class of sequent or hypersequent calculi?

The main advantages of such a method would be:

1. it becomes easier to prove cut-elimination theorems for novel (sequent type) logic calculi and to find analytic calculi for new logics

2. the construction of the cut-elimination methods and the checking of the formal criteria can be automatized - provided the method is effective.

In mathematical logic people study logical systems capturing various parts of formal reasoning. The main subject of this project is comprised by two kinds of nonclassical logic, namely constructive logic and probability logic.

Constructive logic dates back to the beginnings of the twentieth century and tries to capture various forms of constructive mathematical reasoning. Right from the beginning people have tried to link this syntactical approach to constructivism with computational mathematics, for example by giving computational interpretations of the rules and axioms of constructive logic. This, however, turned out to be a difficult enterprise, and in fact all of the ideas to complete it initially failed, until Skvortsova proved in 1988 that the ideas of Kolmogorov and Medvedev could be successfully applied to obtain the desired computational semantics. The structure of Medvedev degrees that she used has many other applications in mathematical logic, and we plan to study the connections of this structure with constructive logic further. In particular we hope to better understand the relation with the theory of Pi-0-1 classes that has recently seen great progress in computability theory.

Probability logic is a much newer and less canonical kind of logic, that nevertheless poses many fundamental questions about the logical and computational nature of probability. In this project we focus on one specific kind of probability logic that is based on Valiants famous pac-model, a model of induction that has become the dominant paradigm in complexity theory and related areas. Here we seek to develop the basic theory of this logic, and in particular to determine the computational complexity of several of the decision problems related to it. In order to do this it will be crucial to develop at the same time its model theory and proof theory, which is immediately related to several intricacies from probability and measure theory.

Project leader: Matthias Baaz.

Skolem functions can be traced back to the famous paper by Thoralf Skolem 1920. Model theoretically they allow for the representation of abstract existential assumptions in axioms by concrete functions. Therefore, any mathematical theory has an open conservative extension. Proof theoretically Skolem functions can be used to eliminate strong quantifiers and thereby to reduce Herbrand's theorem for arbitrary quantifier prefixes to its purely existential variant. It is of course always possible to replace strong quantifiers by Skolem functions depending on the scope of weak quantifiers (or by any other function term), the problem is how to obtain the original formula from the Skolemized version in a correct way (reSkolemization).

In this project we intend to develop and classify algorithms for reSkolemization in the settings of classical and intuitionistic logic. We intend to analyze mathematical proofs (especially the Schütte-van der Waerden solution to the Kissing Number Problem for dimension three) with respect to trigonometric functions which we believe to represent Skolem functions in many relevant cases.

The main result of the proposed project will lie in a deeper understanding of the proof theoretic impact of the presence of functions in mathematical proofs. This might have applications to all areas where Skolem functions are prominent, especially to automated theorem proving whose most important variants as resolution calculus rely on open i.e. Skolemized formalisms.

Unfortunately there is not just one logic as basis for every useful application. In addition, typical application scenarios hardly allow to single out in advance a particular logic as the most adequate basis for formal reasoning. We are therefore rather urged to investigate broad families of logics, and -- if possible -- define uniform calculi that facilitate the switch from one logic to another and deepen the understanding of the relations between them.Therefore, a central task of logic in computer science is to provide the automated generation of analytic calculi for a wide range of non-classical logics, i.e., calculi in which the proof search proceeds by step-wise decomposition of the formula to be proved. The most famous example of such calculi are Gentzen's ones. Cut-free ``Gentzen-style'' calculi can serve as a basis for automated deduction and allow the extraction of important implicit information from proofs such as numerical bounds and programs in proof-style. Moreover, they are one key of a profound understanding of the relation between the logic's syntax and semantics.

The aim of this project is to provide tools for the automated generation of analytic calculi (with hypersequent and sequent of relations) for broad classes of logics. In outline, we intend to describe 1) meta-theorem provers which allow for an automated adaption of existing theorem provers to the logics under considerations 2) modular cut-elimination procedures which are based on general transfer principles extending cut-elimination from subclasses of calculi to all cases 3) tools for proof mining, i.e., the automated extraction of implicit information in proofs such as bounds, programs, variant of Herbrand's disjunctions.

This Lise Meitner project is a research project in mathematical logic, computability, and learning theory. A major objective of the project is to study various models of learning and inference, using methods from logic and computability theory. A second goal is to study logics connected to these models.

Other research themes figuring in this project are the study of randomness and Kolmogorov complexity, and various issues concerning constructive logic (such as intuitionistic logic) and computation.

Project leader: Matthias Baaz.

Gödel logics have been introduced by Gödel to approximate intuitionistic logic by linearly ordered finite-valued logics. Gödel logics naturally arise in a number of different areas within logic, mathematics and computer science. In particular, they are related to temporal logics, fuzzy logic and fuzzy mathematics.

In this project we will investigate the syntax and semantics of Gödel logics with propositional quantifiers. The most important goals of this investigation are, in short:

• A complete characterization of quantified propositional Gödel logics in various aspects. In particular we are interested in their expressive power and classification according to topological properties of the set of truth-values.
• The development of extensions of first-order Gödel logics (especially the one based on the real interval [0,1]) in order to include propositional quantifiers. This will allow a general construction of equivalent prenex normal forms for arbitrary formulas.
• Suitable interpretations of derivations in various formalizations of first-order Gödel logics as concurrent computations using a suitable form of Herbrand's theorem for prenex formulas.

Project leader: Matthias Baaz.

There are many tools in Symbolic Computation supporting scientists and technicians, but only few deal with the automated analysis of given proofs or documented decisions. There will be a demand for such tools in the near future for the following reasons:

• Mathematical proofs are the foundation of practical mathematical knowledge. Structures and theories are developed in accordance with the establishment of reasonable proofs. Long term progress in automated theorem proving for mathematics will be possible only if uptodate proofs become analyzable automatically and consequently proof styles - the results of these analyses - are incorporated into automated theorem provers.
• The increase of mathematical knowledge will make it necessary for more and more mathematicians to work in a hybrid way in the near future, i.e. to establish proof plans who's details are completed by the computer. The interaction between mathematician and computer however depends on the ability of the system to analyze and comprehend proof segments provided by the mathematician.
• Furthermore, the analysis of proofs leads itself to new mathematical results, e.g. the extraction of numerical bounds and algorithms as well as the generalization of proofs, for example showing the independence of given proofs from certain assumptions. The automatization of this investigation will help the working mathematician to enrich his results by additional useful informations at low costs.

The arguments above will hold a forteriori when proof analysis is extended to educational purposes or to a wider range of sciences up to legal decisions which are formally documented. Here the analysis of proof gaps as part of proof verification will become prominent. Many other applications could be mentioned which are due to the nearly unbounded increase of documented data concerning formalized decisions, which can be considered as proofs in their own right.

Project leader: Matthias Baaz.

The main topic of this project has been the analysis of first-order Gödel logics, especially with respect to their axiomatizability.

Project leader: Matthias Baaz.

This project dealt with the introduction and elimination of cuts. Cuts are the logical equivalent of lemmata in mathematical proofs. Eliminating cuts can provide additional information like algorithms or upper bounds for proofs of existence for mathematical proofs. On the other hand, the introduction of cuts is of essential use in structuring mathematical proofs and thus for generating an adaequate representation.

Headed by M. Baaz and M. Parigot.

Headed by M. Baaz and F. Esteva.

Headed by M. Baaz and F. Esteva.

Headed by M. Baaz and M. Parigot.

Headed by M. Baaz and A. Avron.

Due to the pioneering work of Zadeh, it is widely recognised that fuzzy logic is fundamental to an adequate treatment of topics such as formalising common natural language predicates like '"tall" or "dark", and reasoning in the presence of uncertainty and/or vagueness. Despite numerous successful applications in these areas however, there is still a great need for foundational research in fuzzy logic, in particular to develop formal methods for automated reasoning. The aim of the proposed project is to develop and exploit proof theory for some of the most important formalisations of fuzzy logic, which include Lukasiewicz logics and related logics. Proof theory is concerned with the analysis of proofs from a syntactical perspective, and is a basic prerequisite for developing automated reasoning methods for logic. Its main goal is the construction of proof calculi that are "analytic" in the sense that proofs proceed by a stepwise decomposition of the formula to be proved, and "uniform" across a wide range of logics. The project is a continuation of the PhD work of the applicant which solved a long-term open problem in the field by providing analytic proof systems for propositional Lukasiewicz logic L and Product logic P. The objectives are: (1) to provide analytic proof calculi for finite-valued Lukasiewicz logics, and (since these logics are not axiomatisable) fragments of first-order L and P, and (2) to exploit these proof calculi to obtain metalogical results and proof procedures suitable for automated reasoning.

The aim of the project was the study of the provability predicate of constructive theories, in particular of Heyting Arithmetic, the constructive counterpart of Peano Arithmetic. It has resulted in the description of the provability fragment of a logic which is conjectured to be the preservativity (a constructive analogue to interpretability) logic of Heyting Arithmetic; a syntactic algorithm for the admissible rules of intuitionistic logic, which play an important role in provability logic; an axiomatization of the admissible rules of various intermediate logics; a Skolemization method for intuitionistic logic with an existence predicate; and the characterization of the basic logic of proofs of Heyting Arithmetic.

The provably recursive functions of a theory are connected to its proof-theoretic ordinal via hierarchies of sub-recursive functions. One far reaching goal is to adopt this to bounded arithmetic using dynamic ordinals. So far dynamic ordinals are connected only to induction principles which already yields separation results. We will proceed on two paths. On the one side we will try to obtain a complete picture of the correspondence of relativized bounded arithmetic to dynamic ordinals by characterizing additional relativized bounded arithmetic theories by their dynamic ordinals. Stronger (above T¹₂(α) ) and weaker (below S¹₂(α) ) theories will be considered. Furthermore, we will extend the language of bounded arithmetic by functions with stronger but sub-exponential growth rates. To this end our cut-elimination methods and boundedness theorems will be adapted and connected to new fast cut-elimination and proof complexity techniques. On the other side the relation between provably recursive functions and dynamic ordinals will be employed to gain new approaches to the polynomial hierarchy. We have already defined dynamic ordinals by developing exponential codes. As a next step we will investigate feasible hierarchies based on dynamic ordinals which may serve to characterize the provably recursive functions of bounded arithmetic.

Proof theory is concerned with the analysis of proofs from a syntactical point of view, and is a basic prerequisite for developing automated reasoning methods for a logic. Its main goal is the construction of proof calculi that are "analytic" in the sense that proofs proceed by a stepwise decomposition of the formula to be proved.

Fuzzy logic is the base for reasoning with uncertainty. The most important formal representations of fuzzy logic are infinite valued Lukasiewicz, Gödel and Product logic. Any T-norm, that is the main tool to combine uncertain information, can be defined as a suitable combination of these three logics.

The aim of this project was to define analytic calculi for fuzzy logic.

© 2004 DMG-FG2 Group, Arnold Beckmann, Norbert Preining