Previous Reasoning Seminars

Abstract:

Geometry Explorer is a prototype system that allows users to create Euclidean geometry constructions using a dynamic geometry interface, specify conjectures about them and then use an automatic, full-angle method prover to produce diagram independent, human-readable proofs to theorems. Geometry Explorer can then automatically generate novel diagrammatic proofs of the forward-chaining and backward-chaining reasoning used by the geometry theorem prover, as well as visualise multiple proofs to single theorems. We discuss the features of our system, how they were implemented and the issues encountered when trying to create diagrammatic full-angle method proofs.

Abstract:

I will introduce the new Proof General Kit framework for interactive proof, and in particular, it's underlying message passing protocol called PGIP. The core of PGIP allows one to interact with a theorem prover which follows the LCF tradition of goal-directed text based commands to construct a proof. Additional parts of PGIP allow manipulation of terms and proof parts in a graphical way, flexible editing of proof scripts, and preparation of literate proof scripts with content for document preparation systems. I'll describe the current state of implementation, and future extensions which include a generic tactic language within PGIP itself.

Abstract:

In this talk, I will report on my recent progress in the design and implementation of an inductive theorem prover called Poitin. This theorem prover utilises a transformation algorithm called distillation, which strictly extends deforestation, supercompilation and partial evaluation. I will give an overview of the distillation algorithm and will give some examples of its application, such as the transformation of a naive reverse function into an accumulating version. I will then describe how this transformation algorithm is used within Poitin to prove theorems, and will also give some examples of its application to conjectures which cause problems for existing inductive theorem provers. Prospects for further work will be discussed.

Abstract:

We introduce XOR constraints, and show how they enable a theorem prover to reason effectively about security critical subsystems which employ bitwise XOR. Our primary case study is the API of the IBM 4758 hardware security module, which is widely used in banking, ATM networks and electronic payment systems. We also show how our technique can be applied to standard cryptographic security protocols.

Abstract:

Finding tractable methods for program reasoning remains a major research challenge. We address this challenge using an integrated approach to tackle a niche program reasoning application. The application is proving exception freedom, i.e. proving that a program is free from run-time exceptions. Exception freedom proofs are a significant task in the development of high integrity software, such as safety and security critical applications. The SPARK approach for the development of high integrity software provides a significant degree of automation in proving exception freedom. However, when the automation fails, user interaction is required. We build upon the SPARK approach to increase the amount of automation available. Our approach involves extending the proof planning paradigm to include a program analysis capability.

Abstract:

I will outline some recent ideas on an approach to building a generic theorem-prover which would seem to offer greater flexibility to the user (i.e. encoder of logics) than current systems such as Isabelle. These ideas grew out of my joint work with Randy Pollack on encoding logics for ML programs in Isabelle. During the course of this work we came up against various restrictions which Isabelle seemed to impose on its object logics, which led me to consider whether a different approach might be advantageous, and to start implementing a concept demonstrator for such an approach. One important aspect of my proposal is that rather than work with a fixed form of judgement provided by a logical framework, the class of judgement forms itself is open-ended: new judgement forms are defined by the user, and proof rules may mix judgements of different kinds (this can be convenient for formalizing rules with side conditions, for instance). Moreover, a "high-level" logic can be definitionally introduced via a translation into a "low-level" one; in principle we could either prove the soundness of the high-level rules once for all, or validate particular instances of the high-level rules when they are used, or (most likely) something in between.

In this talk I will try to outline my vision for a new kind of generic theorem-prover along these lines, concentrating on examples of the kind of thing I think one would be able to do with it. However, the ideas are still at an embryonic stage, and I would very much welcome feedback and criticism from others who have worked in machine-assisted theorem proving.

Abstract:

Diagrams form an important part of almost all mathematical texts, providing an intuitive and appealing way to present what can be quite complex concepts. Yet they are rarely used within theorem provers. I will be looking at the use of diagrams within mathematical proof, and how computers can extend this in new directions. This throws up some challenging issues regarding representation and interpretation, which I argue can be dealt with by appropriate formalisations. The talk will present examples of formal systems that use diagrams, focusing on my own work - an interactive theorem prover for (a subset of) analysis.

Abstract:

The Mobile Resource Guarantees (MRG) project is developing Proof-Carrying Code technology to endow mobile code with certificates of bounded resource consumption. These certificates should be generated by a compiler which, in addition to translating high-level programs into machine code, derives formal proofs based on programmer annotations and program analysis.

