Derivation and use of induction schemes in higher-order logic
- 1 January 1997
- book chapter
- Published by Springer Nature
- p. 275-290
- https://doi.org/10.1007/bfb0028400
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- The use of explicit plans to guide inductive proofsPublished by Springer Nature ,2010
- An interface between CLAM and HOLPublished by Springer Nature ,1998
- Function definition in higher-order logicPublished by Springer Nature ,1996
- Automating induction over mutually recursive functionsPublished by Springer Nature ,1996
- Unification-Based InductionPublished by Elsevier ,1993
- Automating Recursive Type Definitions in Higher Order LogicPublished by Springer Nature ,1989
- Verifying the unification algorithm in LCFScience of Computer Programming, 1985
- Compiling pattern matchingLecture Notes in Computer Science, 1985