CIAO Abstracts

Formalising and Analysing Textbook Proofs: The Problem of Under-Specification and Granularity

Unlike computer algebra systems, automated theorem provers have not yet achieved considerable recognition and relevance in mathematical practise. A significant shortcoming of mathematical proof assistance systems is that they require the fully formal representation of mathematical content, whereas in mathematical practise an informal, natural-language-like representation where obvious parts are omitted is common. We aim to support mathematical paper writing by integrating a scientific text editor and mathematical assistance systems such that mathematical derivations authored by human beings in a mathematical document can be automatically checked. To this end, we first define a calculus-independent representation language for formal mathematics that allows for under-specified parts. Then we provide two systems of rules that check if a proof is correct and at an acceptable level of granularity. These checks are done by decomposing the proof into basic steps that are then passed on to proof assistance systems for formal verification. We show the feasibility of our approach using a textbook example proof.

Serge Autexier

Novel Directions in the OMEGA Project

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 Benzmüller

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

Constructing Induction Rules for Deductive Synthesis Proofs

We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof, but standard techniques for the construction of appropriate induction rules are restricted to recycling the recursive structure of the specifications. What is needed is induction rule construction techniques that can introduce novel recursive structures. We show that a combination of rippling and the use of meta-variables as a least-commitment device can provide such novelty.

Alan Bundy

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 and Pablo Nogueria-Iglesias

Rippling Rippling

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

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

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

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, Saarbrücken) and Volker Sorge (The University of Birmingham)

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

Dynamic Ontology Refinement

Interaction in multi-agent systems usually depends on the assumption that the agents have a common ontology. However, this is a strong assumption that restricts the applicability of such systems. In this talk, I will present our work on dynamic ontology refinement, which enables agents with non-identical ontologies to diagnose mismatches that are causing communication failure and refine their ontologies accordingly.

Fiona McNeill

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

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

Towards a bell-curve calculus and its application to e-Science

E-Scientists use workflow languages to describe the processing of their experimental data. It would be useful for them to get rough estimates of various quality of service properties of that processing, eg runtimes, accuracy, reliability, etc. We have previously speculated about the use of interval arithmetic to calculate error bounds on such estimates: arithmetic operates on number intervals rather than just numbers. Interval arithmetic is good for worse case analyses, but average case analyses would be more useful. If we associate a probability density function (pdf) with the estimate, then some values in the interval have a higher probability than others. Normal distributions (bell-curves) are often good pdfs for QoS properties, such as those above. So can we invent a bell-curve calculus comparable to interval arithmetic, ie can we define how bell-curves can be combined to form other bell-curves? Just as in interval arithmetic, the results of a bell-curve calculation can often only be approximated by a bell-curve, but that is ok for a rough estimate. We will describe our progress so far in developing such a calculus.

Lin Yang

Intelligent Brokering of Semantic Reasoning Web Services

In my talk I'm going to present the progress of my Ph.D. work on the description of Automated Theorem Proving (ATP) systems and proof transformation systems as Semantic Web Services in the W3C recommendation language OWL-S. I'll explain how a brokering agent can use AI planning to automatically compose reasoning services to answer given queries. The resulting service compositions can be elegantly described in the high-level programming language DTGolog [1]. Given a proving problem, the DTGolog interpreter can determine an optimal execution strategy for a composite service using performance data of the ATP systems.

[1] Craig Boutilier and Raymond Reiter and Mikhail Soutchanski and Sebastian Thrun: Decision-Theoretic, High-Level Agent Programming in the Situation Calculus

Jürgen Zimmer