Paper Info
Title
Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions
Abstract
This paper advocates and explores the use of multipredicate induction schemes for proofs about mutually recursive functions. The interactive application of multi-predicate schemes stemming from datatype definitions is already well-established practice; this paper describes an automated proof procedure based on multi-predicate schemes. Multipredicate schemes may be formally derived from (mutually recursive) function definitions; such schemes are often helpful in proving properties of mutually recursive functions where the recursion pattern does not follow that of the underlying datatypes. These ideas have been implemented using the HOL theorem prover and the Clam proof planner.
Year
DOI
Venue
2000
10.1007/3-540-44957-4_42
Computational logic
Keywords
Field
DocType
multi-predicate scheme,datatype definition,mutually recursive functions,paper advocate,multipredicate scheme,hol theorem prover,automatic derivation,automated proof procedure,recursive function,interactive application,function definition,induction schemes,clam proof planner,theorem prover
HOL,Discrete mathematics,Primitive recursive function,Computer science,Automated theorem proving,Mathematical proof,Parsing,μ operator,Proof procedure,Recursion
Conference
Volume
ISSN
ISBN
1861
0302-9743
3-540-67797-6
Citations 
PageRank 
References 
8
0.55
11
Authors
2
Name
Order
Citations
PageRank
Richard J. Boulton125523.64
Konrad Slind257755.90