A verified decision procedure for orders in Isabelle/HOL

DOI10.1007/978-3-030-88885-5_9zbMATH Open1497.68549arXiv2104.13117OpenAlexW3208388410MaRDI QIDQ2147186FDOQ2147186

Authors: Lukas Stevens, Tobias Nipkow 

Publication date: 22 June 2022

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.

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

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

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)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Title not available (Why is that?)
• On the elementary theory of linear order
• Proof-theoretical analysis of order relations
• Linear Quantifier Elimination
• Data Refinement in Isabelle/HOL
• Undecidability of some simple formalized theories

Cited In (7)

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

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)