| | All
sessions take place in auditorium 3.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 *S*5
(for **K**) and *KD*45 (for **B**) with
the interaction axioms *I*:**K***φ*→**B***φ*
and *C*:**B***φ*→**K****B***φ*. 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. |
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 **S**atisfiability **A**lgorithm
for the **G**u**a**rded 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. |
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** |
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** |
| |