Scottish Theorem Proving

Jonathan Heras: Proof-Pattern Recognition and Lemma Discovery in ACL2

ACL2 is a theorem prover that has features of both Interactive Theorem Provers and Automatic Theorem Provers: it will try to prove given conjectures automatically, but strongly relies on the user having supplied the auxiliary lemmas required for rewriting. In this talk, we present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery applied in ACL2. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. We will present the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.

Brian Campbell: Randomised testing of a HOL 4 microprocessor model

We consider validating a HOL 4 model of the ARM Cortex-M0 microcontroller core by testing the model's behaviour on a randomly chosen instructions against a real chip.

The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions will not give us sufficient confidence in the model. Thus we test randomly chosen sequences of instructions at once.

This produces some interesting constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. I will talk about the relevant features of the model, how we synthesise tests, how we approach solving the constraints using an SMT solver, and what has happened in practice so far.

Daniel Raggi: Re-...-re-representation

My main interest is the role of representation in reasoning. In this talk I'll present my work on formalising transformations (in Isabelle/HOL) and automating a method of reasoning in which the representation of the problem in question is transformed in the attempt to solve it. In the paradigm I'm working, any mapping between the types of a domain can be the basis for a transformation, provided that we can find sufficient matches between the functions and relations of the types of both domains, and that these matches respect the original mapping. For example, if we take the mapping that associates every list with the set of its elements, we can match the function 'append' of lists to 'union' of sets. Realising matches between domains establishes interesting logical relations between them (e.g., we can transform some problems about sets into problems about lists). I have identified and formalised a number of common transformations particularly useful in discrete mathematics. Some proofs using these have been fully formalised in an interactive manner. The next step is to do some experiments in which the transformations are incorporated in the automatic search of a proof.

Steven Obua: ProofPeer: Collaborative Theorem Proving