Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0

DOI10.1007/978-3-540-74591-4_22zbMath1144.68361OpenAlexW66817411MaRDI QIDQ3523183

Konrad Slind, Matt Kaufmann

Publication date: 2 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_22

Mathematics Subject Classification ID

Related Items

The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Uses Software

• ACL2