Complete integer decision procedures as derived rules in HOL

DOI10.1007/10930755_5MaRDI QIDQ3559760zbMATH OpenOpenAlexFDO

Authors Michael Norrish

Publication date 7 May 2010

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

Full work available at URL https://doi.org/10.1007/10930755_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4112064
• A verified decision procedure for orders in Isabelle/HOL
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• scientific article; zbMATH DE number 1956605
• An effective decision procedure for linear arithmetic over the integers and reals

Cited in

(8)

• A verified decision procedure for orders in Isabelle/HOL
• Laws of mission-based programming
• A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic
• scientific article; zbMATH DE number 4112064 (Why is no real title available?)
• scientific article; zbMATH DE number 1956605 (Why is no real title available?)
• Linear quantifier elimination
• Verifying a signature architecture: a comparative case study
• Proof synthesis and reflection for linear arithmetic

Describes a project that uses

Uses Software

• PVS
• Gandalf

This page was built for publication: Complete integer decision procedures as derived rules in HOL

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