Show simple item record

Automated Deduction - CADE-11

dc.contributor.authorWalsh, T.
dc.contributor.authorNunes, A.
dc.contributor.authorBundy, Alan
dc.date.accessioned2011-01-24T14:53:45Z
dc.date.available2011-01-24T14:53:45Z
dc.date.issued1992
dc.identifier.isbn3-540-55602-8en
dc.identifier.urihttp://springerlink.metapress.com/content/f1tp258809130825/en
dc.identifier.urihttp://hdl.handle.net/1842/4677
dc.description.abstractWe 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 outwith induction. This experiment was successful. The series summing program extends previous work in this area and was built in a short time just by providing new series summing methods to our existing inductive theorem proving system CLAM. One surprising discovery was the usefulness of the ripple tactic in summing series. Rippling is the key tactic for controlling inductive proofs, and was previously thought to be specialised to such proofs. However, it turns out to be the key sub-tactic used by all the main tactics for summing series. The only change required was that it had to be supplemented by a difference matching algorithm to set up some initial meta-level annotations to guide the rippling process. In inductive proofs these annotations are provided by the application of mathematical induction. This evidence suggests that rippling, supplemented by difference matching, will find wide application in controlling mathematical proofs. The research reported in this paper was supported by SERC grant GR/F/71799, a SERC PostDoctoral Fellowship to the first author and a SERC Senior Fellowship to the third author. We would like to thank the other members of the mathematical reasoning group for their feedback on this project.en
dc.language.isoenen
dc.publisherSpringer Verlagen
dc.titleThe Use of Proof Plans to Sum Seriesen
dc.typeConference Paperen
dc.identifier.doi10.1007/3-540-55602-8en
rps.titleAutomated Deduction - CADE-11en
dc.extent.noOfPages325-339en
dc.extent.pageNumbers325-339en
dc.date.updated2011-01-24T14:53:46Z
dc.date.openingDate1992-06-15
dc.date.closingDate1992-06-18


Files in this item

This item appears in the following Collection(s)

Show simple item record