 | |
All
sessions take place in auditorium 3.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. |
| 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. |
| 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 t1≤t2
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. |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
