Adapting Real Quantifier Elimination Methods for Conflict Set Computation

DOI10.1007/978-3-319-24246-0_10zbMath1471.68248arXiv1511.01123OpenAlexW2232115856MaRDI QIDQ2964460

Pascal Fontaine, Maximilian Jaroschek, Pablo Federico Dobal

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1511.01123

zbMATH Keywords

cylindrical algebraic decompositionSMTreal quantifier eliminationvirtual substitutionconflict set

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (2)

Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Fully incremental cylindrical algebraic decomposition

Uses Software

• QEPCAD
• REDUCE
• REDLOG
• SIMPLIFY
• SMT-RAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining decision procedures by (model-)equality propagation
• Quantifier elimination for real algebra -- the quadratic case and beyond
• The complexity of linear problems in fields
• Real quantifier elimination is doubly exponential
• Partial cylindrical algebraic decomposition for quantifier elimination
• Simplification of quantifier-free formulae over ordered fields
• Constructing a single cell in cylindrical algebraic decomposition
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• An Incremental Algorithm for Computing Cylindrical Algebraic Decompositions
• Model-based Theory Combination
• Solving Non-linear Arithmetic
• Simplify: a theorem prover for program checking
• Simplification by Cooperating Decision Procedures
• QEPCAD B

This page was built for publication: Adapting Real Quantifier Elimination Methods for Conflict Set Computation