Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL

DOI10.1007/978-3-540-85110-3_20MaRDI QIDQ5505503zbMATH OpenOpenAlexFDO

Authors Amine Chaieb

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)

Recommendations

• Linear quantifier elimination
• Linear Quantifier Elimination
• A verified decision procedure for orders in Isabelle/HOL
• Proof synthesis and reflection for linear arithmetic
• Verifying Mixed Real-Integer Quantifier Elimination

Cited in

(6)

• A verified decision procedure for orders in Isabelle/HOL
• Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
• Linear Quantifier Elimination
• Formal power series
• Linear quantifier elimination
• Proof synthesis and reflection for linear arithmetic

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle

This page was built for publication: Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL

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