Collegium Logicum 2007: Proofs and Structures

24/25 October 2007, Vienna, Austria

Supported by the bilateral PAI/ÖAD project "The Realm of Cut Elimination" between research groups in Paris (LIX, PPS) and Vienna (Theory and Logic Group). Supported and organized by the Kurt Gödel Society.

Participation at the workshop is free.

Venue

See this city map on how to find the building. The seminar room is located on the 3rd floor in the yellow area. It is most easily reached via staircase I (see map of the building).

Program and Organizing Committee

Matthias Baaz
Agata Ciabattoni
Stefan Hetzl
Norbert Preining

Participants

Program

Talks

M. Baaz: Decidability problems of partial proof descriptions

A. Beckmann: On the complexity of definable total search problems
In computational complexity, search problems are often converted into decision problems to fit into standard complexity classes. Often, this conversion produces a (polynomially) equivalent decision problem, but not always. This is particularly important for total search problems, where a solution is guaranteed to exist for each instance of the search problem. For example, consider the popular heuristics 2-OPT for the Travelling Salesperson Problem: given a weighted graph G, find a tour T of G that cannot be improved by swapping the successors of two nodes. The existence of such a tour is guaranteed, basically because any finite set of numbers has a least element. No polynomial time algorithm is known for this problem.
We will look at total search problems whose totality is guaranteed by a formal proof in a Bounded Arithmetic theory. We will describe the complexity of some total search problem classes via proof theoretic investigations based on cut-elimination. In particular, we make use of an ordinal informative method called dynamic ordinal analysis.

A. Ciabattoni: Uniform Standard Completeness Proofs

U. Egly: Reconstructing DPLL in Sequent Calculi
In the last decades, successful SAT solvers and QSAT solvers have been developed. The developement is mainly driven by practical applications and competitions, and theoretical investigations are often neglected. This is escpecially true for QBF-solvers and the requirement of prefix clausal form as an input form is a witness for this claim. This requirement implies a translation operation which increases the number of variables or disrupts the formula's structure. Moreover, the most important part of this transformation, prenexing, is not deterministic.
In this talk, we briefly discuss the disadvantages most of todays QBF solvers have and describe an alternative way to process QBFs without these drawbacks. We briefly describe our solver, qpro, which is able to handle formulas in negation normal form. To this end, we extend algorithms for QBFs to the non-normal form case. Especially, we generalize well-known pruning concepts to the nonclausal case. In order to prove properties of the algorithms generalized to nonclausal form, we use a sequent-style reconstruction of DPLL.

R. Iemhoff: Constructive Set Theory and Translations
Constructive set theory has been introduced as a foundational theory for constructive mathematics. We will discuss the system, explain why it is considered to be constructive, and define certain translations on the theory from which several of its constructive properties can be derived.

C. Fermüller: Interpreting interval based fuzzy logics
Various logics based on intervals of truth values (truth degrees) instead of single truth values have been proposed in the context of approximate reasoning and fuzzy logic. We discuss problems with coherent interpretations of truth functional connectives for these logics and outline a dialogue game based solution that also opens the way to adequate analytic proof systems.

S. Hetzl: On confluence properties of cut-elimination (joint work with M. Baaz)
We study the confluence behaviour of the standard syntactic cut-elimination procedure for classical logic. It turns out that the process of generating the Herbrand-universe of a given signature can be encoded in a proof with cuts: Its cut-elimination will non-deterministically compute a term out of all terms of a certain size.
This allows to define a sequence of short proofs exhibiting a significantly non-confluent cut-elimination behaviour: A proof in this sequence has non-elementary many different cut-free normal forms (each of non-elementary size). These normal forms are different in a strong sense: They not only represent different Herbrand-disjunctions but also have different propositional structures and hence they are not instances of a more general proof.

A. Leitsch: CERES: mathematical properties and applications
CERES (cut-elimination by resolution) is a method for cut-elimination in classical first-order logic. The method was developed mainly to perform cut-elimination on real mathematical proofs. In contrast to reductive methods (like this of Gentzen) a set of clauses C(φ) (the characteristic clause set) is extracted from an LK-proof φ of a sequent S. A resolution refutation γ of C(φ) then yields a skeleton of a proof φ' of S with at most atomic cuts. φ' is constructed by γ und φ by so-called proof projections. It can be shown that CERES outperforms reductive methods asymptotically, and even renders them redundant with respect to the characteristic clause set under subsumption. A serious defect of CERES was the need to skolemize the input-proof and to eliminate all cuts simultaneously. We show that skolemization can be avoided, making the elimination of single cuts possible. CERES has been successfully applied to the analysis of real mathematical proofs (like Fürstenberg's proof of the infinity of primes). Finally we present some ideas to extend CERES to inductive proofs in ACA₀ and to second-order proofs.

D. Miller: Focusing Proof Systems
I will outline various projects within the Parsifal team involved with understanding and applying the completeness of focusing proof systems. I will also present details of a general focusing framework for intuitionistic and classical logics.

N. Preining: Gödel logics over hyper reals
We will present motivation and first steps to define Gödel logics based on hyper reals. This research is motivated by an interesting result by Takano that the logic of the Kripke frame of the reals is axiomatizable.

L. Strassburger: Medial and Relation Webs
Medial is an inference rule scheme that appears in various deductive systems based on deep inference. In this talk we investigate the properties of medial as rewriting rule independently from logic. We present a graph theoretical criterion for checking whether there exists a medial rewriting path between two formulas. Finally, we return to logic and apply our criterion for giving a combinatorial proof for a decomposition theorem, i.e., proof theoretical statement about syntax.

K. Terui: How and when axioms can be transformed into good structural rules (joint work with A. Ciabattoni and N. Galatos)
The class of substructural logics consists of axiomatic extensions of FL (full Lambek calculus, or the multiplicative-additive fragment of intuitionistic noncommutative linear logic). When an axiom is added to FL, it may happen that it can be "structuralized," in the sense that it can be transformed into an equivalent set of structural rules. Furthermore, it may also happen that suc, when suitably structuralized, admits cut-elimination.
In this talk, we identify a natural class of axioms which can be well structuralized over FL. We also give a subclass of axioms that admit cut-elimination, and give a necessary and sufficient condition under which an axiom of the former type belongs to the latter. Our condition can be stated both in terms of an acylclicity property and a conservative extension property.

S. Terwijn: Embeddings into the Medvedev lattice
The Medvedev lattice is a structure from computability theory that is interesting for various reasons. It was originally introduced for its connections with constructive logic, but it is also interesting in other respects, for example in connection with computation on the reals, algorithmic randomness, or as a generalization of the Turing degrees. We study embeddability of lattices, algebras, and semilattices into the Medvedev lattice M. Sorbi showed that the countable dense Boolean algebra is embeddable into M. We show that this result is optimal: if a Boolean algebra is embeddable into M then it must be countable. On the other hand, if one drops the requirement that meets are preserved then much larger structures are embeddable. For example the large Boolean algebra of all subsets of the reals is embeddable as an upper semilattice into M. As for the closely related Muchnik lattice, we show that the previous large Boolean algebra is embeddable into it as an algebra.

H. Veith: Quantifier Distribution as Abstraction Method

D. Weller: Implementing CERES: tools for proof analysis
This talk deals with the implementation of tools necessary to analyse formalized mathematical proofs using cut-elimination. Three tools are presented: Handy LK, a compiler that transforms a proof specified in a higher level language into a formal LK proof; ProofTool, a graphical tool for viewing and editing formal proofs; and CERES, an implementation of cut-elimination by resolution. A short demonstration of the tools and their interaction is included in the talk.

2007 Kurt Gödel Society, Stefan Hetzl.

2007-10-23