| | All
sessions take place in auditorium 3.09:00- | 09:30
| Miquel Bofill, U Girona, Spain Albert
Rubio, Techn. U of Catalonia, Spain
**Well-foundedness
is sufficient for completeness of ordered
paramodulation** For
many years all known completeness results for Knuth-Bendix
completion and ordered paramodulation required the term ordering **>**
to be well-founded, monotonic and
total(izable) on ground terms. Then, it was shown that well-foundedness and
the subterm property were enough for ensuring completeness of ordered
paramodulation. Here we show that the subterm property is not necessary
either. By using a new restricted form of rewriting we obtain a
completeness proof of ordered paramodulation for Horn clauses with equality
where well-foundedness of the ordering suffices. Apart from the fundamental
interest of this result, some potential applications motivating the
interest of dropping the subterm property are given. |
09:30- | 10:00
| Christopher Lynch, Clarkson U, USA Barbara
Morawska, Clarkson U, USA
**Basic
syntactic mutation** We
give a set of inference rules for *E*-unification, similar to the
inference rules for Syntactic
Mutation. If the *E* is finitely saturated by
paramodulation, then we can block certain terms from further inferences.
Therefore, *E*-unification is decidable in *NP*, as is also the case
for Basic Narrowing.
However, if we further restrict *E*, then our
algorithm runs in quadratic time, whereas Basic Narrowing does not become
polynomial, since it is still nondeterministic. |
10:00- | 10:30
| Thomas Hillenbrand, MPI Saarbrücken, Germany Bernd
Löchner, U Kaiserslautern, Germany
**The
next Waldmeister loop** In
saturation-based theorem provers, the reasoning process
consists in constructing the closure of an axiom set under inferences. As
is well-known, this process tends to quickly fill the memory available
unless preventive measures are employed. For implementations based on the
Discount loop, the passive facts are responsible for most of the memory
consumption. We present a refinement of that loop allowing such a
compression that the space needed for the passive facts is linearly bound
by the number of active facts. In practice, this will reduce memory
consumption in the Waldmeister system by more than one order of magnitude
as compared to previous compression schemes. |
11:00- | 11:30
| Jean-Marc Andreoli, Xerox Grenoble, France
**Focussing
proof-net construction as a middleware paradigm** This
paper introduces a new formulation of the computational
paradigm based on proof-construction in terms of proof-nets. It shows the
relevance of this paradigm, thus formulated, to capture some of the
fundamental mechanisms of distributed computation (and in particular,
transaction mechanisms), which are familiar concepts of middleware
infrastructures. It therefore constitutes a first step in the direction of
the definition of a steady conceptual framework in which to formalise and
study various middleware notions, which, until now, have essentially been
studied through ad-hoc and diverse formalisms. Due to space constraints,
the proofs of the technical results of this paper have been skipped. They
were reviewed with the initially submitted version of the paper and are
available from the author. |
Joint
with TABLEAUX 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. |
| |