Interpolant based decision procedure for quantifier-free Presburger arithmetic

MaRDI QIDQ5457276zbMATH OpenFDO

Authors Shuvendu K. Lahiri, Krishna K. Mehra

Publication date 14 April 2008

zbMATH Keywords

SAT-solversatisfiability modulo theories

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Interpolating quantifier-free Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Computer Aided Verification

Cited in

(6)

• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Interpolating quantifier-free Presburger arithmetic
• Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
• Computer Aided Verification

Describes a project that uses

Uses Software

• PVS
• UCLID
• ESC/Java

This page was built for publication: Interpolant based decision procedure for quantifier-free Presburger arithmetic

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