A Verified Decision Procedure for Orders in Isabelle/HOL
arXiv:2104.13117 · doi:10.1007/978-3-030-88885-5_9
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.