Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL

DOI10.1007/978-3-540-74591-4_5zbMath1144.68352OpenAlexW1869527659MaRDI QIDQ3523164

Tobias Nipkow, Alexander Krauss, Lukas Bulwahn

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_5

Mathematics Subject Classification ID

Related Items (10)

Proof pearl: Mechanizing the textbook proof of Huffman's algorithm ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Verification of distributed systems with local-global predicates ⋮ Friends with Benefits ⋮ A Formalized Theory for Verifying Stability and Convergence of Automata in PVS ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Unnamed Item ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Uses Software

• Isabelle
• Isabelle/HOL
• PVS
• HOL Light

This page was built for publication: Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL