Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

DOI10.1007/978-3-642-36742-7_6MaRDI QIDQ5326316zbMATH OpenOpenAlexFDO

Authors Ajith K. John, Supratik Chakraborty

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-36742-7_6

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Weak Integer Quantifier Elimination Beyond the Linear Case
• Efficiently solving quantified bit-vector formulas
• On solving quantified bit-vector constraints using invertibility conditions
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Solving quantified bit-vectors using invertibility conditions
• Quantifier elimination for linear modular constraints
• Linear quantifier elimination
• Linear Quantifier Elimination
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding

Cited in

(4)

• A layered algorithm for quantifier elimination from linear modular constraints
• Quantifier elimination for linear modular constraints
• Efficient handling of universally quantified inequalities
• Sharpening constraint programming approaches for bit-vector theory

This page was built for publication: Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

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