Talks at the CLAM/INKA/OMRS-2003 Workshop in Dagstuhl

Wednesday, April 2

Session 1:

14:00 14:05

Welcome Notes , Dieter Hutter (DFKI)

14:05 14:50

Proving Exception Freedom within High Integrity Software Systems, Bill J Ellis (Heriot-Watt University)

14:50 15:30

A Machine -Verified Code Generator, Christoph Walther and Stephan Schweitzer (TU Darmstadt)

Coffee Break

Session 2:

16:00 16:45

Descente Infinie, Claus-Peter Wirth (Saarland University)

16:45 17:30

Integrating HR and tptp2X into MathWeb to compare automated theorem provers Dialog in Natural Language on Mathematical Proofs Juergen Zimmer (Saarland University)

18:00

Dinner

Thursday, April 3

Session 3:

09:00 9:45

A Combination of Non-standard Analysis and Induction, Ewen McLean (University of Edinburgh)

9:45 10:30

From a Rational Reconstruction of Proof Search Paradigms towards a Unified Framework, Dieter Hutter (DFKI)

Coffee Break
11:00 11:45

Assertion retrieval in the context of proof planning, Quoc Bao Vo (Saarland University)

Lunch

Session 4:

14:00 14:45

Predicting the BNF of a Normal Form, Alan Bundy (University of Edinburgh)

14:45 15:30

Proof and Discovery in Category Theory, Alan Smaill (University of Edinburgh)

Coffee Break

Session 5:

16:00 16:45

Using Specification Transformations to Trigger Proof Transformations, Axel Schairer (DFKI)

16:45 17:30

Business Meeting

18:00

Dinner

Friday, April 4

Session 6:

09:00 9:45

A feature-based best-first planner for theorem proving / proof planning, Alex Heneveld (University of Edinburgh)

9:45 10:30

Initial Results from Proof Planning in Isabelle, Lucas Dixon (University of Edinburgh)

Coffee Break
11:00 11:45

Certifying solutions to permutation group problems, Volker Sorge (University of Birmingham)

Lunch


Alan Bundy (University of Edinburgh)

Predicting the BNF of a Normal Form

We look at the problem of automatically forming the output BNF of a class of formulae exhaustively rewritten by a set of rewrite rules. We discuss an algorithm for doing this proposed by Alan Smaill and discuss various theoretical properties that we would like any algorithm to have. This is joint work with Alan Smaill and Predrag Janicic.


Christoph Benzmueller (Saarland University)

Dialog in Natural Language on Mathematical Proofs - cancelled

Knowledge representation within mathematical proof assistants is generally used solely for the purpose of proving theorems. Aiming at a broader scope, we examine the role of mathematical knowledge for the ambitious purpose of intelligent tutoring. Based on experiments with a simulated tutorial system for teaching proofs in elementary set theory, we formulate some requirements on knowledge representation within a logical system. These requirements include explicit reference between natural language text portions and mathematical formulas, determining the semantic role of mathematical formulas in context, and the potential contribution of user specified inference steps.


Lucas Dixon (University of Edinburgh)

Initial Results from Proof Planning in Isabelle

We outline our approach to proof planning in generic proof assistant Isabelle and how it has been implemented in IsaPlanner. We present some of the techniques encoded and describe some initial results using these techniques.


Bill J Ellis (Heriot-Watt University)

Proving Exception Freedom within High Integrity Software Systems

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.


Alex Heneveld (University of Edinburgh)

A feature-based best-first planner for theorem proving / proof planning.


Dieter Hutter (DFKI)

From a Rational Reconstruction of Proof Search Paradigms towards a Unified Framework

Research on automated and interactive theorem proving aims at the mechanization of logical reasoning. Aside from the development of logic calculi it became rapidly apparent that the organization of proof search on top of the calculi is an essential task in the design of powerful theorem proving systems. Different paradigms of how to organize proof search have emerged in that area of research, the most prominent representatives are generally described by the buzzwords: automated theorem proving, tactical theorem proving and proof planning. Despite their paradigmatic differences, all approaches share a common goal: to find a proof for a given conjecture. In this talk we start with a rational reconstruction of proof search paradigms in the area of proof planning and tactical theorem proving. Guided by similarities between software engineering and proof construction we develop a uniform view that accommodates the various proof search methodologies and eases their comparison. Based on this view, we propose a unified framework that enables the combination of different methodologies for proof construction to take advantage of their individual virtues within specific phases of a proof construction. This is joint work with Serge Autexier and Christoph Benzmueller.


