Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #92116 | |
|---|---|
| Title: | Summing Series Using Proof Plans |
| Authors: | Free,NJ |
| Date: | 1992 |
| Presented: | |
| Keywords: | |
| Abstract: | Formulae for the sums of mathematical series are widely used by computer scientists in the analysis of programs but are often difficult to discover. [Walsh et al 92] describe a system which finds several such formulae using domain specific heuristics and techniques developed by the Mathematical Reasoning Group at Edinburgh University which had previously only been applied to inductive proofs of theorems. This thesis describes the successful implementation of an improved and enhanced version of this system. The new system uses high-order functions to represent summation soundly and has higher-order matching and difference matching algorithms based on Dale Miller's Bon-unification algorithm to facilitate the manipulation of this representation. The number of sums that the system can find solutions to has been increased by implementing additional methods. Facilities have been included to present the reasoning used by the system in a form which can be understood and verified by mathematicians. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}