Arrow Research search

Author name cluster

Alan Bundy

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

33 papers
2 author rows

Possible papers

33

ECAI Conference 2020 Conference Paper

Explainable Inference in the FRANK Query Answering System

  • Kwabena Nuamah
  • Alan Bundy

The demand for insights into how artificial intelligent systems work is rapidly growing. This has arisen as AI systems are being integrated into almost every aspect of our lives from finance to health, security and our social lives. Current techniques for generating explanations focus on explaining opaque algorithms such as neural network models. However, considering the fact that these models do not work in isolation, but are combined, either manually or automatically, with other inference operations, local explanations of individual components are simply not enough to give the user adequate insights into how an intelligent system works. It is not unusual for a system made up of fairly intuitive components to become opaque when it is combined with others to build an intelligent agent. In this paper we argue that there is the need to combine diverse forms of reasoning in order to generate explanations that span the entire chain of reasoning: not just explanations for the, so called, black-box models. Our hypothesis is that: A hybrid approach using statistical and deductive reasoning makes possible a richer form of explanation not available to purely statistical ML approaches. We explore the concepts of ‘local’ and ‘global’ explanations and show how to give users a wide range of insights, using what we term an ‘explanation blanket’. We tackle this challenge using the FRANK query answering system and show that its hybrid approach facilitates this kind of reasoning with explanations. It is important to note that the evaluation of user preferences for explanation is outside the scope of this work.

IS Journal 2015 Journal Article

The Theory behind Theory Mine

  • Alan Bundy
  • Flaminia Cavallo
  • Lucas Dixon
  • Moa Johansson
  • Roy McCasland

The TheoryMine novelty gift company sells the rights to name novel mathematical theorems. The technology is made up of a pipeline of four computer systems that generates recursive theories, then speculates conjectures in those theories and proves the conjectures. All stages of the theorem discovery and proof processes are completely automatic. The process guarantees large numbers of sound, novel theorems of some intrinsic merit.

IJCAI Conference 2007 Conference Paper

  • Alan Bundy

Using the achievements of my research group over the last 30+ years, I provide evidence to support the following hypothesis:

TCS Journal 2001 Journal Article

Applying adversarial planning techniques to Go

  • STEVEN WILLMOTT
  • Julian Richardson
  • Alan Bundy
  • JOHN LEVINE

Approaches to computer game playing based on α–β search of the tree of possible move sequences combined with a position evaluation function have been successful for many games, notably Chess. Such approaches are less successful for games with large search spaces and complex positions, such as Go, and we are led to seek alternatives. One such alternative is to model the goals of the players, and their strategies for achieving these goals. This approach means searching the space of possible goal expansions, typically much smaller than the space of move sequences. Previous attempts to apply these techniques to Go have been unable to provide results for anything other than a high strategic level or very open game positions. In this paper we describe how adversarial hierarchical task network planning can provide a framework for goal-directed game playing in Go which is also applicable both strategic and tactical problems.

IJCAI Conference 1999 Conference Paper

Automatic Concept Formation in Pure Mathematics

  • 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 of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of interesting new mathematics and enables it to build theories from just the axioms of finite algebras.

LPAR Conference 1999 Conference Paper

Extensions to the Estimation Calculus

  • Jeremy Gow
  • Alan Bundy
  • Ian Green

Abstract 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. However, there are certain features of the goal formulae which are more common to the problem of induction rule well-foundedness than the problem of termination, and which the calculus cannot handle. We present a sound extension of the calculus that is capable of dealing with these features. The extension develops Walther’s concept of an argument bounded function in two ways: firstly, so that the function may be bounded below by its argument, and secondly, so that a bound may exist between two arguments of a predicate. Our calculus enables automatic proofs of the well-foundedness of a large class of induction rules not captured by the original calculus.

LPAR Conference 1999 Conference Paper

Proofs About Lists Using Ellipsis

  • Alan Bundy
  • Julian Richardson

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 use an unambiguous higher-order formulation of lists which is amenable to formal proofs without using induction, and to display using the familiar. .. notation.

