CADE on Tuesday

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

All sessions take place in auditorium 3.

Session 13: Equational reasoning

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.

Session 14: Proof theory

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.

Invited talk

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.