Joint seminar Moscow-Vienna

Workshop on Logic and Computation 2009

Семинар «Логика и вычислимость» 2009

June 29th - July 2nd 2009

Vienna University of Technology (TU Wien), Wiedner Hauptstrasse 8-10, 1040 Vienna, Austria

Building “Freihaus”, green zone (also known as tower “A”), 5th floor, Institute of discrete mathematics and geometry (E104), seminar room

Customised Google Map with locations relevant to the participants.

Map of the floors in the building.

This workshop brings together eminent researchers in the area of logic and computation and
continues a successful series of joint workshops organised by Steklov Institute Moscow and Vienna University of Technology.

The workshop will cover a variety of topics in theoretical and applied logic centered around the notions of proof and computation:
Topics include but are not restricted to proof theory, constructive logics, realizability, modal logic, Lambek calculus and linear logic, provability logics and algebras, formal arithmetic and fragments, methods of automated and interactive proof search, categorial grammars and other applications in linguistics, fuzzy logic and epistemic reasoning, proof complexity, computational complexity.

Participation at the workshop is free.

Program Commitee:
Matthias Baaz, (Vienna University of Technology, Kurt Gödel Society)
Lev Beklemishev, (Steklov Mathematical Institute of Moscow)

Organizational Commitee:
Matthias Baaz, Vienna University of Technology
Oliver Fasching, Vienna University of Technology

Supported by FWF and РФФИ (RFBR).

Preliminary time table:

Mo, 2009, June 29^th, Seminar room (open event)

Tu, 2009, June 30^th, Seminar room (open event)

We, 2009, July 1^st, Seminar room

Th, 2009, July 2^nd, Seminar room

We regret having to inform you, that Prof. Plisko had to cancel his participation in the event due to a sudden death of a close family member.
Our deepest condolences to Prof. Plisko and his family.

Abstracts:

Sergei Adian, Steklov Mathematical Institute of Moscow
Estimation of derivation lengths in one particular string rewriting system
Abstract: We shall study a string rewriting (semi-Thue) system in the alphabet {a,b,c} given by three rules: {aa→bc, bb→ac, cc→ab}. Termination of this system was proved by D. Hofmann and J. Waldmann in 2006. From their proof only an exponential upper bound on derivation lengths can be inferred. We give a sharp quadratic upper and lower bounds on derivation lengths for this system.

Matthias Baaz, Vienna University of Technology
Gödel Logics: The monadic class
Abstract: We describe the status of the decision problem for the monadic class of Gödel logics (both for decidability and satisfiability, which poses different problems) Especially we show the decidability of satisfiability for a subclass of the one-variable-class, which does not have the finite model property.

Lev Beklemishev, Steklov Mathematical Institute of Moscow
On topological interpretation of polymodal provability logic
Abstract: The well-known system of provability GLP (introduced by Japaridze) is known to be Kripke-incomplete. We study natural topological models of GLP where modalities correspond to derived set operators on a poly-topological space. We show topological completeness for the fragment of GLP with two modalities. On the other hand, for more than two modalities, completeness w.r.t. ordinal spaces turns out to be dependent on large cardinal axioms of ZFC and various facts on stationary sets and reflection. In particular, it is consistent (relative to ZFC) that GLP is incomplete. However, under the assumption of large cardinal axioms one can establish at least some partial completeness results. Partly joint work with Thomas Icard and Guram Bezhanishvili.

Christian Fermüller, Vienna University of Technology
Linguistics, Logic, and Vagueness

Ekaterina Fokina, University of Vienna
Algorithmic properties of structures and their theories
Abstract: In this lecture we survey the main directions of research in computable model theory. In particular we discuss the questions of existence and uniqueness of computable structures, as well as the questions of algorithmic complexity of theories with computable models and of classes of computable structures. We present some recent results and open questions in each of these directions.

Stefan Hetzl, Ecole Polytechnique, Paris
On the form of witness terms
Abstract: This talk will be about recent work on analyzing the development of terms during Gentzen-style cut-elimination in first-order logic and Peano arithmetic. The main result is a characterization of the form of witness terms in cut-free proofs in terms of structured combinations of basic substiutions that are read off from the proof with cuts. Based on this result, it is shown that each proof (with cuts) induces a regular tree grammar s.t. each term computable by cut-elimination can also be computed by the grammar. As another application, a class of proofs in first-order logic is shown to have only elementary cut-elimination. From the algorithmic point of view, what is obtained is a method for computing witness terms that circumvents cut-elimination and has several advantages, it allows for example to find the shortest witness term. In the second part of the talk, these results are extended to proofs of Σ⁰₁-formulas in Peano arithmetic.

