Friday 1 July 2005 4 pm 2509 JCMB 
Sean Wilson  Geometry Explorer: Combining Dynamic Geometry, Automated Geometry
Theorem Proving and Diagrammatic Proofs
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, fullangle method prover to produce diagram independent, humanreadable proofs to theorems. Geometry Explorer can then automatically generate novel diagrammatic proofs of the forwardchaining and backwardchaining 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 fullangle method proofs. 
Friday 3 June 2005 4 pm AT 4.03 
David Aspinall  Proof General Kit and PGIP: A Framework for Interactive Proof
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 goaldirected 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. 
Friday 6 May 2005 4 pm JCMB 2509 
Geoff Hamilton  The Poitin Theorem Prover
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. 
Friday 1 April 2005 4 pm JCMB 2509 
Graham Steel  Automated Reasoning with XOR Constraints in Security API Modelling
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. 
Friday 11 February 2005 4 pm Room 4.03 Appleton Tower 
Andrew Ireland  NuSPADE: An Integrated Approach to Program Reasoning
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 runtime 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. 
Friday 14 January 2004 4 pm Room 4.03 Appleton Tower 
John Longley  Towards a new kind of generic theoremprover
Abstract: I will outline some recent ideas on an approach to building a generic theoremprover 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 openended: 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 "highlevel" logic can be definitionally introduced via a translation into a "lowlevel" one; in principle we could either prove the soundness of the highlevel rules once for all, or validate particular instances of the highlevel 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 theoremprover 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 machineassisted theorem proving. 
Friday 3 December 2004 4 pm 2509 JCMB 
Dan Winterstein  Diagrams, Computers and Proof
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. 
Friday 5 November 2004 4 pm 4.03 AT 
Alberto Momigliano and Lennart Beringer  Automatic Certification of Resource Consumption
Abstract: The Mobile Resource Guarantees (MRG) project is developing ProofCarrying 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 highlevel 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. 
Friday 6 August 2004 4 pm 4.03 Appleton Tower 
Jane Hillston  Modelling Biochemical Networks with PEPA
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. 
Friday 23 July 2004 4 pm 4.03 Appleton Tower 
J Strother Moore  A Tutorial Introduction to ACL2
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 firstorder mathematical logic, and a mechanical theorem proving system in the BoyerMoore 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. 
Friday 4 June 2004 4 pm 2509 JCMB 
Alan Bundy  An ML Editor based on Proofs as Programs
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 highlevel 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 analogybased 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. 
Friday 7 May 2004 4 pm 4.03 Appleton Tower 
Philip Wadler  Callbyvalue is dual to callbyname
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 callbyvalue is the de Morgan dual of callbyname. 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 callbyvalue and callbyname 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). 
Friday 16 April 2004 4 pm 2509 JCMB 
Michiel van Lambalgen (Amsterdam) and Keith Stenning (Edinburgh)  What Planning may have to do with Human Reasoning
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 wellknown data on the accommodation of interpretation to apparent conflicts in a discourse (the socalled `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 vLHamm, `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). 
Friday 5 March 2004 4 pm 4.05 Appleton Tower 
Randy Pollack  Reasoning About CBV Functional Programs in Isabelle/HOL
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. 
Friday 6 February 2004 4 pm 2509 JCMB 
Lucas Dixon  An Overview of Proof Planning in Isabelle
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. 
Friday 9 January 2004 4 pm 4.03 Appleton Tower 
Paul Anderson  Automated Reasoning Problems in Large Scale System Configuration
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 highlevel fabric behaviour. We would like to automatically generate configuration parameters directly from highlevel 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. 
Friday 5 December 2003 4 pm Room 4.03, Appleton Tower 
Johan Bos  Exploring Model Building for Natural Language Understanding
Abstract: In this talk I will investigate the use of firstorder 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 stateoftheart 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. 
Friday 7 November 2003 4 pm 2509 JCMB 
Dave Robertson  Reasoning for Semantic Grid Services
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 multiagent 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. 
Friday 10 October 2003 4 pm Appleton Tower 3.06 
Paul Jackson  Readable Formal Proof Languages: A step forward or backward?
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' proofscript language in the Isabelle system has gained much in popularity recently. This style of script is more declarative and closer to a textbook 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. 
Friday 5 September 2003 4 pm 2511 JCMB 
Ewen Maclean  Using ProofPlanning to Investigate the Structure of Proof in
NonStandard Analysis
Abstract: The theory of nonstandard 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 proofplanner, designed both to investigate the structure of proof, and the suitability of proofplanning to automate proof in a complex mathematical theory. 
Friday 1 August 2003 4 pm JCMB 2509 
Alan Smaill  Linear Logic as a ProblemSolving Calculus
Abstract: Kolmogorov gave a problemsolving 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. 
Friday 4 July 2003 4 pm AT 3.04 
David Aspinall  Proof General: the Programmer's Proof Editor
Abstract: http://www.proofgeneral.org Proof General is a generic frontend 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 proofbypointing. 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). 
Friday 6 June 2003 4 pm HCRC Seminar Room, 4BP 
Qiang Shen  Descriptive Knowledge Modelling and Applications
Abstract: The development of automated intelligent systems for many realworld 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 semanticspreserving feature selection and generalisation of historical data to create explicit knowledge models that can handle imprecise and illdefined information. To demonstrate the utility of such work I shall present sample application results, drawn from problems such as plant monitoring, etext categorisation, and biomedical image classification. The talk will conclude by highlighting some potential future developments. 
Friday 2 May 2003 4 pm AT 3.04 
John Longley  Title: A proof system for correctness of ML programs
Abstract: I have been engaged for several years now on a programme of research whose goal is to provide an intuitive and programmerfriendly 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. 
Friday 7 March 2003 4 pm 2509 JCMB 
John Lee  Notation and Convention in Graphical Proof
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. 
Friday 7 February 2003 4 pm HCRC Seminar Room, 4 BP 
Ian Stark  Reasoning with Names
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. 
Friday 17 January 2003 4 pm Room 3.03 Appleton Tower 
Don Sannella  Mobile Resource Guarantees
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 resourcerelated property which are by their very nature selfevident 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 (IST200133149), which is a collaboration between Edinburgh University and LMU Munich, is funded by the EC under the FET proactive initiative on Global Computing. 
Friday 6 December 2002 4 pm HCRC Seminar Room, 4 BP 
Colin Stirling  Taming the Infinite
Abstract: A notable success of Computer Science has been the development of automatic techniques for verifying finitestate systems with direct applications to hardware and finite control. These methods include modelchecking, 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 infinitestate system into a manageable finitestate system. An alternative approach is to develop automatic techniques that deal directly with infinitestate systems. Recently, there has been considerable activity in the study of classification and algorithmic properties of infinitestate systems. The hope is that successful algorithmic techniques such as modelchecking and equivalence checking can be transferred from finite to classes of infinitestate systems. I will provide an overview of some work in this general area and of some work that I have done with colleagues. 
Friday 1 November 2002 4 pm Room 2511 JCMB KB 
Bonnie Webber & Johan Bos  Inference in Question Answering
Abstract: Automated QuestionAnswering (QA) has reemerged 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. 
Friday 6th September 2002 4 pm venue Room 2511, JCMB. 
Jacques Fleuriot  Title: Formalized Continuous Mathematics
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. 
Friday 2nd August 2002 4 pm venue: 2511, JCMB 
Joanna Bryson  Modularity, specialization, and an innate bias for reason.
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 productionrule 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 bestfitting 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 productionrule 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, singletier 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:

Friday 5th July 2002 4 pm Room F13, 80 South Bridge 
Javier Esparza  ModelChecking Infinite State Systems
Abstract: Even though the software industry is in large need of automatic analysis tools, it currently uses modelchecking techniques in a much smaller scale than the hardware industry. One of the main reasons is the fact that modelchecking 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. 
Friday 7th June 2002 4 pm Room 2511, JCMB. 
Keith Stenning  Reasoning to an interpretation vs. from an interpretation: the
balance in human reasoning
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? 
Friday 3rd May 2002 4 pm Conference Suite, 4 Buccleuch Place. 
Alan Bundy  The Work of the Mathematical Reasoning Group
Abstract: I will give an overview of the work of the Mathematical Reasoning Group. The talk will be pretty highlevel but I will pick out a couple of areas for a little more technical detail: proof critics and proof planning for nonstandard 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, nonstandard analysis and geometry, firstorder temporal logic, program synthesis and concept/conjecture formation. 
Forthcoming Seminars 
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, Email: schooloffice@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 