As the basis for reasoning and certificate generation, we employ a program logic for a subset of the JVM, implemented in Isabelle/HOL a' la Nipkow. Although, this has some niceties, such as the soundness and (relative) completeness, which we have formally verified, it proved less suited for concrete program verification, as it required a good deal of user interaction.

We here present a derived logic which is defined on top of the core logic and directly relates to our compile time analysis. It encodes at the JVM level the interpretation of the type system of Hofmann and Jost for heap space consumption. The complexity of the side conditions in the new logic is significantly lower than those in the base logic, making automatic verification feasible. In fact, a fairly naive tactic will solve all the examples we have considered so far.

If time permits, we will demo the whole MRG ``flow'', culminating in certificate generation.

Abstract:

Signalling pathways or networks are found in many biological systems, at a variety of levels, serving many different purposes. In general they are modelled either dynamically, as systems of differential equations, or structurally, for example as graphs, with no formal relation between the models. In this talk I will describe some work which we have been doing modelling a signal transduction network within cells which it thought to to have a role in the development or prevention of tumours. We develop two PEPA models of the network and show that they are bisimilar. The first represents the system as the interaction of protein reactants; the second emphasises the structure of the system as a number of interconnected pathways. I will show how the reactants model can be used to derive differential equations which can be solved to find the dynamic behaviour of reactant concentrations, even though the PEPA models presents only an abstract view of this aspect of the system.

This is joint work with Muffy Calder and Stephen Gilmore.

Abstract:

In this talk I will describe and demonstrate the ACL2 theorem prover. ACL2 stands for "A Computational Logic for Applicative Common Lisp"; ACL2 consists of a functional programming language, a first-order mathematical logic, and a mechanical theorem proving system in the Boyer-Moore tradition, written by Matt Kaufmann and Moore. ACL2 has been used in industry, for example to prove the correspondence between a microarchitecture and an instruction set architecture for a Motorola digital signal processing chip, to prove that the AMD Athon's hardware design for elementary floating point arithmetic is IEEE compliant, and to prove that microcode implementing a separation kernel on the Rockwell Collins AAMP7 insures process isolation. In this talk, I will use elementary examples to illustrate some of ACL2's capabilities and be prepared to answer questions, especially about how ACL2 compares to my earlier theorem provers.

Abstract:

Cynthia is a novel editor for a subset of the functional programming language ML. Each function definition is represented as the proof of a simple specification. Users of Cynthia write ML programs by applying sequences of high-level editing commands to existing programs. The commands make changes to the proof representation, from which a new program is extracted. This use of synthesis proofs provides a sound framework for analysing ML programs and giving useful feedback about errors. Amongst the properties analysed within Cynthia is termination. Reasoning is completely automated, so that it can be hidden from users, who are aware only of the analogy-based editing of programs. This makes it especially suited for teching novice ML programmers. Cynthia has been successfully evaluated in the teaching of two ML courses at Napier University.

This work was completed by Jon Whittle in 1999 for his Edinburgh PhD thesis. It is timely to discuss it now because we are considering teaching functional programming to our Informatics 1 class and Cynthia might find application in this course.

Abstract:

The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about "and" are dual to rules about "or". A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and Curien and Herbelin (2000), has led to the startling conclusion that call-by-value is the de Morgan dual of call-by-name.

This paper presents a dual calculus that corresponds to the classical sequent calculus of Gentzen (1935) in the same way that the lambda calculus of Church (1932,1940) corresponds to the intuitionistic natural deduction of Gentzen (1935). The paper includes crisp formulations of call-by-value and call-by-name that are obviously dual; no similar formulations appear in the literature. The paper gives a CPS translation and its inverse, and shows that the translation is both sound and complete, strengthening a result in Curien and Herbelin (2000).

Abstract:

Confusion between interpretative processes whereby a fragment of language is given an interpretation, and derivational processes whereby conclusions are drawn from an interpretation are rife in the study of human language processing. As a contribution toward untangling these processes, we present a default logical framework which can be shown to model well-known data on the accommodation of interpretation to apparent conflicts in a discourse (the so-called `suppression' task of Byrne 1989).

The logical framework is a `planning logic' which uses logic programming plus negation as failure, augmented with integrity constraints. (This formalism was shown to underlie many semantic computations in natural language in the monograph vL-Hamm, `The proper treatment of events', Blackwell 2004). It will be shown that the observed effects in the suppression task are precisely what one would expect if planning underlies logical reasoning. It can also be shown that this logic, provided it is given the right semantics for negation, has an appealing neural interpretation (the subject of an ANC seminar on 20th April).

