 | |
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 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. |
| 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 |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
