| | Sessions
take place in auditorium 3 unless otherwise indicated.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. |
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. |
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 **D**_{k} (*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 **D**_{k}, in particular
their constructivity and their decidability. |
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. |
Joint
with ICLP
*Room:*
Restaurant Luftkastellet 20:30- | 22:00
| Veronica Dahl, Simon Fraser U, Canada Banquet
speaker: **Title TBA** |
| |