TABLEAUX on Thursday

Detailed program
Thursday August 1st, 2002
See also the unified by-slot program


All sessions take place in auditorium 3.

Session 7

09:00-09:30  Patrick Blackburn, LORIA Nancy, France
Maarten Marx, U Amsterdam, The Netherlands
Tableaux for quantified hybrid logic
We present a (sound and complete) tableau calculus for Quantified Hybrid Logic (QHL). QHL is an extension of orthodox quantified modal logic: as well as the usual [] and <> modalities it contains names for (and variables over) states, operators @s for asserting that a formula holds at a named state, and a binder ↓ that binds a variable to the current state. The first-order component contains equality and rigid and non-rigid designators. As far as we are aware, ours is the first tableau system for QHL.
Completeness is established via a variant of the standard translation to first-order logic. More concretely, a valid QHL-sentence is translated into a valid first-order sentence in the correspondence language. As it is valid, there exists a first-order tableau proof for it. This tableau proof is then converted into a QHL tableau proof for the original sentence. In this way we recycle a well-known result (completeness of first-order logic) instead of a well-known proof.
The tableau calculus is highly flexible. We only present it for the constant domain semantics, but slight changes render it complete for varying, expanding or contracting domains. Moreover, completeness with respect to specific frame classes can be obtained simply by adding extra rules or axioms (this can be done for every first-order definable class of frames which is closed under and reflects generated subframes).

09:30-10:00  Virginie Thion, U Paris XI (Paris-Sud), France
Serenella Cerrito, U Paris XI (Paris-Sud), France
Marta Cialdea Mayer, U Rome III, Italy
A general theorem prover for quantified modal logics
The main contribution of this work is twofold. It presents a modular tableau calculus, in the free-variable style, treating the main domain variants of quantified modal logic and dealing with languages where rigid and non-rigid designation can coexist. The calculus uses, to this end, light and simple semantical annotations. Such a general proof-system results from the fusion into a unified framework of two calculi previously defined by the second and third authors. Moreover, the work presents a theorem prover, called GQML-Prover, based on such a calculus, which is accessible in the Internet. The fair deterministic proof-search strategy used by the prover is described and illustrated via a meaningful example.

10:00-10:30  Linh Anh Nguyen, Warsaw U, Poland
Analytic tableau systems for propositional bimodal logics of knowledge and belief
We give sound and complete analytic tableau systems for the propositional bimodal logics KB, KB-C, KB-5, and KB-5C. These logics have two universal modal operators K and B, where K stands for knowing and B stands for believing. The logic KB is a combination of the modal logic S5 (for K) and KD45 (for B) with the interaction axioms I:KφBφ and C:BφKBφ. The logics KB-C, KB-5, KB-5C are obtained from KB respectively by deleting the axiom C (for KB-C), the axioms 5 (for KB-5), and both of the axioms C and 5 (for KB-5C). As analytic sequent-like tableau systems, our calculi give simple decision procedures for reasoning about both knowledge and belief in the mentioned logics.

Session 8

11:00-11:30  Jan Hladik, Dresden U of Techn., Germany
Implementation and optimization of a tableau algorithm for the guarded fragment
In this paper, we present Saga, the implementation of a tableau-based Satisfiability Algorithm for the Guarded Fragment (GF). Satisfiability for GF with finite signature is ExpTime-complete and therefore theoretically intractable, but existing tableau-based systems for ExpTime-complete description and modal logics perform well for many realistic knowledge bases. We implemented and evaluated several optimisations used in description logic systems, and our results show that with an efficient combination, Saga can compete with existing highly optimised systems for description logics and first order logic.

11:30-12:00  Claus-Peter Wirth, Saarland U, Germany
A new indefinite semantics for Hilbert's epsilon
After reviewing the literature on semantics of Hilbert's epsilon symbol, we present a new one that is similar to the referential interpretation of indefinite articles in natural languages.

12:00-12:30  Dan E. Willard, State U of New York-Albany, USA
Some new exceptions for the semantic tableaux version of the second incompletness theorem
This article continues our study of axiom systems that can verify their own consistency and prove all Peano Arithmetic's Π1 theorems. We will develop some new types of exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem.

Session 9: Position papers

14:00-14:20  Reiner Hähnle, Chalmers U of Techn., Sweden
Neil V. Murray, State U of New York-Albany, USA
Erik Rosenthal, U New Haven, USA
Position paper: Unit preference for ordered resolution and for connection graph resolution

14:20-14:40  Georg Moser, Vienna U of Techn., Austria
Position paper: Epsilon, delta, and speed-ups

14:40-15:00  James Harland, RMIT U, Australia
Position paper: Search calculi for classical and intuitionistic logic

15:00-15:20  Guido Fiorino, Varese U, Italy
Position paper: Improving the treatment of negation in propositional Dummett logic

15:20-15:40  Breanndán Ó Nualláin, U Amsterdam, The Netherlands
Position paper: Constraint tableaux

Session 10: Position papers

16:10-16:30  Frank M. Brown, U Kansas, USA
Position paper: A tableaux based system for propositional nonmonotonic logics

16:30-16:50  Jens Happe, Simon Fraser U, Canada
Position paper: Free-variable tableaux for efficient deduction in K

16:50-17:10  Regimantas Pliuskevicius, Inst. of Mathematics and Informatics, Vilnius, Lithuania
Position paper: A parametrical similarity saturation based decision procedure for a fragment of FTL

17:10-17:30  Norbert Preining, Vienna U of Techn., Austria
Position paper: Proof theory and proof systems for projective and affine geometry