Name
Abstract | ||
|---|---|---|
Walther's estimation calculus was designed to prove the termination of functional programs, and can also be used to solve the similar problem of proving the well-foundedness of induction rules. However, there are certain features of the goal formulae which are more common to the problem of induction rule well-foundedness than the problem of termination, and which the calculus cannot handle. We present a sound extension of the calculus that is capable of dealing with these features. The extension develops Walther's concept of an argument bounded function in two ways: firstly, so that the function may be bounded below by its cirgument, and secondly, so that a bound may exist between two arguments of a predicate. Our calculus enables automatic proofs of the well-foundedness of a large class of induction rules not captiued by the original calculus. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48242-3_16 | LPAR |
Keywords | Field | DocType |
induction rule well-foundedness,certain feature,induction rule,functional program,sound extension,estimation calculus,original calculus,automatic proof,similar problem,argument bounded function,functional programming,termination analysis | Situation calculus,Epsilon calculus,Natural deduction,Computer science,Proof calculus,Algorithm,Calculus of communicating systems,Time-scale calculus,Differentiation rules,Process calculus,Calculus | Conference |
ISBN | Citations | PageRank |
3-540-66492-0 | 3 | 6.13 |
References | Authors | |
8 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeremy Gow | 1 | 1702 | 84.56 |
| A. Bundy | 2 | 3713 | 532.03 |
| Ian Green | 3 | 71 | 11.77 |