Show simple item record

dc.contributor.authorBoulton, Richard
dc.date.accessioned2010-04-23T14:03:35Z
dc.date.available2010-04-23T14:03:35Z
dc.date.issued2000-04
dc.identifier.urihttp://hdl.handle.net/1842/3405
dc.description.abstractWhere mutually recursive data types are used in programming languages, etc., mutually recursive functions are usually required. Mutually recursive functions are also quite common for non-mutually recursive types. Reasoning about recursive functions requires some form of mathematical induction but there have been difficulties in adapting induction methods for simple recursion to the mutually recursive case. This paper proposes the use of multi-predicate induction schemes in the context of explicit induction and presents a proof method for their use within a proof planning system. An implementation in Clam has successfully planned proofs for a number of mutually recursive examples.en
dc.language.isoenen
dc.relation.ispartofseriesInformatics Report Seriesen
dc.relation.ispartofseriesEDI-INF-RR-0014en
dc.subjectInformaticsen
dc.titleMulti-Predicate Induction Schemes for Mutual Recursionen
dc.typeTechnical Reporten


Files in this item

This item appears in the following Collection(s)

Show simple item record