TABLEAUX on Tuesday

Detailed program
Tuesday July 30th, 2002
See also the unified by-slot program

All sessions take place in auditorium 3.

Invited talk

Joint with CADE

11:30-12:30  Matthias Baaz, Vienna U of Techn., Austria
Invited talk: Proof analysis by resolution
Proof analysis of existing proofs is one of the main sources of scientific progress in mathematics: new concepts can be obtained e.g. by denoting explicit definitions in proof parts and axiomatizing them as new mathematical objects in their own right. (The development of the concept of integral is a well known example.) All forms of proof analysis are intended to make informations implicit in a proof explicit i.e. visible. Logical proof analysis is mainly concerned with the implicit constructive content of more or less formalized proofs. In this paper, we concentrate on automatizable logical proof analysis in first-order logic by means of incooperating resolution.

Session 1

14:00-14:30  Anatoli Degtyarev, U Liverpool, UK
Michael Fisher, U Liverpool, UK
Boris Konev, U Liverpool, UK
A simplified clausal resolution procedure for propositional linear-time temporal logic
The clausal resolution method for propositional linear-time temporal logics is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. In this paper, we show how the normal form can be radically simplified and, consequently, how a simplified clausal resolution method can be defined for this important variety of logic.

14:30-15:00  Nathalie Chetcuti-Sperandio, IRIT Toulouse, France
Tableau-based automated deduction for duration calculus
Duration Calculus is a temporal logic introduced to specify real-time systems. It is a very expressive but undecidable logic. In this paper we turn our attention to a decidable fragment for which we develop a tableau-based decision method taking into account some semantic restrictions.

15:00-15:30  Marta Cialdea Mayer, U Rome III, Italy
Carla Limongelli, U Rome III, Italy
Linear time logic, conditioned models and planning with incomplete knowledge
The "planning as satisfiability" paradigm, which reduces solving a planning problem P to the search of a model of a logical description of P, relies on the assumption that the agent has complete knowledge and control over the world. This work faces the problem of planning in the presence of incomplete information and/or exogenous events, still keeping inside the "planning as satisfiability" paradigm, in the context of linear time logic.
We give a logical characterization of a "conditioned model", which represents a plan solving a given problem together with a set of "conditions" that guarantee its executability. During execution, conditions have to be checked by means of sensing actions. When a condition turns out to be false, a different "conditioned plan" must be considered. A whole conditional plan is represented by a set of conditioned models. The interest of splitting a conditional plan into significant sub-parts is due to the heavy computational complexity of conditional planning.
The paper presents an extension of the standard tableau calculus for linear time logic, allowing one to extract from a single open branch a conditioned model of the initial set of formulae, i.e. a partial description of a model and a set of conditions U guaranteeing its "executability". As can be expected, if U is required to be minimal, the analysis of a single branch is not sufficient. We show how a global view on the whole tableau can be used to prune U from redundant conditions. In any case, if the calculus is to be used with the aim of producing the whole conditional plan off-line, a complete tableau must be built. On the other hand, a single conditioned model can be used when planning and execution (with sensing actions) are intermingled. In that case, the requirement for minimality can reasonably be relaxed.

Session 2

16:00-16:30  Reinhold Letz, Techn. U of Munich, Germany
Gernot Stenz, Techn. U of Munich, Germany
Integration of equality reasoning into the disconnection calculus
Equality handling has always been a traditional weakness of tableau calculi because the typical refinements of those calculi were not compatible with the most successful methods for equality handling. The disconnection tableau calculus represents a new confluent framework well suited for the integration of a large class of different methods for equality handling, as we demonstrate in this paper. We consider both saturation based and goal-oriented methods for equality handling. We also show how specialized equality handling can affect the properties of the calculus at the example of the well-known regularity condition. All the presented approaches of equality handling have been implemented in the theorem prover DCTP and we present the results of an experimental evaluation.

16:30-17:00  Viorica Sofronie-Stokkermans, MPI Saarbrücken, Germany
Deciding uniform word problems involving bridging operators on bounded distributive lattices
In this paper we analyze some fragments of the universal theory of distributive lattices with many sorted bridging operators. Our interest in such algebras is motivated by the fact that, in description logics, numerical features are often expressed by using maps that associate numerical values to sets (more generally, to lattice elements). We first establish a link between satisfiability of universal sentences with respect to algebraic models and satisfiability with respect to certain classes of relational structures. We use these results for giving a method for translation to clause form of universal sentences, and provide some decidability results based on the use of resolution or hyperresolution. Links between hyperresolution and tableau methods are also discussed, and a tableau procedure for checking satisfiability of formulae of type t1t2 is obtained by using a hyperresolution calculus.

17:00-17:30  Uwe Petermann, Leipzig U of Applied Sciences, Germany
A confluent theory connection calculus
In the present paper we combine two different enhancements of connection method based theorem proving calculi: a confluent connection calculus of Baumgartner, Eisinger and Furbach and our approach for building-in theories into connection calculi.