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 --------------------------------------------------------------------