Abstract:

We are developing a program logic for reasoning about Standard ML (SML) programs. The logic is inspired by denotational models, but expressed in terms of purely operational concepts. Our work is implemented in Isabelle/HOL so we can experiment with machine checked proof. There is a typeclass of SML types, and HOL equality on SML types is intended to represent observational equivalence. We have started with the functional core language, and plan to add exceptions, then references and I/O to the language. We choose to embed the programming language in HOL (rather than FOL) so as to have a rich language for specifying programs. Using the core, with datatypes of natural numbers and polymorphic lists, we have proved some simple programs correct (a fast Fibonacci function, insertion sort) and verified some more challenging properties of list folding. Our current focus is a uniform treatment of positive recursive datatypes.

Abstract:

I will give an overview of IsaPlanner: a proof planner for encoding and applying reasoning techniques in the generic interactive theorem prover Isabelle. This will start with a brief introduction to proof planning and the IsaPlanner approach which supports interleaving the execution of proof plans with their construction. I will then describe how techniques are encoded, and outline a particularly successful technique for inductive proofs. Finally, I will present some results and a few open questions leading to further work.

Abstract:

The raw material for a computing "fabric" (such as DICE, or a Grid compute farm) consists of bare hardware, and a "repository" of software. The "system configuration" problem involves loading appropriate software onto the machines, and setting the configuration parameters to define the behaviour of individual machines, and the relationships between them.

Currently, configurations tends to be specified at a very low level, and generated manually by skilled staff, from informal specifications of the required high-level fabric behaviour. We would like to automatically generate configuration parameters directly from high-level requirements on the fabric behaviour. This leads to many interesting problems, both in the specification language, and in the tools to deploy and maintain the configurations.

This talk describes the system configuration topic in more detail, and presents several unsolved practical problems relating to automated reasoning.

Abstract:

In this talk I will investigate the use of first-order model building for natural language understanding in practical systems. After outlining several tasks where model building would be useful, I will report on experiments using two state-of-the-art model builders, MACE and PARADOX. The performances of these model builders are acceptable but only applicable for small texts or dialogues. I will suggest several ways for improvement.

Abstract:

A semantic grid is a way of overlaying software components with a specification of the knowledge they contain (describing how it is expressed; and how it may be accessed and manipulated) and using this specification to support automated reasoning about these components (to locate them; configure them; adapt them; coordinate them; etc). The concept of a semantic grid is being explored in parallel by those interested in evolving the existing Worldwide Web and by those starting from the (comparatively) clean sheet of computational grids and multi-agent systems. Some of the theory required for us to build reasoning systems for semantic grids is conventional but the blend of methods and the emphasis on distributed and asynchronous communication assumed by such systems is novel. I shall discuss this, aided by examples from recent research.

Abstract:

Traditionally proofs in interactive theorem provers (e.g. HOL, PVS, Coq, Lego, Isabelle, Nuprl) have been guided by proof scripting languages (e.g. ML). While a proof script for a theorem suffices for automatically generating a proof of that theorem, it serves as a poor account to a human trying to understand the proof.

