A verified decision procedure for orders in Isabelle/HOL

DOI10.1007/978-3-030-88885-5_9MaRDI QIDQ2147186zbMATHOpenAlexFDO

Authors Lukas Stevens, Tobias Nipkow

Publication date 22 June 2022

Full work available at URL https://arxiv.org/abs/2104.13117

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Linear quantifier elimination
• Linear Quantifier Elimination
• Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL
• Complete integer decision procedures as derived rules in HOL
• A practical integration of first-order reasoning and decision procedures

Cites work

• scientific article; zbMATH DE number 1670734 (Why is no real title available?)
• Data refinement in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Linear Quantifier Elimination
• On the elementary theory of linear order
• Proof-theoretical analysis of order relations
• Undecidability of some simple formalized theories

Cited in

(8)

• Linear quantifier elimination
• Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• Linear Quantifier Elimination
• Complete integer decision procedures as derived rules in HOL
• Logic for Programming, Artificial Intelligence, and Reasoning
• A slice-based decision procedure for type-based partial orders
• Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/HOL
• Archive Formal Proofs
• Szpilrajn Extension

This page was built for publication: A verified decision procedure for orders in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147186)