CADE-19 in Miami

28 July - 2 August 2003

In the sunshine ... On the beach

Invited Speakers

Tony Cohn
Dr Tony Cohn is Professor of Automated Reasoning and Head of the School of Computing at the University of Leeds. Tony's research interests have always centred on knowledge representation and the control of reasoning. For a number of years he worked on expressive many sorted logics. His current major focus is on ontologies and logics for reasoning about physical systems and calculi for qualitative spatial and spatio-temporal reasoning in particular. The RCC calculus is perhaps the best known example of the work of his group at Leeds. Applications of this work include Geographical Information Systems and Cognitive Vision. The work has received support from a variety of sources including the UK funding council EPSRC, the EU and industrial partners.

Invited Talk: Reasoning about Qualitative Representations of Space and Time

In this talk I survey Qualitative Representations of Space and Time which have formed an increasingly active area of Knowledge Representation recently. Although most of the work has concerned topology and mereology (theories of parthood), known collectively as mereotopology, a variety of calculi have also addressed distance, size, orientation and, more generally, the notion of qualitative shape. Increasingly, calculi are now being designed to represent and reason about more than one such aspect simultaneously.

I will report on some of the complexity results known, and I will discuss some of the approaches to the usual tradeoff between expressiveness and tractability, including the use of special purpose logics and reasoning procedures, including composition tables, constraint based reasoning, and the use of intuititionistic and modal zero-order logics.

Spatial change is of great applicability in a variety of possible application domains, for example in reasoning about high level computer vision, or in geographic information systems. I will present the notion of a conceptual neighbourhood which can be used to capture continuous transitions of spatial entities over time. Traditionally, these have been hand computed, rather than being formally derived from more primitive notions. I will first discuss some alternative notions of qualitative continuity and then I will describe the challenge of using of machine reasoning tools techniques to verify the correctness of a conceptual neighbourhood graph. In this context, I will report on recent work conducted at Leeds addressing this challenge using the automated theorem prover SPASS.

Edmund Clarke
Dr Edmund Clarke is a Professor of Electrical and Computer Engineering and the FORE Systems Professor of Computer Science in the School of Computer Science at Carnegie Mellon University. Dr. Clarke's interests include software and hardware verification and automatic theorem proving. In his Ph.D. thesis he proved that certain programming language control structures did not have good Hoare style proof systems. In 1981 he and his Ph.D. student Allen Emerson first proposed the use of Model Checking as a verification technique for finite state concurrent systems. His research group pioneered the use of Model Checking for hardware verification. Symbolic Model Checking using BDDs was also developed by his group. This important technique was the subject of Kenneth McMillan's Ph.D. thesis, which received an ACM Doctoral Dissertation Award. In addition, his resarch group developed the first parallel resolution theorem prover (Parthenon) and the first theorem prover to be based on a symbolic computation system (Analytica).

Invited Talk: SAT-based Counterexample Guided Abstraction Refinement in Model Checking

We introduce a SAT based automatic abstraction refinement framework for model checking systems with several thousand state variables in the cone of influence of the specification. The abstract model is constructed by designating a large number of state variables as "invisible". In contrast to previous work where invisible variables were treated as free inputs we describe a computationally more advantageous approach in which the abstract transition relation is approximated by "pre-quantifying" invisible variables during image computation. The abstract counterexamples obtained from model-checking the abstract model are symbolically simulated on the concrete system using a state-of-the-art SAT checker. If no concrete counterexample is found, a subset of the invisible variables is reintroduced into the system and the process is repeated. The main contribution of this paper are two new algorithms for identifying the relevant variables to be reintroduced. These algorithms monitor the SAT checking phase in order to analyze the impact of individual variables. Our method is complete for safety properties AG p in the sense that - performance permitting - a property is either verified or disproved by a concrete counterexample. Experimental results are given to demonstrate the power of our method on real-world designs.

Hélène Kirchner
Dr Hélène Kirchner is a permanent researcher (Directeur de Recherche) at CNRS. Since January 2001 she has been the Director of LORIA and INRIA-Lorraine, a joint research center between CNRS, INRIA, and Nancy Universities. In her Habilitation Thesis she studied completion procedures for term rewriting systems modulo sets of equations, and applications to automated deduction. As post-doctoral fellow at Stanford University she contributed to the design and implementation of the algebraic programming language OBJ-3. Back in France her research interests then turned to constraint solving, combinations of solvers, and theorem proving with constraints, where she made several theoretical contributions. The project team Protheo, which she led 1997-2000, has developed the ELAN software, an environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies, backed up by rewriting logic and rewriting calculus. Her current research interests are the study of non-deterministic rewriting and strategies, termination proof under strategies, modelisation with rule-based languages, and the combination of proof assistants with rewrite based systems.

Invited Talk: Proof Search and Proof Check for Equational and Inductive Theorems

This talk presents an on-going research project on theoretical and practical issues of combining rewriting based automated theorem proving and user-guided proof development, with the strong constraint of safe cooperation of both. In practice, we instantiate the theoretical study on the COQ proof assistant and the ELAN rewriting based system. A first approach of cooperation between COQ and ELAN is described, where COQ delegates equational proofs by rewriting to ELAN, builds a proof term while doing the proof. This proof term is then returned to COQ and checked. In the context of proof by structural induction performed by COQ, this technique is currently used in experiments for proving both the base case and the induction case by rewriting. However proofs by noetherian induction performed by rewriting are much more powerful than structural induction.

A second approach, which is yet on-going work, is then presented. Based on the description at the proof theoretical level of proof by noetherian induction provided by the deduction modulo framework, we show how to use narrowing in order to perform proof search for an inductive proof by rewriting, and how to build a proof term that can be checked by COQ. In order to check the proof, additional proof obligations to justify the noetherian induction principle in COQ are also needed. The talks thus presents different ingredients (especially rewriting and inductive proof techniques, proof term construction in rewriting calculus, and deduction modulo) that can contribute to the design of a development framework for certified and modular software.

Greg Nelson
Dr Greg Nelson received his Ph.D. in Computer Science from Stanford University in 1980, where he worked under the supervision of Bob Tarjan on program verification and algorithms for automatic theorem proving. He received his B.A degree in Mathematics from Harvard College in 1976. As an undergraduate at Harvard, he invented a method of combining decision procedures for different logical theories into a decision procedure for the combination of the theories (often called the "Nelson-Oppen method") that has become influential in the automatic theorem-proving community. He was a member of the committee that designed the programming language Modula-3, and was the author of the Juno constraint-based graphics system at the Computer Science Laboratory of the Xerox Palo Alto Research Center and one of the authors of its successor Juno-2. He has taught computing at Princeton University, and is currently a Principal Member of the Technical Staff at Hewlett-Packard Company's Systems Research Center.

Invited Talk: Reasoning About Quantifiers by Matching in the E-graph

The talk will describe the method used for reasoning about quantifiers in the Simplify theorem-prover, which is the reasoning engine inside the Extended Static Checkers built for Java and for Modula-3 at the DEC/Compaq/HP Systems Research Center. The essence of the method is pattern-based heuristic instantiation. The two main novelties are (1) because matching is performed in the E-graph instead of in an ordinary term DAG, the prover makes better use of equality information, and (2) two E-graph specific performance optimizations will be described, the "mod-time optimization" and the "pattern-elements optimization".