Sándor Jenei, Vienna University of Technology
On the geometry of residuated lattices with applications
Abstract: A few geometric aspects of the study of residuated lattices will be summarized together with a new finding in this direction. By using it, we present one application: the structural description of e-involutive uninorms on [0,1]. This description involves a striking new construction, called skew-symmetrization, in which one has to leave the accustomed residuated setting, and enter the co-residuated setting. The main metamathematical contribution of this particular application is to point out: for the description of residuated structures one needs as well co-residuation.

Alexander Leitsch, Vienna University of Technology
Fast Cut-Elimination by CERES
CERES is a method of cut-elimination based on the construction of a resolution refutation r of a characteristic clause set CL(P) extracted from an LK-proof P. The complexity of cut-elimination by CERES is directly related to the size of the refutation r of CL(P). Methods of resolution decision procedures for clause classes provide powerful tools to identify classes of proofs admitting elementary cut-elimination, where reductive methods fail. We investigate several classes of proofs for which cut-elimination can be reduced to resolution refutations on well known decidable classes like Herbrand's class and the one-variable class. Finally we show that the complexity of CERES is uniformely superior to that of Gentzen-type reduction methods.

George Metcalfe, Vanderbilt University, USA
Interpolation and Amalgamation for Ordered Algebraic Structures
Abstract: In this talk I will explain how the logical property of interpolation can be used as a stepping stone to the algebraic property of amalgamation. In particular, I will give a simple proof of the so-called deductive interpolation property for lattice ordered abelian groups that implies not only the amalgamation property but also decidability and generation of the variety by the integers. I will also show how the approach can be modified to establish the amalgamation property for the variety of MV-algebras, the algebraic semantics for Łukasiewicz logic.

Magdalena Ortiz, Vienna University of Technology
Querying Description Logic Knowledge Bases: automata-theoretic techniques
Abstract: Description Logics (DLs) are a family of languages for logic representation. They have gained importance in the last years due to their role in the semantic Web and, more recently, to their popularity as mechanisms for structuring, accessing and sharing data repositories. As a consequence, using query languages known from databases to access DL knowledge bases has become a major topic of interest in the knowledge representation community. The area poses some very interesting challenges. Unlike the traditional database setting, infinite structures and incomplete data under the open world assumption must be handled. While DLs are closely related to modal and program logics, the considered query languages usually fall in orthogonal fragments of predicate logic. Novel ideas must be exploited in order to adapt and combine reasoning techniques from different fields. In this talk, we will discuss the query answering problem for expressive description logics. In particular, we discuss how techniques based on alternating two-way automata on infinite trees (2ATA) can be exploited for knowledge base reasoning and query answering in very expressive description logics, obtaining new tight complexity bounds and significantly pushing the decidability frontier with respect to both the query language and the considered DL.

Michel Parigot, University Paris 7
Deep inference and proof complexity

Mati Pentus, Moscow State University
Proof nets and NP-completeness of the Lambek calculus
Abstract: Given a sequent of the Lambek calculus, the variable part in proof search consists of axiom links. We consider two notions of proof nets, which provide efficient algorithms for checking whether given axiom links yield a proof net. We discuss some complexity results on Lambek calculus that have been proved using these proof nets (Mati Pentus, 2003; Yury Savateev, 2008).

Gernot Salzer, Vienna University of Technology
Description Problems over Finite Totally-Ordered Domains
Abstract: Constraints are a formalism to specify admissible assignments to variables. The constraint satisfaction problem is the question whether for a given constraint any admissible assignment exists. The description problem is in some sense the reverse question: given a set of assignments, find a constraint satisfied by (exactly) these assignments. We present several classes of many-valued formulas and affine constraints for which the description problem can be solved efficiently.

Ilya Shapirovsky, Institiute of Information Transmission Problems, RAS
Abstract: In this talk we consider fusions of ordered sums of transitive Kripke frames. We show that if satisfiability problems for classes of monomodal Kripke frames C₁ and C₂ are in PSPACE, then the satisfiability problem for the fusion I(C₁)∗I(C₂) is also in PSPACE, where I(C) denotes the class of ordered sums of frames from C over the class of all finite index sets. It leads immediately to PSPACE-decidability for a wide class of fusions of transitive modal logics.

Valentin Shehtman, Steklov Mathematical Institute of Moscow
Simplicial and metaframe semantics for modal predicate logics
Abstract: Simplicial and metaframe semantics were introduced by D. Skvortsov in 1990 as natural generalizations of Ghilardi's functor semantics. Unlike Kripke semantics, they are rather powerful, but not so handy. The talk gives an overview of main properties of these semantics, together with a new result sharpening Skvortsov's representation theorem.

Thomas Vetterlein, Medical University of Vienna
On logics handling both uncertainty and gradation

Daniel Weller, Vienna University of Technology
Proof Skolemization and De-Skolemization

© 2009. Impressum gem. § 25 MedienG: Kurt Gödel Gesellschaft, Wien

Latest change: 2009-06-24