PROOF PRESENTATIONS AND NOTATIONS
=================================


Serge Autexier

-----------------------------------------------------------


Proof Presentation
Jörg Siekmann

-----------------------------------------------------------

Intuitive and Formal Representations: The Case of Matrices


A major obstacle for bridging the gap between textbook mathematics and
formalising it on a computer is the problem how to adequately capture
the intuition inherent in the mathematical notation when formalising
mathematical concepts.  While logic is an excellent tool to represent
certain mathematical concepts it often fails to retain all the
information implicitly given in the representation of some
mathematical objects. In this work we concern ourselves with matrices,
whose representation can be particularly rich in implicit
information. We analyse different types of matrices and present a
mechanism that can represent them very close to their textbook style
appearance and captures the information contained in this
representation but that nevertheless allows for their compilation into
a formal logical framework.  This firstly allows for a more
human-oriented interface and secondly enables efficient reasoning with
matrices.

Manfred Kerber (The University of Birmingham)
joint work with: Martin Pollet  (Universitaet des Saarlandes, Saarbruecken) and
                 Volker Sorge   (The University of Birmingham)



--------------------------------------------------------------------


Novel Directions in the OMEGA Project

Abstract (first version): We report on the latest research directions
in the OMEGA project. The focus of this talk will be on the
integration of OMEGA with the scientific texteditor TeXmacs.

Chistoph Benzmueller

--------------------------------------------------------------------

FUNCTIONAL PROGRAMMING
======================

Automated reasoning by supercompilation.

Supercompilation (supervised compilation) is a technique of
specialisation (and, more generally, of transformation) of programs
written in functional programming languages. The technique was
introduced in the 1970s by V.F.Turchin. He proposed an idea of
creating a supercomplier, that is a tool which should observe
operation of a program implementing a function F on a partially
defined input.  These observations then can be used to formulate new
algorithmic definition (a program) for (an extension of) F.  Turchin's
ideas have been studied by a number of authors for a long time.
Several supercompilers, mainly for REFAL programming language, were
implemented.

It is interesting, that supercompilers can be used also for automated
reasoning and for verification of programs and protocols. The idea is
to encode a system/program/protocol to be verified as a parametrized
functional program and apply supercompilation in order to get an
equivalent transformed program, for which a correctness condition can
be easily checked, just by looking for simple syntactical property. It
has turned out this idea works surprisingly well in many cases,
including reasoning about and verification of finite state systems and
parametrized protocols.

In the talk we will give outline of the priniciples of
supercompilation, demonstrate and discuss results of various
experiments on automated reasoning and verification, which we have
done on a particular supercompiler SCP4.

Alexei Lisitsa and Andrei Nemytykh

--------------------------------------------------------------------

Experiences proving the Correctness of Student Functional Programs in
Isabelle

We have been proving the correctness of student functional programs in
Isabelle with the ultimate intention of creating an automated
proof-based tool to assist with program marking based upon IsaPlanner.
We discuss our preliminary observations.

Louise Dennis
joint work with Pablo Nogueria-Iglesias

--------------------------------------------------------------------

APPLICATIONS
============

XOR Constraints in Security API Modelling

We show how the use of XOR constraints in a first-order model allows
a theorem prover to reason effectively about security APIs using
bitwise XOR. Our primary case study is the API of the IBM 4758
hardware security module.

Graham Steel

-----------------------------------------------------------

PROGRAM VERIFICATION
====================

On Reasoning About Pointer Based Programs

Separation logic was developed for reasoning about programs that use
shared mutable data structures, in particular pointer based programs.
In this talk I will outline separation logic and sketch some related
ideas on proof automation.

Andrew Ireland

--------------------------------------------------------------------

INTEGRATION OF REASONERS
========================

Can a Higher-Order and a First-Order Theorem Prover Cooperate?

State-of-the-art first-order automated theorem proving systems have
reached considerable strength over recent years. However, in many
areas of mathematics they are still a long way from reliably proving
theorems that would be considered relatively simple by humans. For
example, when reasoning about sets, relations, or functions,
first-order systems still exhibit serious weaknesses.  While it has
been shown in the past that higher-order reasoning systems can solve
problems of this kind automatically, the complexity inherent in their
calculi and their inefficiency in dealing with large numbers of
clauses prevent these systems from solving a whole range of problems.

We present a solution to this challenge by combining a higher-order
and a first-order automated theorem prover, both based on the
resolution principle, in a flexible and distributed environment. By
this we can exploit concise problem formulations without forgoing
efficient reasoning on first-order subproblems. We demonstrate the
effectiveness of our approach on a set of problems still considered
non-trivial for many first-order theorem provers.

Volker Sorge

--------------------------------------------------------------------

The verification of programs in Hume.

Hume is a functional programming language. The verification is achieved by an
integrated approach combining model checking and theorem proving.

Gudmund Grov 

--------------------------------------------------------------------

PROOF TRANSFORMATION
====================

Using Induction for Cut-Simulation

In higher-order logic, the induction principle can be expressed
as a single sentence instead of as an axiom schema.
When an induction principle is included as a hypothesis,
however, one can simulate the cut rule.  The effect of
this simulation is that one can translate from a derivation
using the cut rule to a derivation without using the cut
rule without any significant increase in the size of the
proof.  Of course, this has negative consequences for
automated search for such proofs.


Chad Brown


Proof Transformations for Evolutionary Formal Development -- A Case
Study

Axel Schairer

--------------------------------------------------------------------
INDUCTION/RIPPLING
==================

Rippling Rippling

abstract: I will talk about a formalization of rippling based on
embedding terms and describe some experiments using Isabelle and
IsaPlanner to prove properties of this characterisation by induction
and rippling.

Lucas Dixon


--------------------------------------------------------------------