Deductive Synthesis of Workflows for e-Science (2009)
Bin Yang, Alan Bundy, Alan Smaill, Lucas Dixon
In this paper we show that the automated reasoning technique of deductive synthesis can be applied to address the problem of machine-assisted composition of e-Science workflows according to users ’...
A Comparison of Two Proof Critics: Power vs. Robustness (2009)
Abstract. Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow...
Lin Yang, Alan Bundy, Dave Berry, Conrad Hughes
National e-Science Centre Workflows are playing a crucial role in e-Science systems. In many cases, e-Scientists need to do average case estimates of the performance of workflows. Quality of Service...
The Method of Assigning Incidences (2008)
Weiru Liu, David Mcbryan, Alan Bundy
Incidence calculus is a probabilistic logic in which incidences, standing for the situations in which formulae may be true, are assigned to some formulae, and probabilities are assigned to...
Abstract Best-First Rippling (2008)
Moa Johansson, Alan Bundy, Lucas Dixon
Rippling is a form of rewriting that guides search by only performing steps that reduce the syntactic differences between formulae. Termination is normally ensured by a measure that is decreases with...
2006, ‘Planning as Deductive Synthesis in Intuitionistic Linear Logic (2008)
Lucas Dixon, Alan Smaill, Alan Bundy
Isabelle/HOL of Intuitionistic Linear Logic and consider the support this provides for constructing plans using deductive synthesis of the proof terms. This representation of plans in linear logic...
The Annual Boole Lecture was established and is sponsored by the Boole Centre for Research in (2008)
seminal work on logic in the mid-1800s is central to modern digital computing. To mark this great contribution, leaders in the field of computing and mathematics are invited to talk to the general...
Searching for a Solution to Program Verification=Equation Solving in CCS ⋆ (2008)
Raúl Monroy, Alan Bundy, Ian Green
Abstract. Unique Fixpoint Induction, UFI, is a chief inference rule to prove the equivalence of recursive processes in CCS [7]. It plays a major role in the equational approach to verification. This...
Proof Critics for IsaPlanner (2008)
Moa Johansson, Lucas Dixon, Alan Bundy
The discovery of missing lemmas and case-splits are challenging problems for automated theorem proving. Most interactive provers rely on the user for guidance through these proof-steps....
Roy Mccasl, Alan Bundy, Serge Autexier
Abstract. Inductive mathematical theorems have, as a rule, historically been quite difficult to prove – both for mathematics students and for automated theorem provers. That said, there has been...
Mandy Lupton Australian National University (2008)
Alan Bundy, Debbie Orr, Central Queensl, Alan Bundy
The Australian and New Zealand information literacy framework may be freely used, translated, and adapted for noncommercial purposes, subject to acknowledgment of its US and Australasian provenance....
Moa Johansson, Alan Bundy, Lucas Dixon
Abstract. Rippling is a form of rewriting that guides search by only performing steps that reduce the differences between formulae. Termination is normally ensured by a defined measure that is...
Automated Discovery in Pure Mathematics (2008)
Simon Colton, Alan Bundy, Toby Walsh
The HR project aims to automate two important discovery processes which occur in mathematics before theorem proving happens, namely the making of the conjecture to be proved and the invention of the...
Computing and Social Responsibility Group for feedback (2008)
Alan Bundy, Richard Clutterbuck
We propose a mechanism for the promotion of high-standards in commercial Artificial Intelligence products, namely an association of companies which would regulate their own membership using a code of...
Cooperating Reasoning Processes: More than just the Sum of their Parts ∗ (2008)
Bernard Silver, Julian Richardson, Alan Smaill, Andrew Stevens, Alan Bundy
Using the achievements of my research group over the last 30+ years, I provide evidence to support the following hypothesis: By complementing each other, cooperating reasoning process can achieve...
Frank Van Harmelen, Alan Bundy, Frank Van Harmelen, Alan Bundy
Explanation-based generalisation
REPRESENTING SEMANTIC INFORMATION IN PULLEY PROBLEMS (2008)
Several recent research reports have focussed on the representation and solution of problems in semantically rich domains (1),(2),(3),(4). These include analysis of algebra word problems as well as...
Simon Colton, Alan Bundy, Toby Walsh
We survey five mathematical discovery programs by looking in detail at the discovery processes they illustrate and the success they’ve had. We focus on how they estimate the interestingness of...
Mathematical Reasoning Group (2008)
Simon Colton, Alan Bundy, South Bridge
We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically inventing integer sequences. Seventeen sequences invented by HR are interesting enough...
Proof by mathematical induction plays a crucial role in reasoning about functional programs. A generalization step often holds the key to discovering an inductive proof. We present a generalization...
Proof Planning the Verification of CCS Programs (2007)
Raul Monroy, Alan Bundy, Andrew Ireland, Jane Hesketh
. The verification of CCS programs has often been characterised as an expensive, time-consuming, and error-prone task, where computer assistance is thought to be essential. Yet, existing theorem...
Alan Bundy, Ben Du Boulay, Ben Du Boulay, Jim Howe, Jim Howe, ...
ion : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8 3.9 Ambitious Paralysis : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 8 3.10 Methodology does not make a thesis :...
A Prototype Interface between (2007)
Clam And Hol, Richard Boulton, Alan Bundy, Konrad Slind, Mike Gordon
This paper describes a prototype interface between the CLaM proof planner and the HOL interactive theorem prover. CLaM uses artificial intelligence planning techniques to find proofs at a high-level,...
The Termination of Rippling + Unblocking (2007)
. Rippling is a heuristic technique for guiding rewriting of a goal with respect to one or more givens. Rewriting is restricted so that the similarities between goal and given are preserved and the...
Observant: an Annotated Term-Rewriting System for Deciding Observation Congruence (2007)
Raúl Monroy, Alan Bundy, Ian Green
The use of term-rewriting systems (TRSs) is at the core of automated theorem proving (ATP). There are a number of methods whereby we can build terminating TRSs with full deduction power, with respect...
System Description CyNTHIA (2007)
Jon Whittle, Alan Bundy, Richard Boulton, Helen Lowe
This paper describes ways of using proofs as a foundation to improve the situation, in the context of the language ML [4]. The most common way to write ML programs is via a text editor and compiler...
Roger Needham, Roger Needham, Martín Abadi, Ross Anderson, Jean Bacon, Andrew Birrell, ...
comprising in this compilation are copyright of the respective authors. All rights are reserved. This publication may not be copied, reproduced, published or distributed in whole or in part in any...
Steven Willmott, Julian Richardson, Alan Bundy, John Levine
Approaches to computer game playing based on ff \Gamma fi search of the tree of possible move sequences combined with a position evaluation function have been successful for many games, notably...
Using Implicit Induction to Guide a Parallel Search for Inconsistency (2007)
Graham Steel, Alan Bundy, Ewen Denney
We describe the first full implementation of the Comon-Nieuwenhuis method for implicit induction, including a consistency checker, in a novel system where the proof and refutation programs...
Mathematical Reasoning Group (2007)
Simon Colton, Alan Bundy, Toby Walsh
We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically inventing integer sequences. Seventeen sequences invented by HR are interesting enough...
Mathematical Reasoning Group (2007)
Simon Colton, Alan Bundy, South Bridge
We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically inventing integer sequences. Seventeen sequences invented by HR are interesting enough...
Mathematical Reasoning Group (2007)
Simon Colton, Alan Bundy, Toby Walsh
We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically inventing integer sequences. Seventeen sequences invented by HR are interesting enough...
Inductive Proof Plans for the Correction of Faulty Software Specifications (2007)
Raul Monroy, Supervisors Professor, Alan Bundy, Dr. Andrew Irel, Dr. Jane Hesketh
According to [Liskov & Berzins 79], "every program performs some task correctly " and hence meets, at least, one specification. However, not every specification is satisfiable....
Computing Abstraction Hierarchies by Numerical Simulation (2007)
Bundy A, Giunchiglia F, Sebastiani R, Walsh T, Alan Bundy, Fausto Giunchiglia, ...
istituto per la ricerca scientifica e tecnologica
A. Bundy, F. Giunchiglia, T. Walsh, Alan Bundy, Fausto Giunchiglia, Toby Walsh
The use of abstraction has been largely informal. As a consequence, it has often been difficult to see how or why a particular abstraction works. This paper attempts to help correct this trend by...
Automated Discovery in Pure Mathematics (2007)
Simon Colton, Alan Bundy, Toby Walsh
The HR project aims to automate two important discovery processes which occur in mathematics before theorem proving happens, namely the making of the conjecture to be proved and the invention of the...
Steven Willmott, Julian Richardson, Alan Bundy, John Levine
Approaches to computer game playing based on ff \Gamma fi search of the tree of possible move sequences combined with a position evaluation function have been successful for many games, notably...
Part I: Previous research track record (2007)
Alan Bundy, Johanna Moore, Claus Zinn
Prof. Alan Bundy was educated as a Mathematician, obtaining a 1st class honours degree in Mathematics in 1968 from Leicester University and a PhD in Mathematical Logic in 1971, also from Leicester,...
Jon Whittle, Alan Bundy, Richard Boulton, Helen Lowe
Abstract. C Y NTHIA is a novel editor for the functional programming language ML in which each function definition is represented as the proof of a simple specification. Users of C Y NTHIA edit...
Daniel Winterstein, Alan Bundy, Mateja Jamnik
Abstract. This paper presents one approach to the formalisation of diagrammatic proofs as an alternative to algebraic logic. An idea of `generic diagrams ' is developed whereby one diagram (or...
An Editor for Helping Novices to Learn (2007)
Standard Ml Jon, Jon Whittle, Alan Bundy, Helen Lowe
This paper describes a novel editor intended as an aid in the learning of the functional programming language Standard ML. A common technique used by novices is programming by analogy whereby...
The Method of Assigning Incidences (2007)
Weiru Liu, David Mcbryan, Alan Bundy
Incidence calculus is a probabilistic logic in which incidences, standing for the situations in which formulae may be true, are assigned to some formulae, and probabilities are assigned to...
Semi-Automated Discovery in Zariski Spaces (A Proposal) (2007)
Zariski Spaces were introduced in 1998 [MMS98]. In order to understand these spaces, one needs to rst understand Zariski Topologies. In a broad sense, these topologies are rather like prime...
Steven Willmott, Julian Richardson, Alan Bundy, John Levine
Approaches to computer game playing based on (typically ) search of the tree of possible move sequences combined with an evaluation function have been successful for many games, notably Chess. For...
A. Arm, J. Gallagher, A. Smaill, A. Bundy, Alessandro Armando, Jason Gallagher, ...
Automating the synthesis of decision procedures in a
Supervisors Prof, Alan Bundy, Dr. Graham Steel
The proof planning systems available today are sequential systems. The hypothesis of this project is that the engineering of a proof planning system that is capable of dynamic, distributed, parallel...
OpenKnowledge ⋆ Deliverable 3.1.: Dynamic Ontology Matching: a Survey (2006)
Pavel Shvaiko, Fausto Giunchiglia, Marco Schorlemmer, Fiona Mcneill, Alan Bundy, Maurizio Marchese, ...
Abstract. Matching has been recognized as a plausible solution for the semantic heterogeneity problem in many traditional applications, such as schema integration, ontology integration, data...
On Repairing Reasoning Reversals via Representational Refinements (2006)
Alan Bundy Fiona, Alan Bundy, Fiona Mcneill, Chris Walton
Representation is a fluent. A mismatch between the real world and an agent's representation of it can be signalled by unexpected failures (or successes) of the agent's reasoning.
A Very Mathematical Dilemma (2006)
The Annual Boole Lecture was established and is sponsored by the Boole Centre for Research in Informatics, the Cork Constraint Computation Centre, the Department of Computer Science, and the School...
Alan Bundy, Mateja Jamnik, Andrew Fugard
To those brought up in a logic-based tradition there seems to be a simple and clear definition of proof. But this is largely a 20 th century invention; many earlier proofs had a different nature. We...
Using ontologies for planning tourist visits 52 (2005)
Juan Fernández Olivares, Eva Onaindía, Susanne Biundo, Karen Myers, Kanna Rajan, Juan Fernández Olivares, ...
Table of contents
Attacking Group Protocols (2005)
Automated tools for finding attacks on flawed security protocols often fail to deal adequately with group protocols. This is because the abstractions made to improve performance on fixed 2 or 3 party...
Deduction with XOR Constraints In Security API Modelling (2005)
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...
Constructing induction rules for deductive synthesis proofs (2005)
Alan Bundy, Lucas Dixon, Jeremy Gow, Jacques Fleuriot
We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer...
Places of connection : new public and academic library buildings in Australia and New Zealand (2004)
English summaries of mathematical proofs (2004)
Marianthi Alexoudi, Claus Zinn, Alan Bundy
Automated theorem proving is becoming more important as the volume of applications in industrial and practical research areas increases. Due to the formalism of theorem provers and the massive amount...
Planning and patching proof; in (2004)
Abstract. We describe proof planning: a technique for both describing the hierarchical structure of proofs and then using this structure to guide proof attempts. When such a proof attempt fails,...
The Researcher's Bible The Researcher's Bible (2004)
Alan Bundy, Ben Du Boulay, Jim Howe, Gordon Plotkin, Peter Ross
Getting a Ph.D. or M.Phil is hard work. This document gives advice about various aspects of the task. Section 1 describes the problem- what is a thesis? Sections 2 and 3 describe some of the pitfalls...
Dr.Doodle: A Diagrammatic Theorem Prover (2004)
Daniel Winterstein Alan, Alan Bundy, Corin Gurr
This paper presents the Dr.Doodle system, an interactive theorem prover that uses diagrammatic representations. The assumption underlying this project is that, for some domains (principally geometry)...
Attacking a protocol for group key agreement by refuting incorrect inductive conjectures (2004)
Graham Steel, Alan Bundy, Monika Maidl
Abstract. Automated tools for finding attacks on flawed security protocols often struggle to deal with protocols for group key agreement. Systems designed for fixed 2 or 3 party protocols may not be...
Places of connection : new public and academic library buildings in Australia and New Zealand (2004)
Places of connection : new public and academic library buildings in Australia and New Zealand (2004)
This second edition of the 2001 Information literacy standards is entitled the Australian and New Zealand information literacy framework: principles, standards and practice to reflect the ways...
Only connect : towards the information enabling of young Australians (2003)
One of the few certainties about the 21st century is that it will be a century of the mind characterised by information abundance. Realising a vision of Australia as an information enabled nation...
This second edition of the 2001 Information literacy standards is entitled the Australian and New Zealand information literacy framework: principles, standards and practice to reflect the ways...
Formalising the Grid Environment (2003)
The St Step, Alan Bundy, Alan Smaill, Bin Yang
In the emerging e-Science, a Grid computing environment is coming into shape. However, the features of "rapid customised assembly of services" and "autonomic computing" have yet...
Constructing Probabilistic ATMS Using Extended Incidence Calculus (2003)
This paper discusses the relations between extended incidence calculus and assumption-based truth maintenance systems (ATMSs). We rst prove that managing labels for statements (nodes) in an ATMS is...
On differences between the real and physical Plane: Analysis of the inside relation (2003)
Daniel Winterstein, Daniel Winterstein, Daniel Winterstein, Supervisors Prof, Alan Bundy, Dr. Corin Gurr
inside relation by
Only connect : towards the information enabling of young Australians (2003)
One of the few certainties about the 21st century is that it will be a century of the mind characterised by information abundance. Realising a vision of Australia as an information enabled nation...
Only connect : towards the information enabling of young Australians (2003)
One of the few certainties about the 21st century is that it will be a century of the mind characterised by information abundance. Realising a vision of Australia as an information enabled nation...
The applicants are members of the Mathematical Reasoning Group (mrg), which is part of the Centre for Intelligent Systems and their Applications within the Division of Informatics at the University...
Finding counterexamples to inductive conjectures and discovering security protocol attacks (2002)
Graham Steel, Alan Bundy, Ewen Denney
We present an implementation of a method for finding counterexamples to universally quantified conjectures in first-order logic. Our method uses the proof by consistency strategy to guide a search...
Automated Theory Formation for Tutoring Tasks in Pure Mathematics (2002)
Simon Colton, Roy McCasland, Alan Bundy, Toby Walsh
The HR program forms mathematical theories from as little information as the axioms of a domain. The theories include concepts with examples and de nitions, conjectures, theorems and proofs....
Automated theory formation for tutoring tasks in pure mathematics (2002)
Simon Colton, Roy Mccasl, Alan Bundy, Toby Walsh, Cork Constraint, Computation Centre
A Comparison of two Proof Critics: Power vs. Robustness (2002)
Dennis, Louise Abigail, Bundy, Alan
Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow the proof to...
Centre for Intelligent Systems and their Applications (2001)
Steven Willmott, Julian Richardson, Alan Bundy, John Levine, Steven Willmott, Julian Richardson, ...
Applying adversarial planning techniques to Go
Strict General Setting for Building Decision Procedures into Theorem Provers (2001)
The efficient and flexible incorporating of decision procedures into theorem provers is very important for their successful use. There are several approaches for combining and augmenting of decision...
The main issue of the so called information age is still being given scant systematic attention. Even if they recognise their need for information, people often lack the understandings and skills to...
Libraries a living force (2000)
Australia has one of the most accessible and heavily used public library networks in the world. However from a July 2000 survey, much needs to be done in the 21st century to highlight and address...
Library statistics have two main purposes, for internal management and interlibrary benchmarking, and for advocacy for better funded libraries. Australian library statistics are deficient, especially...
Information literacy : the foundation of lifelong learning (2000)
Most Australian adults, and many school students, lack the information literacy to transform information into knowledge and wisdom. Information technology is no educational panacea, but much funding...
Combining Knowledge and Search to Solve Single-suit Bridge (2000)
Ian Frank, David Basin, Alan Bundy
In problem solving, it is often important not only to nd a solution but also to be able to explain it. We use the game of Bridge to illustrate how tactics, which formalise domain-specic expertise,...
Cross-domain Mathematical Concept Formation (2000)
Graham Steel, Simon Colton, Alan Bundy, Toby Walsh
Many interesting concepts in mathematics are essentially `cross-domain' in nature, relating objects from more than one area of mathematics, e.g. prime order groups. These concepts are often...
Solving Single-suit Bridge Play: Winning and Knowing Why (2000)
Ian Frank, David Basin, Alan Bundy
In problem solving, it is often important not only to nd a solution but also to be able to explain it. We use the game of Bridge to illustrate how tactics, which formalise domain specic expertise,...
On the Notion of Interestingness in Automated Mathematical Discovery (2000)
Simon Colton, Alan Bundy, Toby Walsh
We survey ve mathematical discovery programs by looking in detail at the discovery processes they illustrate and the success they've had. We focus on how they estimate the interestingness of...
A Recursive Techniques Editor for Prolog (2000)
Alan Bundy, Gerd Grosse, Paul Brna
We describe an editor geared to recursive Prolog procedures. It is similar to the structure editors built for many programming languages, except that instead of just ensuring the correctness of the...
Automatic Invention of Integer Sequences (2000)
Simon Colton Alan, Alan Bundy, Toby Walsh
We report on the application of the HR program (Colton, Bundy, & Walsh 1999) to the problem of automatically inventing integer sequences. Seventeen sequences invented by HR are interesting enough...
On the notion of interestingness in automated mathematical discovery (2000)
We survey five automated discovery programs working in mathematics, by looking in detail at the discovery processes they illustrate, summarising the successes they’ve had and by focusing on how...
Cross domain mathematical concept formation (2000)
Graham Steel, Simon Colton, Alan Bundy, Toby Walsh
Many interesting concepts in mathematics are essentially ‘cross-domain ’ in nature, relating objects from more than one area of mathematics, e.g. prime order groups. These concepts are often...
Agent based cooperative theory formation in pure mathematics (2000)
Simon Colton, Alan Bundy, Toby Walsh
The HR program, Colton et al. (1999), performs theory formation in domains of pure mathematics. Given only minimal information about a domain, it invents concepts, make conjectures, proves theorems...
On the notion of interestingness in automated mathematical discovery (2000)
Deciding whether something is interesting or not is of central importance in automated mathematical discovery, as it helps determine both the search space and search strategy for finding and...
Dennis, Louise Abigail, Bundy, Alan, Green, Ian
Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about...
The main issue of the so called information age is still being given scant systematic attention. Even if they recognise their need for information, people often lack the understandings and skills to...
Libraries a living force (2000)
Australia has one of the most accessible and heavily used public library networks in the world. However from a July 2000 survey, much needs to be done in the 21st century to highlight and address...
Library statistics have two main purposes, for internal management and interlibrary benchmarking, and for advocacy for better funded libraries. Australian library statistics are deficient, especially...
Information literacy : the foundation of lifelong learning (2000)
Most Australian adults, and many school students, lack the information literacy to transform information into knowledge and wisdom. Information technology is no educational panacea, but much funding...
The main issue of the so called information age is still being given scant systematic attention. Even if they recognise their need for information, people often lack the understandings and skills to...
Information literacy : the foundation of lifelong learning (2000)
Most Australian adults, and many school students, lack the information literacy to transform information into knowledge and wisdom. Information technology is no educational panacea, but much funding...
Library statistics have two main purposes, for internal management and interlibrary benchmarking, and for advocacy for better funded libraries. Australian library statistics are deficient, especially...
Libraries a living force (2000)
Australia has one of the most accessible and heavily used public library networks in the world. However from a July 2000 survey, much needs to be done in the 21st century to highlight and address...
A partner in learning and research : the hybrid university library of the 21st century (1999)
This paper reviews issues facing university education into the next century as the context for commentary on the type of library and Librarians which will be required so that effective teaching,...
Alan Bundy, Alan Bundy, Alan Bundy
To appear in the ”Handbook of Automated Reasoning” Abstract: This paper is a chapter of the Handbook of Automated Reasoning edited by Voronkov and Robinson. It describes techniques for automated...
Extensions to the estimation calculus (1999)
Jeremy Gow, Jeremy Gow, Jeremy Gow, Alan Bundy, Alan Bundy, Alan Bundy, ...
Walther’s estimation calculus was designed to prove the termination of functional programs, and can also be used to solve the similar problem of proving the well-foundedness of induction rules....
Predrag Janicic, Predrag Janicic, Alan Bundy, Alan Bundy, Ian Green, Ian Green
The role of decision procedures is often essential in theorem proving. Decision procedures can reduce the search space of heuristic components of a prover and increase its abilities. However, in some...
A survey of automated deduction (1999)
Alan Bundy, Alan Bundy, Alan Bundy
Abstract: We survey research in the automation of deductive inference, from its beginnings in the early history of computing to the present day. We identify and describe the major areas of research...
Proofs about lists using ellipsis (1999)
Abstract. In this paper we explore the use of ellipsis in proofs about lists. We present a higher-order formulation of elliptic formulae, and describe its implementation in the λClam proof planner....
Proofs about lists using ellipsis (1999)
Abstract. In this paper we explore the use of ellipsis in proofs about lists. We present a higher-order formulation of elliptic formulae, and describe its implementation in the Clam proof planner. We...
A survey of automated deduction (1999)
Alan Bundy, Alan Bundy, Alan Bundy
Abstract: We survey research in the automation of deductive inference, from its beginnings in the early history of computing to the present day. We identify and describe the major areas of research...
Recursive Program Optimization Through Inductive Synthesis Proof Transformation (1999)
Peter Madden, Alan Bundy, Alan Smaill
The research described in this paper involved developing transformation techniques which increase the efficiency of the noriginal program, the source, by transforming its synthesis proof into one,...
Automatic Concept Formation in Pure Mathematics (1999)
Simon Colton And, Simon Colton, Alan Bundy, Toby Walsh
The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties...
An Adversarial Planning Approach to Go (1999)
Steven Willmott, Julian Richardson, Alan Bundy, John Levine
. Approaches to computer game playing based on (typically #-#) search of the tree of possible move sequences combined with an evaluation function have been successful for many games, notably Chess....
Extensions to the Estimation Calculus (1999)
Jeremy Gow, Alan Bundy, Ian Green
. Walther's estimation calculus was designed to prove the termination of functional programs, and can also be used to solve the similar problem of proving the well-foundedness of induction...
On Automating Diagrammatic Proofs of Arithmetic Arguments (1999)
Mateja Jamnik, Alan Bundy, Ian Green
. Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so...
An ML Editor Based on Proofs-as-Programs (1999)
Jon Whittle, Recom Technologies, Alan Bundy, Richard Boulton, Helen Lowe
C Y NTHIA is a novel editor for the functional programming language ML in which each function definition is represented as the proof of a simple specification. Users of C Y NTHIA edit programs by...
A Survey of Automated Deduction (1999)
We survey research in the automation of deductive inference, from its beginnings in the early history of computing to the present day. We identify and describe the major areas of research interest...
Automatic Verification of Functions with Accumulating Parameters (1999)
Proof by mathematical induction plays a crucial role in the verification of program transformations. This paper focuses on the automatic verification of transformations which introduce accumulating...
Extensions to the Estimation Calculus (1999)
Jeremy Gow, Alan Bundy, Ian Green
. Walther's estimation calculus was designed to prove the termination of functional programs, and can also be used to solve the similar problem of proving the well-foundedness of induction...
Automatic Concept Formation in Pure Mathematics (1999)
The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties...
Proof Planning Methods as Schemas (1999)
A major problem in automated theorem proving is search control. Many expanded proofs are generally built from a large number of relatively low-level inference steps, with the results that searching...
Automatic Verification of Functions with Accumulating Parameters (1999)
Proof by mathematical induction plays a crucial role in the verification of program transformations. This paper focuses on the automatic verification of transformations which introduce accumulating...
Proofs About Lists Using Ellipsis (1999)
Alan Bundy And, Alan Bundy, Julian Richardson
In this paper we explore the use of ellipsis in proofs about lists. We present a higher-order formulation of elliptic formulae, and describe its implementation in the Clam proof planner. We use an...
Using a Generalisation Critic to find Bisimulations for Coinductive Proofs (1999)
Dennis, Louise Abigail, Bundy, Alan, Green, Ian
Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that...
A partner in learning and research : the hybrid university library of the 21st century (1999)
This paper reviews issues facing university education into the next century as the context for commentary on the type of library and Librarians which will be required so that effective teaching,...
A partner in learning and research : the hybrid university library of the 21st century (1999)
This paper reviews issues facing university education into the next century as the context for commentary on the type of library and Librarians which will be required so that effective teaching,...
Lightweight formalisation in support of requirements engineering (1998)
Jane Hesketh, David Robertson, Norbert Fuchs, Alan Bundy
Formal design supported by automated reasoning can help keep track of requirements- a particular problem for large, detailed systems. Designers of system specifications are often constrained by codes...
HR - A System for Machine Discovery in Finite Algebras (1998)
Alan Bundy, Simon Colton, Toby Walsh
We describe the HR concept formation program which invents mathematical definitions and conjectures in finite algebras such as group theory and ring theory. We give the methods behind and the reasons...
Verification of Diagrammatic Proofs (1998)
Mateja Jamnik, Alan Bundy, Ian Green
Human mathematicians often "prove" theorems by the use of diagrams and manipulations on them. We call these diagrammatic proofs. In (Jamnik, Bundy, & Green 1997) we presented how...
Adversarial Planning in Complex Domains (1998)
Steven Willmott, Alan Bundy, John Levine, Julian Richardson
. Most current planning research relies on the assumption of a benign domain containing only co-operative agents. There has been little work on applying modern planning techniques to adversarial...
On Automating Diagrammatic Proofs of Arithmetic Arguments (1998)
Mateja Jamnik Alan, Alan Bundy, Ian Green
. Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so...
System Description: An Interface between CLaM and HOL (1998)
Konrad Slind, Mike Gordon, Richard Boulton, Alan Bundy
. The CLaM proof planner has been interfaced to the HOL interactive theorem prover to provide the power of proof planning to people using HOL for formal verification, etc. The interface sends HOL...
Proof Planning for Maintainable Configuration Systems (1998)
Michal Pechoucek, Alan Bundy, Helen Lowe, Helen Lowe
Configuration is a complex task generally involving varying measures of constraint satisfaction, optimization, and the management of soft constraints. Although many successful systems have been...
HR: A System for Machine Discovery in Finite Algebras (1998)
Abstract. We describe the HR concept formation program which invents mathematical definitions and conjectures in finite algebras such as group theory and ring theory. We give the methods behind and...
A comparison of decision procedures (1997)
Predrag Janicic, Alan Bundy, Predrag Janicic, Alan Bundy
The efficient combining and augmenting of decision procedures are often very important for a successful use of theorem provers. There are several schemes for combining and augmenting decision...
Supporting programming by analogy in the learning of functional programming languages (1997)
Jon Whittle, Alan Bundy, Helen Lowe
This paper examines the learning of the functional programming language Standard ML. A common technique used by novices is programming by analogy whereby students refer to similar programs that they...
The Use of Classification in Automated Mathematical Concept Formation (1997)
Simon Colton Stephen, Stephen Cresswell, Alan Bundy
Concept formation programs aim to produce a high yield of concepts which are considered interesting. One intelligent way to do this is to base a new concept on one or more concepts which are already...
Automation of Diagrammatic Reasoning (1997)
Mateja Jamnik, Alan Bundy, Ian Green
Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations...
Supporting Programming by Analogy in the Learning of Functional Programming Languages (1997)
Jon Whittle, Alan Bundy, Helen Lowe
This paper examines the difficulties in learning new programming languages and addresses ways to overcome these difficulties. In particular, we concentrate on the functional programming language ML....
Automation of Diagrammatic Reasoning (1997)
Mateja Jamnik Alan, Alan Bundy, Ian Green
Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations...
A comparison of decision procedures in Presburger arithmetic (1997)
Predrag Janicic, Ian Green, Alan Bundy
It is part of the tradition and folklore of automated reasoning that the intractability of Cooper's decision procedure for Presburger integer arithmetic makes is too expensive for practical use....
Using a Generalisation Critic to Find Bisimulations for Coinductive Proofs (1997)
Louise Dennis, Louise Dennis, Alan Bundy, Alan Bundy, Alan Bundy, ...
Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that...
An Editor for Helping Novices to Learn Standard ML (1997)
Jon Whittle, Alan Bundy, Helen Lowe
This paper describes a novel editor intended as an aid in the learning of the functional programming language Standard ML. A common technique used by novices is programming by analogy whereby...
The use of classification in automated mathematical concept formation (1997)
Simon Colton, Stephen Cresswell, Alan Bundy
Concept formation programs aim to produce a high yield of concepts which are considered interesting. One intelligent way to do this is to base a new concept on one or more concepts which are already...
Productive use of failure in inductive proof (1996)
Proof by mathematical induction gives rise to various kinds of eureka steps, e.g. missing lemmata, generalization, etc. Most inductive theorem provers rely upon user intervention in supplying the...
Computing Abstraction Hierarchies by Numerical Simulation (1996)
Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh
ion Hierarchies by Numerical Simulation Alan Bundy Dept of AI University of Edinburgh Fausto Giunchiglia IRST, Trento and University of Trento Roberto Sebastiani DIST University of Genoa Toby Walsh...
Automation of Diagrammatic Proofs in Mathematics (1996)
Mateja Jamnik, Alan Bundy, Ian Green
Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which can also be proved in a more informal way by the use of geometric...
Extensions to a Generalization Critic for Inductive Proof (1996)
In earlier papers a critic for automatically generalizing conjectures in the context of failed inductive proofs was presented. The critic exploits the partial success of the search control heuristic...
Alan Bundy January, Alan Bundy
We describe proof planning, a technique for the global control of search in automatic theorem proving. A proof plan captures the common patterns of reasoning in a family of similar proofs and is used...
Planning and Proof Planning (1996)
. The paper adresses proof planning as a specific AI planning. It describes some peculiarities of proof planning and discusses some possible cross-fertilization of planning and proof planning. 1...
An experimental comparison of rippling and exhaustive rewriting (1996)
We compare rippling and exhaustive rewriting using recursive path ordering, on a range of inductive proofs. We present statistics on success rates, branching rates and CPU times. We use these...
Experiments in Automating Hardware Verification using Inductive Proof Planning (1996)
Francisco Cantu Alan, Alan Bundy, Alan Smaill
We present a new approach to automating the verification of hardware designs based on planning techniques. A database of methods is developed that combines tactics, which construct proofs, using...
Automating the Synthesis of Decision Procedures in a Constructive Metatheory (1996)
Alessandro Armando Jason, Jason Gallagher, Alan Smaill, Alan Bundy
this paper we identify a set of principled extensions to the heuristics for
Proof Planning & Configuration (1996)
Helen Lowe, Michal Pechoucek, Alan Bundy
This paper presents two configuration problems: that of configuring computer hardware to meet a given specification, and an "engineer-and-made-to-order" problem in the domain of breathing...
An Incompleteness Theorem via Abstraction (1996)
Alan Bundy, Fausto Giunchiglia, Adolfo Villafiorita, Toby Walsh
ion Alan Bundy 1 , Fausto Giunchiglia 2;3 , Adolfo Villafiorita 4;5 and Toby Walsh 2;5 1. Mathematical Reasoning Group, Dept of AI, University of Edinburgh 2. Mechanized Reasoning Group, IRST 3....
Experiments in Automating Hardware Verification using Inductive Proof Planning (1996)
Francisco J. Cantu, Alan Bundy, Alan Smaill, David Basin
. We present a new approach to automating the verification of hardware designs based on planning techniques. A database of methods is developed that combines tactics, which construct proofs, using...
Relational rippling: A general approach (1995)
We propose a new version of rippling, called relational rippling. Rippling is a heuristic for guiding proof search, especially in the step cases of inductive proofs. Relational rippling is designed...
The Automation of Proof by Mathematical Induction (1995)
Contents 1. Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 1.1. Explicit vs...
Relational Rippling: A General Approach (1995)
Vincent Lombart Alan, Alan Bundy
We propose a new version of rippling, called relational rippling. Rippling is a heuristic for guiding proof search, especially in the step cases of inductive proofs. Relational rippling is designed...
Middle-Out Reasoning for Synthesis and Induction (1995)
Ina Kraan, David Basin, Alan Bundy
We develop two applications of middle-out reasoning in inductive proofs: Logic program synthesis and the selection of induction schemes. Middleout reasoning as part of proof planning was first...
Relational Rippling: A General Approach (1995)
We propose a new version of rippling, called relational rippling. Rippling is a heuristic for guiding proof search, especially in the step cases of inductive proofs. Relational rippling is designed...
Automatic Guidance of Mechanically Generated Proofs (1995)
13> Mollusc is a generic proof editor. By defining a logic in it, Mollusc is instantiated into a proof editor for that logic. This proof editor can be driven by human interaction or by a proof...
Proof plans for the correction of false conjectures (1994)
Raul Monroy, Alan Bundy, Andrew Irel
Abstract. Theorem proving is the systematic derivation of a mathematical proof from a set of axioms by the use of rules of inference. We are interested in a related but far less explored problem: the...
Constructing Probabilistic ATMS Using Extended Incidence Calculus (1994)
This paper discusses the relations between extended incidence calculus and the Assumption-based Truth Maintenance Systems (ATMS). We first prove that managing labels for statements (nodes) in an ATMS...
On the Relations between Incidence Calculus and ATMS (1993)
Weiru Liu, Alan Bundy, Dave Robertson
Abstract. This paper discusses the relationship between incidence calculus and the ATMS. It shows that managing labels for statements in an ATMS is similar to producing the incidence sets of these...
Models of interaction as a grounding for peer to peer knowledge sharing (1993)
David Robertson, Chris Walton, Adam Barker, Paolo Besana, Fadzil Hassan, ...
Abstract. Most current attempts to achieve reliable knowledge sharing on a large scale have relied on pre-engineering of content and supply services. This, like traditional knowledge engineering,...
Coloured rippling: An extension of a theorem proving heuristic (1993)
Tetsuya Yoshida, Alan Bundy, Ian Green, Toby Walsh
. Rippling is a type of rewriting developed in inductive theorem proving for removing differences between terms; the induction conclusion is annotated to mark its differences from the induction...
Rippling: A Heuristic for Guiding Inductive Proofs (1993)
Alan Bundy, Andrew Stevens, Frank Van Harmelen, Andrew Ireland, Alan Smaill
We describe rippling: a tactic for the heuristic control of the key part of proofs by mathematical induction. This tactic significantly reduces the search for a proof of a wide variety of inductive...
Logic Program Synthesis via Proof Planning (1993)
Ina Kraan, Ina Kraan, David Basin, David Basin, David Basin, ...
We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At...
Middle-Out Reasoning for Logic Program Synthesis (1993)
Ina Kraan David, Ina Kraan, David Basin, David Basin, David Basin, ...
We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At...
Recovering Incidence Functions (1993)
Weiru Liu, Alan Bundy, Dave Robertson
In incidence calculus, inferences are usually made by calculating incidence sets and computing probabilities of formulae based on a given incidence function in an incidence calculus theory. Incidence...
Middle-Out Reasoning for Logic Program Synthesis (1993)
Im Stadtwald, Ina Kraan, Ina Kraan, David Basin, David Basin, Alan Bundy, ...
Logic programs can be synthesized as a by-product of the planning of their verification proofs. This is achieved by using higher-order variables at the proof planning level, which become instantiated...
A Framework for Program Development Based on Schematic Proof (1993)
David Basin, Alan Bundy, Ina Kraan, Sean Matthews, Im Stadtwald
. Often, calculi for manipulating and reasoning about programs can be recast as calculi for synthesizing programs. The difference involves often only a slight shift of perspective: admitting...
Recovering Incidence Functions (1993)
Weiru Liu, Alan Bundy, Dave Robertson
In incidence calculus, inferences usually are made by calculating incidence sets and probabilities of formulae based on a given incidence function in an incidence calculus theory. However it is still...
Models of interaction as a grounding for peer to peer knowledge sharing (1993)
David Robertson, Adam Barker, Paolo Besana, Alan Bundy, Fausto Giunchiglia, ...
Abstract. Most current attempts to achieve reliable knowledge sharing on a large scale have relied on pre-engineering of content and supply services. This, like traditional knowledge engineering,...
Models of interaction as a grounding for peer to peer knowledge sharing (1993)
Frank Van, Ronny Siebes, David Robertson, David Robertson, Adam Barker, ...
Abstract. Most current attempts to achieve reliable knowledge sharing on a large scale have relied on pre-engineering of content and supply services. This, like traditional knowledge engineering,...
Using middle-out reasoning to control the synthesis of tail-recursive programs (1992)
Jane Hesketh, Alan Bundy, Alan Smaill
We describe a novel technique for the automatic synthesis of tail-recursive programs. The technique is to specify the required program using the standard equations and then synthesise the...
Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs (1992)
Jane Hesketh Alan, Jane Hesketh, Alan Bundy, Alan Bundy, Alan Bundy, ...
We describe a novel technique for the automatic synthesis of tail-recursive programs. The technique is to specify the required program using the standard equations and then synthesise the...
Experiments with Proof Plans for Induction (1992)
Alan Bundy, Frank Van Harmelen, Jane Hesketh, Alan Smaill
The technique of proof plans, is explained. This technique is used to guide automatic inference in order to avoid a combinatorial explosion. Empirical research is described to test this technique in...
The Use of Proof Plans for Normalization (1992)
We propose using proof plans to implement expression normalizers in automatic theorem proving. We outline some general-purpose proof plans and show how these can be combined in various ways to yield...
A Rational Reconstruction and Extension of Recursion Analysis (1992)
Alan Bundy, Frank Van Harmelen, Jane Hesketh, Alan Smaill, Andrew Stevens
The focus of this paper is the technique of recursion analysis. Recursion analysis is used by the Boyer-Moore Theorem Prover to choose an appropriate induction schema and variable to prove theorems...
Using Failure to Guide Inductive Proof (1992)
Andrew Ireland Alan, Alan Bundy
Lemma discovery and generalization are two of the major hurdles in automating inductive proof. This paper addresses aspects of these related problems. We build upon rippling, a heuristic which plays...
An Adaptation of Proof-Planning to Declarer Play in Bridge (1992)
In Bridge, Ian Frank, David Basin, Alan Bundy
. We present Finesse, a system that forms plans for declarer play in the game of Bridge. Finesse generalises the technique of proof-planning, developed at Edinburgh University in the context of...
An Adaptation of Proof-Planning to Declarer Play in Bridge (1992)
Ian Frank, David Basin, Alan Bundy
. We present Finesse, a system that forms optimal plans for declarer play in the game of Bridge. Finesse generalises the technique of proof-planning, developed at Edinburgh University in the context...
The Use of Proof Plans to Sum Series (1992)
Toby Walsh, Alex Nunes, Alan Bundy
We describe a program for finding closed form solutions to finite sums. The program was built to test the applicability of the proof planning search control technique in a domain of mathematics...
The Combination of Different Pieces of Evidence Using Incidence Calculus (1992)
Combining multiple sources of information is a major and difficult task in the management of uncertainty. Dempster's combination rule is one of the attractive approaches. However, many...
This paper addresses the question of how we can understand reasoning in general and mathematical proofs in particular. It argues the need for a high-level understanding of proofs to complement the...
A Science of Reasoning: Extended Abstract (1990)
How can we understand reasoning in general and mathematical proofs in particular? It is argued that a high-level understanding of proofs is needed to complement the low-level understanding provided...
A rational reconstruction and extension of recursion analysis (1989)
Alan Bundy, Frank Van Harmelen, Jane Hesketh, Alan Smaill, Andrew Stevens
The focus of this paper is the technique of recur8\on analysis. Recursion analysis is used by the Boyer-Moore Theorem Prover to choose an appropriate induction schema and variable to prove theorems...
The Use of Explicit Plans to Guide Inductive Proofs (1988)
We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and...
Explanation-based generalisation = Partial evaluation (1988)
Frank Van Harmelen, Alan Bundy
We argue that explanation-based generalisation as recently proposed in the machine learning literature is essentially equivalent to partial evaluation, a well known technique in the functional and...
Prospects for Artificial Intelligence (1986)
Alan Bundy January, Alan Bundy
Artificial intelligence (AI) has had a turbulent history. It has alternated between periods of optimism and accelerated funding and periods of pessimism and reduced funding. Why does this field of...
Solving mechanics problems using meta-level inference (1979)
Alan Bundy, Lawrence Byrd, George Luger, Chris Mellish, Martha Palmer
which solves a wide range of mechanics problems from statements in both predicate calculus and English. Mecho uses the technique of meta-level inference to control search in natural language...
Middle-Out Reasoning for Synthesis and Induction
David Basin, David Basin, Ina Kraan David, Ina Kraan, Alan Bundy, ...
We develop two applications of middle-out reasoning in inductive proofs: Logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first...
On the Relations between Incidence Calculus and ATMS
Weiru Liu, Alan Bundy, Dave Robertson
. This paper discusses the relationship between incidence calculus and the ATMS. It shows that managing labels for statements in an ATMS is similar to producing the incidence sets of these statements...