A verified decision procedure for orders in Isabelle/HOL

DOI10.1007/978-3-030-88885-5_9zbMath1497.68549arXiv2104.13117OpenAlexW3208388410MaRDI QIDQ2147186

Tobias Nipkow, Lukas Stevens

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)

Uses Software

• Isabelle/HOL
• Archive Formal Proofs
• Szpilrajn Extension

Cites Work

• Unnamed Item
• Proof-theoretical analysis of order relations
• Isabelle/HOL. A proof assistant for higher-order logic
• Linear Quantifier Elimination
• Data Refinement in Isabelle/HOL
• On the elementary theory of linear order
• Undecidability of some simple formalized theories

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