A Verified Decision Procedure for Orders in Isabelle/HOL
Logic in Computer Science
2021-11-25 v2
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.
Cite
@article{arxiv.2104.13117,
title = {A Verified Decision Procedure for Orders in Isabelle/HOL},
author = {Lukas Stevens and Tobias Nipkow},
journal= {arXiv preprint arXiv:2104.13117},
year = {2021}
}