AAAI Conference 1996 Conference Paper

Computing Abstraction Hierarchies by Numerical Simulation

  • Alan Bundy
  • Roberto Sebastiani

We present a novel method for building ABSTRIPSstyle abstraction hierarchies in planning. The aim of this method is to minimize the amount of backtracking between abstraction levels. Previous approaches have determined the criticality of operator preconditions by reasoning about plans directly. Here, we adopt a simpler and faster approach where we use numerical simulation of the planning process. We demonstrate the theoretical advantages of our approach by identifying some simple properties lacking in previous approaches but possessed by our method. We demonstrate the empirical advantages of our approach by a set of four benchmark experiments using the ABTWEAK system. We compare the quality of the abstraction hierarchies generated with those built by the ALPINE and HIGHPOINT algorithms.

ICAPS Conference 1996 Invited Paper

Proof Planning

  • 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 to guide the search for new proofs in this family. Proof plans are very similar to the plans constructed by plan formation techniques. Some differences are the nonpersistence of objects in the mathematical domain, the absence of goal interaction in mathematics, the high degree of generality of proof plans, the use of a metalogic to describe preconditions in proof planning and the use of annotations in formulae to guide search.

IJCAI Conference 1995 Conference Paper

Relational Rippling: A Ceneral Approach

  • Alan Bundy
  • Vincent Lombart

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 for representations in which value passing is by shared existential variables, as op­ posed to function nesting. Thus relational rip­ pling can be used to guide reasoning about logic programs or circuits represented as relations. We give an informal motivation and introduc­ tion to relational rippling. More details, includ­ ing formal definitions and termination proofs can be found in the longer version of this pa­ per, [Bundy and Lombart, 1995].

LPAR Conference 1994 Conference Paper

Proof Plans for the Correction of False Conjectures

  • Raúl Monroy
  • Alan Bundy
  • Andrew Ireland

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 analysis and correction of false conjectures, especially where that correction involves finding a collection of antecedents that, together with a set of axioms, transform non-theorems into theorems. Most failed search trees are huge, and special care is to be taken in order to tackle the combinatorial explosion phenomenon. Fortunately, the planning search space generated by proof plans, see [1], are moderately small. We have explored the possibility of using this technique in the implementation of an abduction mechanism to correct non-theorems.

LPAR Conference 1993 Conference Paper

Incresing the Versatility of Heuristic Based Theorem Provers

  • Alistair Manning
  • Andrew Ireland
  • Alan Bundy

Abstract Heuristic based theorem proving systems typically impose a fixed ordering on the strategies which they embody. The ordering reflects the general experience of the system designer. As a consequence, there will exist a variety of specific instances where the fixed ordering breaks down. We present an approach which liberates such systems by introducing a more versatile framework for organising proof strategies.

LOPSTR Conference 1993 Conference Paper

Logic Program Synthesis via Proof Planning

  • Ina Kraan
  • David A. Basin
  • Alan Bundy

Abstract 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 the object level, we prove program verification conjectures in a sorted, first-order theory. The conjectures are of the form \( \forall \xrightarrow[{\arg s. }]{}prog(\xrightarrow[{\arg s}]{}) \leftrightarrow spec(\xrightarrow[{\arg s}]{}). \). At the meta-level, we plan the object-level verification with an unspecified program definition. The definition is represented with a (second-order) meta-level variable, which becomes instantiated in the course of the planning. This technique is an application of the Clam proof planning system [Bundy et al 90c]. Clam is currently powerful enough to plan verification proofs for given programs. We show that, if Clam’s use of middle-out reasoning is extended, it will also be able to synthesize programs.

AIJ Journal 1993 Journal Article

Rippling: A heuristic for guiding inductive proofs

  • 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 theorems. We first present a basic version of rippling, followed by various extensions which are necessary to capture larger classes of inductive proofs. Finally, we present a generalised form of rippling which embodies these extensions as special cases. We prove that generalised rippling always terminates, and we discuss the implementation of the tactic and its relation with other inductive proof search heuristics.