For this reason, the `Isar mode' proof-script language in the Isabelle system has gained much in popularity recently. This style of script is more declarative and closer to a text-book style than the very operational style of traditional script languages.

I'll briefly survey some of the history of declarative style languages (e.g. with Ontic and Mizar) and discuss why they are not necessarily the way forward. In particular they confuse the issues of generation and presentation, needlessly fix a single level of presentation, and inhibit improvement of automation.

I'll suggest how research in proof scripting languages and support systems should be pushed to overcome these problems yet maintain some of the benefits of a declarative style. Some of the ideas are not new and are present in systems in use today. If time I'll give some demonstrations with Nuprl and PVS to illustrate this.

Abstract:

The theory of non-standard analysis, developed by Robinson in the 1960s, offers a more algebraic way of looking at proof in analysis. We describe some experiments performed in the $\lambda$ Clam proof-planner, designed both to investigate the structure of proof, and the suitability of proof-planning to automate proof in a complex mathematical theory.

Abstract:

Kolmogorov gave a problem-solving calculus that corresponds to intuitionistic logic. Starting from linear logic, I will look at a problem solving calculus that supports aspects of distributed actions. Using Abramsky's computational interpretation of linear logic, this suggests an approach to the synthesis of distributed algorithms.

Abstract:

http://www.proofgeneral.org

Proof General is a generic front-end for interactive proof assistants. It is popular among users of various proof systems, particularly including LEGO, Coq, and Isabelle. The current incarnation of Proof General is built in the text editor Emacs. Several useful facilities are provided for help with developing proof texts interactively, including script management and proof-by-pointing. In this talk I will describe the Proof General project from its start to its present status today. This summer marks a turning point in the project, and I will introduce some of the future plans. (I would particularly like to encourage local users of Proof General to attend to hear about these plans and give feedback).

Abstract:

The development of automated intelligent systems for many real-world problems requires knowledge modelling that entails not only computational efficiency and accuracy, but also user understandability and interpretability. Existing approximate modelling techniques typically overlook the significance of such requirements. In this talk, I shall introduce some of the recent work on flexible descriptive modelling and reasoning, based on an integrated use of rough and fuzzy set theories, that attempts to address these requirements. In particular, the approach allows semantics-preserving feature selection and generalisation of historical data to create explicit knowledge models that can handle imprecise and ill-defined information. To demonstrate the utility of such work I shall present sample application results, drawn from problems such as plant monitoring, e-text categorisation, and biomedical image classification. The talk will conclude by highlighting some potential future developments.

Abstract:

I have been engaged for several years now on a programme of research whose goal is to provide an intuitive and programmer-friendly logic for reasoning about ML programs, together with machine support for doing proofs in such a logic. This research programme currently takes the form of a project involving Mike Fourman, Jacques Fleuriot, Randy Pollack and myself. Besides clarifying the necessary theoretical foundations, the project involves encoding the logic in the Isabelle theorem prover, building infrastructure to support proof construction, and experimenting with the use of proof planning techniques to provide automation for certain kinds of proofs.

In this talk I will give an overview of the general ideas behind this research programme and what I feel is distinctive about our approach. I will also report briefly on where we are up to and on what remains to be done.

Abstract:

The role and status of graphics in argument has always been somewhat fraught, and there are several notions of "graphical proof", as well as claims that no such thing is possible. I shall discuss some of these notions, and support one that treats graphics as a certain kind of notation with an abstract interpretation. This can be related to some of Nelson Goodman's ideas about notations, and also to issues about the conventional nature of proofs and the languages in which they are expressed. Some recent work on the emergence of conventions in graphical communication may help to shed light on the latter.

Abstract:

The general idea of a "name" arises repeatedly across computer science in a variety of forms: as program variables, object identities, communication channels, locations, and other examples from areas like security and distributed systems. Generally, a name is something that has identity, but nothing else. Informal reasoning with names is intuitive and convenient, but it is often hard to match this with formal or mechanical support. In this talk I shall look at various approaches to dealing with this, in particular how some nonstandard set theory recently inspired the programming language FreshML.

Abstract:

The MRG project is building infrastructure for endowing mobile bytecode programs with independently verifiable certificates describing their resource consumption. These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgable. Arbitrarily complex methods may be used to construct such a certificate, but once constructed its verification will always be a simple computation. This makes it feasible for the recipient to check that the proof is valid, and so the claimed property holds, before running the code.

This work falls within an area known as "proof carrying code". Our focus in MRG on quantitative resource guarantees is different from the traditional PCC focus which is security. Another novelty is the method to be used to generate proofs, which is to use a "linear" type system that classifies programs according to their resource usage as well as according to the kinds of values they consume and produce. The intention is to generate proofs of resource usage from typing derivations.

The MRG project (IST-2001-33149), which is a collaboration between Edinburgh University and LMU Munich, is funded by the EC under the FET proactive initiative on Global Computing.

Abstract:

A notable success of Computer Science has been the development of automatic techniques for verifying finite-state systems with direct applications to hardware and finite control. These methods include model-checking, automatic verification of crucial liveness and safety properties, and equivalence checking, showing that two systems exhibit the same behaviour.

The application of these methods to software is more indirect and usually depends on abstracting a potentially infinite-state system into a manageable finite-state system. An alternative approach is to develop automatic techniques that deal directly with infinite-state systems.

Recently, there has been considerable activity in the study of classification and algorithmic properties of infinite-state systems. The hope is that successful algorithmic techniques such as model-checking and equivalence checking can be transferred from finite to classes of infinite-state systems.

I will provide an overview of some work in this general area and of some work that I have done with colleagues.

Abstract:

Automated Question-Answering (QA) has re-emerged as a technology that, in contrast with Information Retrieval, promises users precisely and only the information they are seeking. Technology developed to date has proved surprisingly successful at finding answers to short factual questions and not just the documents in which they can be found.

Nevertheless QA systems have significant problems that could impede further technological development, if unsolved. They include: severe difficulties with (1) recognising answers that are implicit in a text; (2) determining whether some apparently relevant text actually provides an answer to the given question; and (3) assessing whether several potentially relevant texts contain the same or different answers to the given question.

Many leaders in the QA field believe that these and other problems could be solved through the use of inference, by which they mean any way of going from a set of premises and assumptions to needed conclusions.

In this talk, we give a brief overview of current QA, and types of reasoning that can deal with the above problems. We then discuss our interest in whether automated reasoning engines can be used to support QA, either in their current state or with capabilities specifically developed in directions needed for Natural Language Processing.

Abstract:

In this talk I shall give an overview of my ongoing work on the mechanization of continuous mathematics in Isabelle/HOL. I will focus on some of the nonstandard aspects of the development - such as notions of infinite, infinitesimal, and hyperfinite concepts - and describe how these, together with standard notions from real and complex analysis for example, can often be used to produce interesting formal proofs in various areas of mathematics.

Abstract:

In both psychology and artificial intelligence, many prominent researchers believe that intelligence is at least partially modular, but there has been relatively little work unifying the psychological and AI perspectives on modularity. This talk begins with a production-rule model of transitive inference reasoning developed at Edinburgh by Mitch Harris and Brendan McGonigle, and ends with a new theory of the neuroscience of learning. The transition between these points is a relatively simple extension of the Harris and McGonigle model I built as a methodology demonstration while writing my dissertation.

Transitive inference determines that A>B and B>C implies A>C. Harris and McGonigle (1994) provide the best-fitting model of TI to date, particularly taking into account the consequences of providing individuals (in this case, monkeys) with three items to choose between in the test case, rather than the ordinary two. They showed that, if one learns a production-rule stack that can works correctly on all the pairs, TI comes for free. To build a plausible learning model, I split the task into two parallel problems: learning an association between stimuli and actions, and learning an ordering of which stimuli to attend to. The model not only worked, but showed three interesting and unexpected correlates to real biological systems: 1) it could no longer learn TI pairs reliably without the type of training children & monkeys require, 2) when it did learn, its performance was reliable over a larger set of learning parameters than a standard, single-tier neural model of TI, 3) when it failed to learn, it made errors common to real animals.

My model also turns out to be an incredibly simple model of hippocampal learning. If time permits, I will discuss important questions such as the following:

1. How good of a model of the hippocampus is this?
2. How general a model of biological task learning is this?
3. What if production rules really are a good model of natural intelligence? Will we all have to learn Soar?

Abstract:

Even though the software industry is in large need of automatic analysis tools, it currently uses model-checking techniques in a much smaller scale than the hardware industry. One of the main reasons is the fact that model-checking has focused mostly on the analysis of systems with a possibly large but finite state space. While the finiteness constraint is appropriate for hardware, even the simplest software systems may have an infinite state space. The sources of infinity in software systems are multiple. In our group we concentrate on infinities caused by control structures (recursive procedures, process creation) and parametrisation. I'll describe the basic ideas of our approaches and our current research problems.

Abstract:

The goal of this talk is to explain a general issue that is beginning to receive some much overdue attention in the study of human reasoning, and to talk about some recent work exploring this issue in one very particular context. The purpose of the talk is to try to present work in human reasoning in a way that seeks a productive relation to work in logic and theoretical computer science. The particular study I will describe takes Wason's selection task, a continuing scandal in the psychology of reasoning, and seeks to explain the available observations on the basis that subjects' main activity is attempting to reason to an interpretation of the information they are given, rather than from the assumed interpretation. Some general morals for the direction of human reasoning research can be drawn, and some questions raised about the relation between the study of logic and the study of human reasoning. What scope is there for collaboration between the two?

Abstract:

I will give an overview of the work of the Mathematical Reasoning Group. The talk will be pretty high-level but I will pick out a couple of areas for a little more technical detail: proof critics and proof planning for non-standard analysis. Our work covers many aspects of the automation of the processes of mathematical reasoning and its application to formal methods, but has recently focussed on the control of search via proof planning, inductive proof, non-standard analysis and geometry, first-order temporal logic, program synthesis and concept/conjecture formation.

Forthcoming Seminars