Franz Baader: Syntactic sugar can speed up reasoning in Description Logics

Abstract: Motivated by a chemical process engineering application, we look at a new concept constructor in Description Logics (DLs), an n-ary variant of the existential restriction operator, which generalizes both existential restrictions and so-called qualified number restrictions. Given concepts C1,..,Cn and a role r, this constructor allows us to say that there are n DIFFERENT role-successors d1,...,dn of a given individual d such that di belongs to Ci for i = 1,...n.

We show the following:

1. The new constructor can be expressed in ALCQ, the extension of the basic DL ALC by qualified number restrictions. However, this results in an exponential blow-up of the concept description. In addition, the translated descriptions contain a high number of \"expensive\" disjunctions and qualified number restrictions. Consequently, applying (even highly optimized) reasoners for ALCQ to these descriptions does not result in a good performance.
2. By giving a direct tableau-based algorithm for ALC extended with the new constructor, we can show that the complexity of reasoning in this new DL is not harder than the one of reasoning in ALCQ.
3. Moreover, when restricting to a DL that provides only the new constructor together with conjunction, then the subsumption problem becomes polynomial. This restricted DL is actually sufficient for the chemical process engineering application mentioned above.

Thus, although the new constructor can be viewed as syntactic sugar in ALCQ, having it explicitly available, rather than expressing it by an exponentially large ALCQ concept description, results in a significant speed up of reasoning.

Chad E. Brown: Automated Theorem Proving in Extensional Type Theory

Abstract: In order to prove theorems involving sets and functions, one often uses comprehension principles asserting the existence of certain sets. When higher-order logic is formulated using simply typed lambda calculus, set comprehension principles correspond to including certain logical constants in the formulation.

On the semantic side, one can consider combinatory frames which may lack interpretations for certain logical constants. Using such frames as models for fragments of extensional type theory, one can show that certain logical constants are necessary to prove a certain theorem.

To ensure completeness, a higher-order theorem prover must ensure that instantiations for sets definable using logical constants can be discovered. In the presence of extensionality, one can make several restrictions to the set instantiations necessary without sacrificing completeness. For example, one can restrict the logical constants available for set instantiations.

LEO and TPS are two theorem provers which search for proofs in extensional type theory. We will briefly indicate the extensional aspects of TPS.

Abstract: It is well-known that formulas from modal logic K can be translated into the intersection of the guarded fragment and the 2-variable fragment by the standard relational translation. (We call this fragment GF2)

However many simple modal logics, like e.g. S4, have their translation outside of GF2, because of the transitivity property.

In order to overcome these problems, many extensions of the guarded fragment have been proposed, In this talk, I suggest another solution: Modifying the relational translation. We give a modified relational translation, which is satisfiability preserving, and which translates formulas from S4 into GF2. We identify a class of logics (regular grammar logics with converse) for which such a translation is possible, and provide a characterization for determining whether a modal logic is a regular grammar logic with converse.

Abstract: Bounded model checking is a promising approximation technique for model checking linear time logics. So far, it is known how do it for LTL. But LTL can only express First-Order-definable properties on omega-words. In order to be able to express Monadic-Second-Order-, i.e. regular properties of infinite words, one has to employ the linear time mu-calculus. We show how to do bounded model checking for the linear time mu-calculus.

Dietrich Kuske: MSO-definierbare lokale temporale Logiken fuer Mazurkiewicz-Spuren

Abstract: Temporale Logiken fuer Mazurkiewicz-Spuren sind in den vergangenen 15 Jahren ausfuehrlich untersucht worden. Um fuer die Verifikation nutzbar zu sein, muss hierbei sichergestellt werden, dass das Erfuellbarkeits- und das Model Checking Problem in vertretbarer Komplexitaet geloest werden koennen. Bisher wurden fuer alle neu eingefuehrten lokalen temporalen Logiken neue Beweise dafuer angegeben, dass diese Probleme in PSPACE loesbar sind. Im Vortrag werde ich ein allgemeines Resultat herleiten, das auf alle bekannten (und viele weitere) lokale temporale Logiken anwendbar ist. Hierbei wird ein Zusammenhang zwischen der Komplexitaet der genannten Probleme und der Form der verwandten Modalitaeten hergestellt werden. Ein Ausblick befasst sich dann mit der Frage, inwiefern sich diese Ergebnisse auf sog. Message Sequence Charts erweitern lassen.

Diese Untersuchungen wurden zusammen mit Paul Gastin (Paris) durchgefuehrt und erste Ergebnisse wurden auf CONCUR 2003 vorgestellt.

