Ian Green

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.

ECAI Conference 1998 Conference Paper

Observant: An Annotated Term-Rewriting System for Deciding Observation Congruence

• Raúl Monroy
• Alan Bundy
• Ian Green

LOPSTR Conference 1994 Conference Paper

A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (Abstract)

• Peter Madden
• Jane Hesketh
• Ian Green
• Alan Bundy

ECAI Conference 1994 Conference Paper

Coloured Rippling: An Extension of a Theorem Proving Heuristic

• Tetsuya Yoshida
• Alan Bundy
• Ian Green
• Toby Walsh
• David A. Basin

AAAI Conference 1991 Conference Paper

Using Abstraction to Automate Program Improvement by Transformation

• Ian Green

The problem of automatically improving functional programs using Darlington’s unfold/fold technique is addressed. Transformation tactics are formalized as methods consisting of pre- and postconditions, expressed within a sorted meta-logic. Predicates and functions of this logic induce an abstract program property space within which conventional monotonic planning techniques are used to automatically compose methods (hence tactics) into a program improving strategy. This metaprogram reasoning casts the undirected search of the transformation space as a goal-directed search of the more abstract space. Tactics are only weakly specified by methods. This flexibility is required if they are to be applicable to the class of generalized programs that satisfy the pre-conditions of their methods. This is achieved by allowing the tactics to generate degenerate scripts that may require refinement. Examples of tactics and given, with illustrations of their use program improvement. methods are in automatic