Friday March 14th, 2003
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.
2.15-2.45pm:
Reasoning about Guarded Formulae
Lilia Georgieva
School of Mathematical and Computer Sciences, Heriot-Watt University
Abstract
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.
2.45-3.15pm:
Transcendental Functions and The Inverse Function Theorem in PVS
Ruth Hardy
School of Computer Science, University of St Andrews
Abstract
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.
3.15-3.45pm:
Tea and Coffee
3.45-4.15pm:
Proving Exception Freedom within High Integrity Software Systems
Bill J. Ellis
School of Mathematical and Computer Sciences, Heriot-Watt University
Abstract
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.
4.15-4.45pm:
Using Features to Choose Methods in Integral Calculus Proof Planning
Alex Heneveld
School of Informatics, University of Edinburgh
Abstract
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.