A Verified Decision Procedure for Orders in Isabelle/HOL
Lukas Stevens, Tobias Nipkow
TL;DR
This paper introduces the first verified implementation of a decision procedure for orders in Isabelle/HOL, formalized and executable within the proof assistant, enhancing Isabelle's capabilities.
Contribution
It provides a formally verified, executable decision procedure for orders, integrated into Isabelle/HOL, which was previously unavailable.
Findings
Verified implementation of the decision procedure
Integration into Isabelle's simplifier
Formalization within Isabelle/HOL
Abstract
We present the first verified implementation of a decision procedure for the quantifier-free theory of partial and linear orders. We formalise the procedure in Isabelle/HOL and provide a specification that is made executable using Isabelle's code generator. The procedure is already part of the development version of Isabelle as a sub-procedure of the simplifier.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.