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.
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).
Matthias Baaz
Agata Ciabattoni
Stefan Hetzl
Norbert Preining
Wednesday, October 24 - Seminar Room 185/2 | |
9:00-10:00 | A. Beckmann: On the complexity of definable total search problems (abstract) |
10:00-10:30 | Coffee Break |
10:30-11:00 | C. Fermüller: Interpreting interval based fuzzy logics (abstract) |
11:00-11:30 | S. Terwijn: Embeddings into the Medvedev lattice (abstract) |
11:30-12:00 | R. Iemhoff: Constructive Set Theory and Translations (abstract) |
12:00-14:00 | Lunch Break |
14:00-15:00 | D. Miller: Focusing Proof Systems (abstract) |
15:00-15:30 | Coffee Break |
15:30-16:00 | S. Hetzl: On confluence properties of cut-elimination (abstract) |
16:00-16:30 | H. Veith: Quantifier Distribution as Abstraction Method |
16:30-17:00 | Coffee Break |
17:00-18:00 | K. Terui: How and when axioms can be transformed into good structural rules (abstract) |
18:00-18:30 | A. Ciabattoni: Uniform Standard Completeness Proofs |
19:30- | Conference Dinner location: Restaurant Smutny, Elisabethstrasse 8, 1010 Wien Within walking distance of the workshop venue: map |
Thursday, October 25 - Laboratory 185/2 | |
9:30-10:00 | L. Strassburger: Medial and Relation Webs (abstract) |
10:00-10:30 | Coffee break |
10:30-11:00 | M. Baaz: Decidability problems of partial proof descriptions |
11:00-11:30 | U. Egly: Reconstructing DPLL in Sequent Calculi (abstract) |
11:30-12:00 | Coffee break |
12:00-12:30 | A. Leitsch: CERES: mathematical properties and applications (abstract) |
12:30-13:00 | D. Weller: Implementing CERES: tools for proof analysis (abstract) |
13:00-13:30 | N. Preining: Gödel logics over hyper reals (abstract) |
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_{0} 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 |