The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #92137

Title:Summing Series with Proof Plans
Authors:Nunes,A
Date: 1992
Presented:
Keywords:
Abstract:This project dealt with the problem of summing finite series using the proof plans formalism, [Bundy 88, Bundy et al 91]. This is an altogether new application of the proof plans formalism which until now has been examined in the context of inductive theorem-proving. The research conducted over the course of this project demonstrated that not only can this formalism express the high-level strategies employed to sum series but also that many ideas originally developed for inductive proof planning can be exploited with great success in this domain. In particular, the rippling tactic, [Bundy & Stevens 91], finds application the great majority of proofs constructed by the system described within. In order to harness the full power of rippling, a new matching algorithm was specially developed in [Basin & Walsh 91], and its first, successful implementation is reported here. In addition, a number of methods which incorporate standard summing series techniques were implemented, namely standard form, conjugate, telescope and perturbate. These can sum a wide variety of series, some of which are novel to existing summing series systems. inductive domains of mathematics. One of the most important conclusions of this research was that the key inductive proof planning tactics, rippling, could be exploited with equal success in this non-inductive domain. In order for this to be possible, a new matching algorithm was specially developed in [Basin & Walsh 91], and its first implementation is reported in this project. For basic methods were successfully implemented, namely standard form, conjugate, telescope and perturbate which can sum a wide range of series. Some of these series cannot be summed by other existing systems.
Download:NO ONLINE COPY

[Search These Pages] [DAI Home Page] [Comment]