LOPSTR Conference 1992 Conference Paper

Synthesis and Transfomation of Logic Programs from Constructive, Inductive Proof

  • Geraint A. Wiggins
  • Alan Bundy
  • Ina Kraan
  • Jane Hesketh

Abstract We discuss a technique which allows synthesis of logic programs in the “proofs-as-programs” paradigm [Constable 82]. Constructive, inductive proof is used to show that the specification of a program is realisable; elaboration of a proof gives rise to the synthesis of a program which realises it. We present an update on earlier ideas, and give examples of and justification for them. The work is presented as foundation for further work in proof planning, where we aim to synthesise not only programs, but good programs.

IJCAI Conference 1989 Conference Paper

A Rational Reconstruction and Extension of Recursion Analysis

  • 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 by mathematical induction. A rational reconstruction of recursion analysis is outlined, using the technique of proof plans. This rational reconstruction suggests an extension of recursion analysis which frees the induction suggestion from the forms of recursion found in the conjecture. Preliminary results are reported of the automation of this rational reconstruction and extension using the CLAM- Oyster system.

AIJ Journal 1988 Journal Article

Explanation-based generalisation = partial evaluation

  • 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 logic programming literature. We show this equivalence by analysing the definitions and underlying algorithms of both techniques, and by giving a PROLOG program which can be interpreted as doing either explanation-based generalisation or partial evaluation.

AIJ Journal 1985 Journal Article

An analytical comparison of some rule-learning programs

  • Alan Bundy
  • Bernard Silver
  • Dave Plummer

To become a mature science, Artificial Intelligence needs more theoretical work. One form this should take is the analytic comparison of existing programs to extract precise techniques from the code, compare similar techniques, expose faults, and extend successful techniques. In this spirit, we compare the rule-learning programs of Brazdil [2], Langley [7], Mitchell et al. [14, 15], Shapiro [18], and Waterman [22]. Each of these programs has two main parts: a critic for identifying faulty rules and a modifier for correcting them. To aid comparison we describe the techniques of the various authors using a uniform notation. We find several similarities in the techniques used by the various authors and uncover the relations between them. We compare the rule-learning programs with the concept-learning programs of Quinlan [17], and Young et al. [25]. The two types of program have much in common, and many of the rule-modifying techniques are subsumed by the techniques of Young et al. Quinlan's program is able to learn disjunctive concepts that are more general than those that can be learned by most of the other programs.

IJCAI Conference 1985 Conference Paper

Discovery and Reasoning in Mathematics

  • Alan Bundy

We discuss the automation of mathematical reasoning, surveying the abilities displayed by human mathematicians and the computational techniques available for automating these abilities. We argue the importance of the simultaneous study of these techniques, because problems inherent in one technique can often be solved if it is able to interact with others.

AIJ Journal 1981 Journal Article

Using meta-level inference for selective application of multiple rewrite rule sets in algebraic manipulation

  • Alan Bundy
  • Bob Welham

In this paper we describe a technique for controlling inference, called meta-level inference, and a program for algebraic manipulation, PRESS, which embodies this technique. In PRESS, algebraic expressions are manipulated by a series of methods. The appropriate method is chosen by meta-level inference and itself uses meta-level reasoning to select and apply rewrite rules to the current expression. The use of meta-level inference is shown to drastically cut down on search, lead to clear and modular programs, aid the proving of properties of the program and enable the automatic learning of both new algebraic facts and new control information.

AIJ Journal 1978 Journal Article

Will it reach the top? Prediction in the mechanics world

  • Alan Bundy

We describe an extension of a mechanics problem solving program to the set of “roller coaster” problems, i. e. problems about the motion of a particle on a complex path. The reasoning strategy adopted by the program is described and compared to earlier work in this domain. Conclusions are drawn about the representation of motion and prediction. Questions are raised about Frames and Multiple Representations.

v2026.09.13