Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Multi-Predicate Induction Schemes for Mutual Recursion
Authors: Richard Boulton
Date:Apr 2000
Where 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.
2000 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Richard Boulton },
title = {Multi-Predicate Induction Schemes for Mutual Recursion},
year = 2000,
month = {Apr},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh