Scottish Theorem Proving Meeting

Friday March 14th, 2003

Hosted by the
School of Mathematical and Computer Sciences
Heriot-Watt University
Riccarton, Edinburgh, EH14 4AS

Contact: Andrew Ireland

The next Scottish Theorem Proving meeting will take place on Friday March 14th between 2.15-4.45pm in Room 1.27 within the Earl Mountbatten Building - building 2 on the Edinburgh Campus Map.



Reasoning about Guarded Formulae

Lilia Georgieva

School of Mathematical and Computer Sciences, Heriot-Watt University


We study the guarded fragment of first-order logic in the framework of hyperresolution. The guarded fragment is a generalisation of the modal fragment and is introduced in an attempt to explain the good computational properties of modal logics. We provide a sound, complete and practical decision procedure for subfragments of the guarded fragment based on hyperresolution. The decision procedure corresponds to tableaux-based decision procedures prominent for modal and description logics. We show that the it is also a model builder for satisfiable guarded formulae and that it can be refined so that only minimal Herbrand models are generated. By using a suitable control strategy we obtain a decision procedure for guarded formulae with optimal polynomial space complexity. The decision procedure has concrete application domains. It provides a framework for reasoning about very expressive modal and description logics with role inverse that can be embedded into the guarded fragment. We show that the decidability and model building results can be extended to a new clausal class which allows for the embedding of formulae outside the guarded and the loosely guarded fragments.


Transcendental Functions and The Inverse Function Theorem in PVS

Ruth Hardy

School of Computer Science, University of St Andrews


Much support for the exponential and trigonometric functions has been built into PVS, however, the treatment of their inverses has been less thorough. In this talk I will give an overview of the existing support for these functions along with some simple example where this is not sufficient. I will discuss work done to build the inverse function theorem into PVS and show how this can be used, along with the existing support for the transcendental functions, to allow a more thorough treatment of the natural logarithm and the inverse trigonometric functions.


Tea and Coffee


Proving Exception Freedom within High Integrity Software Systems

Bill J. Ellis

School of Mathematical and Computer Sciences, Heriot-Watt University


SPARK is a formally defined subset of the Ada programming language. It was defined by Praxis Critical Systems for the development of high integrity software. For additional confidence SPARK users can prove that their code is free from run time errors (exception freedom). Using the Praxis Examiner tool, this task reduces to discharging a large number of verification conditions (VCs). Using the Praxis Simplifier, a light weight theorem prover, the vast majority (around 90%) of the VCs are automatically discharged. Our goal is to address the remaining VCs using a proof planning approach and in particular loop invariant discovery techniques.


Using Features to Choose Methods in Integral Calculus Proof Planning

Alex Heneveld

School of Informatics, University of Edinburgh


In this talk I will present some recent developments in the lambda-clam architecture including (1) a partial implementation of a global best-first algorithm, (2) the capability to have user-defined features guide the best-first planning search, and (3) applications of this approach to solving integrals in calculus, using features and plan steps observed from human subjects. This is work-in-progress seeking to improve automated reasoning by modelling human problem solving. A demonstration will be given.

Scottish Theorem Proving