Ewen McLean (University of Edinburgh)

A Combination of Non-standard Analysis and Induction.

We present a technique for constructing proof-plans for analysis proofs, in the case where the goal is existential. We introduce the notion of partitioning, which constructs a sequence of intervals, and show how non-standard analysis can be used to simplify the reasoning when the sequence is infinite. We use Rolle's Theorem as a case study to exemplify the technique.


Quoc Bao Vo

Assertion retrieval in the context of proof planning


Alan Smaill (University of Edinburgh)

Proof and Discovery in Category Theory

The book "Conceptual Mathematics" by Lawvere and Schanuel gives an introduction to Category Theory intended to be accessible to beginning university students. Unusually for texts on category theory, it emphasises techniques for the discovery of various constructions, rather than pulling them out of a hat in the middle of a proof. I present a version of this approach in the context of proof planning, where I attempt to capture both the theory and the discovery techniques in a declarative manner.


Axel Schairer (DFKI)

Using Specification Transformations to Trigger Proof Transformations.

Formal methods are an efficient way to increase the quality of the software development process, in particular in early phases where specification and proofs play the role of rigorous inspections. The consequence is that frequent changes are an inevitable part of the process and that better tool support is indispensable in practice. We propose a novel approach that considers specification and proofs as one compound entity, and in which changes are transformations on specification and proofs. We present a framework to express transformations on a structured specification systematically, propagating information about what is changed. When proof obligations are changed in this process, the propagated information is available to trigger corresponding proof transformations, similar to the ones which we have presented at last year's CIAO.


Volker Sorge (University of Birmingham)

Certifying solutions to permutation group problems.

We describe the integration of permutation group algorithms with proof planning. We consider eight basic questions arising in computational permutation group theory, for which our code provides both answers and a set of certificates enabling a user, or an intelligent software system, to provide a full proof of correctness of the answer. To guarantee correctness we use proof planning techniques, which construct proofs in a human-oriented reasoning style. This gives the human mathematician the necessary insight into the computed solution, as well as make it feasible to check the solution for relatively large groups.

This is joint work with Arjeh Cohen, Scott Murray, and Martin Pollet.


Christoph Walther and Stephan Schweitzer (TU Darmstadt)

A Machine -Verified Code Generator

We consider the machine-supported verification of a code generator computing machine code from WHILE-programs, i.e. abstract syntax trees which may be obtained by a parser from programs of an imperative programming language. We motivate the representation of states developed for the verification, which is crucial for success as the interpretation of the tree-structured WHILE-programs differs significantly in its operation from the interpretation of the linear machine code. This work has been developed for a course to demonstrate to the students the support gained by computer-aided verification in a central subject of computer science, boiled down to the classroom-level. We report about the insights into the properties of machine code obtained as well as the challenges and efforts encountered when verifying the correctness of the code generator, and also illustrate the performance of the VeriFun system which has been used for this work.


Claus Peter Wirth (Saarland University)

Descente Infinie

While structural induction is known continuously for over two millenia now, The ancient Greek's descente infinie had to be rediscovered by Pierre de Fermat in the middle of the 17th century. As descente infinie is the method of choice for the working mathematician to engineer hard induction proofs, for which the induction axioms cannot be guessed by recursion analysis, more attention should be payed to its computer support.


Juergen Zimmer (Saarland University)

Integrating HR and tptp2X into MathWeb to compare automated theorem provers

The assessment and comparison of automated theorem proving systems (ATPs) is important for the advancement of the field. At present, the de facto assessment method is to test provers on the TPTP library of nearly 6000 theorems. We describe here a project which aims to complement the TPTP service by automatically generating theorems of sufficient difficulty to provide a significant test for first order provers. This has been achieved by integrating the HR automated theory formation program into the MathWeb Software Bus. HR generates first order conjectures in TPTP format and passes them to a concurrent ATP service in MathWeb. MathWeb then uses the tptp2X utility to translate the conjectures into the input format of a set of provers. In this way, various ATP systems can be compared on their performance over sets of thousands of theorems they have not been previously exposed to. Our purpose here is to describe the integration of various new programs into the MathWeb architecture, rather than to present a full analysis of the performance of theorem provers. However, to demonstrate the potential of the combination of the systems, we describe some preliminary results from experiments in group theory.

Go Back