Validated proof-producing decision procedures

MaRDI QIDQ2848058zbMATH OpenFDO

Authors Robert Klapper, Aaron Stump

Publication date 25 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105050723

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Producing proofs from an arithmetic decision procedure in elliptical LF
• Mechanizing Mathematical Reasoning
• Automated Deduction – CADE-20
• CVC: A cooperating validity checker
• A practical integration of first-order reasoning and decision procedures

Cited in

(5)

• Proof generation in the Touchstone theorem prover
• Verifying integrity of decision diagrams
• Painless programming combining reduction and search, design principles for embedding decision procedures in high-level languages
• Fast congruence closure and extensions
• Proof synthesis and reflection for linear arithmetic

This page was built for publication: Validated proof-producing decision procedures

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