Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
This paper reports a case study in the use of proof planning in the context of higher order syntax. Rippling is a heuristic for guiding rewriting steps in induction that has been used successfully in proof planning inductive proofs using first order representations. Ordinal arithmetic provides a n...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Springer
2001
|
| Online Access: | https://eprints.nottingham.ac.uk/339/ |