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.

翻译：我们首次对部分订单和线性订单的无量化理论的决定程序进行了核查,正式确定了伊莎贝尔/HOL程序,并提供了使用伊莎贝尔代码生成器可执行的规格,该程序已经是伊莎贝尔开发版本的一部分,作为简化的次级程序。