Proposal to investigate structural properties of formal proofs by graph theoretic methods.

Graph theory has sufficiently demonstrated to be an adequate framework for applications whenever the structural relations between individual objects are considered (such as gas or electricity distribution networks, sociograms and communication structures, molecular structures in chemistry, road maps in transport logistics). The scope of this proposed project is the study of graphs that model the interaction of the individual parts of a formal proof. Recent development in computer technique has given the concept of formal proofs new significance since the theoretical concept embraces automated deductions from data bases; by a better understanding of the structural aspects, the efficiency of automated deductions can be increased and waiting periods can be shortened. Single graph theoretic concepts have been applied to proofs and their structures frequently, though a combination with features of the logical calculi under consideration impedes an application of more complex methods from graph theory. We have developed a new abstract graph model (PROOF GRAPHS) by which the structure of proofs stemming from a wide range of individual proof systems can be modelled. The new model supports a natural and direct formulation of logical concepts in graph theoretical terms. The planned research consists of three main phases. In the first phase we will consider important proof techniques known from literature and study the corresponding PROOF GRAPHS. The second phase focuses on graph theoretical methods in the context of PROOF GRAPHS (especially, graph homomorphisms and the vertex splitting procedure). The final phase is dedicated to an analysis of well studied classes of graphs (such as planar graphs, n- regular graphs, Eulerian graphs, critical graphs, etc.) in view of results of the preceding two phases. We plan to support our theoretical purposes with computer experiments based on the Library of Efficient Data types and Algorithms (LEDA, Max-Planck-Institut Saarbrücken).

Certain satisfiability problems can be solved efficiently by graph theoretic methods. This is of importance for theoretical computer science as well as several practical applications (for example, verification of computer chips). The question, whether a propositional expression is satisfiable (known as the "SAT problem") is of practical as well as theoretical importance. Many problems that arise in practical applications can be formulated as SAT problems (e.g., verification of computer chips, validation of railway signals, etc.); on the other hand, the SAT problem holds a central role in theoretical computer science and complexity theory (it was the first problem shown to be NP-complete). For the present research project, certain combinatorial structures ("proof graphs") were used to model instances of the SAT problem. Due to this representation, it was possible to apply graph theoretic concepts to SAT-problems. In particular, matching theory turned out to be very appropriate for this approach; indeed, by the use of concepts from matching theory, algorithms for the recognition of certain subclasses of minimally unsatisfiable formulas could be developed; this solved a conjecture by Kleine Büning. Furthermore, the concept of graph homomorphisms could be applied successfully to proof graphs, yielding new results for the theory of propositional proof systems. For example, a new characterization of so-called "tree resolution" in terms of homomorphisms could be given.