Ralf Küster: Automatic Analysis of Cryptographic Protocols with Exclusive Or and Diffie-Hellman Exponentiation

Abstract: Operators such as XOR and Diffie-Hellman exponentiation are frequently used in cryptographic protocols. However, most formal methods for analyzing cryptographic protocols cannot handle these operators. In particular, up until recently deciding the security of protocols in presence of XOR and Diffie-Hellman exponentiation has been an open problem.

In this talk, I first provide a brief overview of the various approaches for analyzing cryptographic protocols and introduce the standard Dolev-Yao model–-the intruder model most methods for the (semi-)automatic analysis of protocols are based on. I then extend the Dolev-Yao model to include XOR and Diffie-Hellman exponentiation, respectively, and illustrate that within the resulting models new attacks on realistic protocols can be found. Finally, I present the main result which says that deciding the insecurity of protocols in these models is NP-complete.

Bernd Löchner: A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting

Abstract: Redundancy criteria are an important means to restrict the search space of a theorem prover. In the presence of associative and commutative (AC) operators saturating provers soon generate many similar equations. Most of them are redundant. One approach is therefore to work modulo AC. This means a considerable implementation effort because core routines (e.g. for unification or matching) have to be extended. Furthermore, new restrictions apply. For example orderings have to be AC-compatible.

Our approach is different in that we retain the usual unfailing completion procedure and refine it with appropriate redundancy criteria. This allows us to keep all of the implementation. Only small extensions have to be made.

We present a new redundancy criterion that is based on ground reducibility by ordered rewriting and can be specialized for the AC-case. The criterion uses a new sufficient test for the unsatisfiability of ordering constraints. The test runs in polynomial time, is easy to implement, and covers reduction orderings in a generic way, with possible extensions for LPO and KBO. Experiments show that the new criterion can lead to significant speed-ups, especially for challenging proof tasks.

If time permits we present some work-in-progress in which we generalize the approach to a related critical-pair criterion.

Andreas Meier: Beweisplanen mit mehreren Strategien

Abstract: Strategien sind unabhängige Komponenten für das Beweisplanen, wobei verschiedene Strategien verschiedene Verfeinerungen oder Modifikationen eines Beweisplans realisieren können. Im Vergleich mit dem bisherigen Beweisplanen führt Beweisplanen mit mehreren Strategien eine neue Hierarchieebene und deren heuristische Kontrolle ein. Sowohl die Strategien selbst als auch ihre Kontrolle können (mathematisches) Wissen über eine Domäne kodieren.

In dem Vortrag wird sowohl die Motivation für Beweisplanen mit mehreren Strategien als auch die Realisierung im MULTI-System und dessen Anwendungen in Fallstudien diskutiert.

Tobias Schmidt-Samoa: Introduction to the New Proof Control of the Inductive Theorem Prover QuodLibet

Abstract: QuodLibet is an inductive theorem prover for the specification and verification of algorithms in the style of abstract data types. It admits partial definitions of operators over free constructors using (possibly non-terminating) positive/negative-conditional equations as well as destructor recursion or mutual recursion. Proofs are performed within a human-oriented inference system which easily allows required user interactions. Automation is achieved by tactics written in an adapted imperative programming language QML.

Induction is performed lazily by descente infinie, i.e. lemmas are used inductively if needed resulting in additional proof obligations that guarantee the wellfoundedness of the induction scheme. This allows us to simulate explicit induction without inheriting its disadvantages if the analysis process is not strong enough to compute the right induction hypotheses. This helps us to prove properties of mutually recursive functions as e.g. properties of the lexicographic path order (LPO).

In this talk we will give a short introduction to QuodLibet's induction mechanism as well as its new proof control. Especially, we will present new heuristics for contextual rewriting based on obligatory and mandatory literals that have to be handled when relieving conditions of conditional lemmas.

Abstract: We present some results on modular refutational theorem proving in first-order logic with equality.
We start by presenting a superposition calculus for clauses over signatures where functions can be declared as either total or partial. We show that the calculus is modular in cases of theory combinations where all functions that are not in the intersection of the signatures are declared to be partial. (Modularity means that inferences are pure, only involving clauses over the alphabet of one of the theories). Moreover, we consider a constraint superposition calculus for the case of hierarchical theories and show that it has a related modularity property.

We then identify some interesting problem classes where partial models can always be totalized - namely shallow and local extensions of a base theory -, show that for those classes of extensions constraint superposition is complete and modular also with respect to the total algebra semantics of the theories, and present several applications of this result.

(Joint work with Harald Ganzinger and Uwe Waldmann.)

Bao Quoc Vo: A Proof-Manager for the DIALOG Project