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.

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.

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.

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".