TABLEAUX on Wednesday

Detailed program
Wednesday July 31st, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

Session 3

09:00-10:00  Dale Miller, Penn State U, USA
Elaine Pimentel, Penn State U, USA
Invited talk: Using linear logic to reason about sequent systems
Linear logic can be used as a meta-logic for the specification of some sequent calculus proof systems. We explore in this paper properties of such linear logic specifications. We show that derivability of one proof system from another has a simple decision procedure that is implemented simply via bounded logic programming search. We also provide conditions to ensure that an encoded proof system has the cut-elimination property and show that this can be decided again by simple, bounded proof search algorithms.

10:00-10:30  Martin Giese, Karlsruhe U, Germany
A model generation style completeness proof for constraint tableaux with superposition
We present a calculus that integrates equality handling by superposition into a free variable tableau calculus. We prove completeness of this calculus by an adaptation of the model generation technique commonly used for completeness proofs of resolution calculi, e.g. by Bachmair and Ganzinger or Nieuwenhuis and Rubio. The calculi and the completeness proof are compared to earlier results of Degtyarev and Voronkov.

Session 4

11:00-11:30  Thomas Eiter, Vienna U of Techn., Austria
Volker Klotz, Vienna U of Techn., Austria
Hans Tompits, Vienna U of Techn., Austria
Stefan Woltran, Vienna U of Techn., Austria
Modal nonmonotonic logics revisited: Efficient encodings for the basic reasoning tasks
Modal nonmonotonic logics constitute a well-known family of knowledge-representation formalisms capturing ideally rational agents reasoning about their own beliefs. Although these formalisms are extensively studied from a theoretical point of view, most of these approaches lack generally available solvers thus far. In this paper, we show how variants of Moore's autoepistemic logic can be axiomatised by means of quantified Boolean formulas (QBFs). More specifically, we provide polynomial reductions of the basic reasoning tasks associated with these logics into the evaluation problem of QBFs. Since there are now efficient QBF-solvers, this reduction technique yields a practicably relevant approach to build prototype reasoning systems for these formalisms. We incorporated our encodings within the system QUIP and tested their performance on a class of benchmark problems using different underlying QBF-solvers.

11:30-12:00  Reinhold Letz, Techn. U of Munich, Germany
Lemma and model caching in decision procedures for quantified boolean formulas
The increasing role of quantified Boolean logic in many applications calls for practically efficient decision procedures. One of the most promising paradigms is the semantic tree format implemented in the style of the DPLL procedure. In this paper, so-called learning techniques like intelligent backtracking and caching of lemmas which proved useful in the pure propositional case are generalised to the quantified Boolean case and the occuring differences are discussed. Due to the strong restriction of the variable selection in semantic tree procedures for quantified Boolean formulas, learning methods are more important than in the propositional case, as we demonstrate. Furthermore, in addition to the caching of lemmas, significant advances can be achieved by techniques based on the caching of models, too. The theoretical effect of these improvements is illustrated by a comparison of the search spaces on pathological examples. We also describe the basic features of the system Semprop, which is an efficient implementation of (some of) the developed techniques, and give the results of an experimental evaluation of the system on a number of practical examples.

12:00-12:30  Balder ten Cate, U Amsterdam, The Netherlands
Chung-chieh Shan, Harvard U, USA
Question answering: from partitions to prolog
We implement Groenendijk and Stokhof's partition semantics of questions in a simple question answering algorithm. The algorithm is sound, complete, and based on tableau theorem proving. The algorithm relies on a syntactic characterization of answerhood: Any answer to a question is equivalent to some formula built up only from instances of the question. We prove this characterization by translating the logic of interrogation to classical predicate logic and applying Craig's interpolation theorem.

Session 5

14:00-14:30  George Metcalfe, King's College London, UK
Nicola Olivetti, U Turin, Italy
Dov Gabbay, King's College London, UK
Analytic sequent calculi for abelian and Lukasiewicz logics
In this paper we present the first labelled and unlabelled analytic sequent calculi for abelian logic A, the logic of lattice-ordered abelian groups with characterisic model Z, motivated by Meyer and Slaney as a logic of relevance and Casari as a logic of comparison. We also show that the so-called material fragment of A coincides with Lukasiewicz's infinite-valued logic L, hence giving us as a significant by-product, labelled and unlabelled analytic sequent calculi for L.

14:30-15:00  Matthias Baaz, Vienna U of Techn., Austria
Agata Ciabattoni, Vienna U of Techn., Austria
A Schütte-Tait style cut-elimination proof for first-order Gödel logic
We present a Schütte-Tait style cut-elimination proof for the hypersequent calculus HIF for first-order Gödel logic. This proof allows to bound the depth of the resulting cut-free derivation by 4ρ(d)|d|, where |d| is the depth of the original derivation and ρ(d) the maximal complexity of cut-formulas in it. We compare this Schütte-Tait style cut-elimination proof to a Gentzen style proof.

15:00-15:30  Mauro Ferrari, U Milan, Italy
Camillo Fiorentini, U Milan, Italy
Guido Fiorino, Varese U, Italy
Tableau calculi for the logics of finite k-ary trees
We present tableau calculi for the logics Dk (k≥2) semantically characterized by the classes of Kripke models built on finite k-ary trees. Our tableau calculi use the signs T and F, some tableau rules for Intuitionistic Logic and two rules formulated in a hypertableau fashion. We prove the Soundness and Completeness Theorems for our calculi. Finally, we use them to prove the main properties of the logics Dk, in particular their constructivity and their decidability.

Session 6

16:00-16:30  Calogero G. Zarba, Stanford U, USA
A tableau calculus for combining non-disjoint theories
The Nelson-Oppen combination method combines ground satisfiability checkers for first-order theories satisfying certain conditions into a single ground satisfiability checker for the union theory. The most significant restriction that the combined theories must satisfy, for the Nelson-Oppen combination method to be applicable, is that they must have disjoint signatures. Unfortunately, this is a very serious restriction since many combination problems concern theories over non-disjoint signatures.
In this paper we present a tableau calculus for combining first-order theories over non-disjoint signatures. The calculus generalizes the Nelson-Oppen combination method to formulae with quantifiers and to the union of arbitrary theories over non necessarily disjoint signatures.

16:30-17:00  Gernot Stenz, Techn. U of Munich, Germany
System description: DCTP 1.2
We describe version 1.2 of the theorem prover DCTP, which is an implementation of the disconnection calculus. The disconnection calculus is a confluent tableau method using non-rigid variables. This current version of DCTP has been extended and enhanced significantly since its participation in the IJCAR system competition in 2001. We briefly sketch the underlying calculus and the proof procedure and describe some of its refinements and new features. We also present the results of some experiments regarding these new features.

17:00-17:30  Luc Habert, LORIA Nancy, France
Jean-Marc Notin, LORIA Nancy, France
Didier Galmiche, LORIA Nancy, France
System description: LINK: a proof environment based on proof nets
LINK is a proof environment including proof nets-based provers for multiplicative linear logics: mixed linear logic, or recently called non-commutative logic (MNL), commutative linear logic (MLL) and non-commutative (or cyclic) linear logic (MCyLL). Its main characteristic is the provability analysis through automatic proof nets construction, that appears as a powerful alternative to deal with resource management in proof search. These provers can be also seen as implementations of new connection methods for these linear logic fragments.

17:30-18:30  TABLEAUX Business Meeting

Conference dinner

Joint with ICLP
Room: Restaurant Luftkastellet

19:30-20:30  Banquet

20:30-22:00  Veronica Dahl, Simon Fraser U, Canada
Banquet speaker: Title TBA