Delta-Decision Procedures for Exists-Forall Problems over the Reals

Delta-Decision Procedures for Exists-Forall Problems over the Reals

© The Author(s) 2018. We propose δ -complete decision procedures for solving satisfiability of nonlinear SMT problems over real numbers that contain universal quantification and a wide range of nonlinear functions. The methods combine interval constraint propagation, counterexample-guided synthesis,...

Full description

Bibliographic Details
Main Authors: Kong, Soonho, Solar-Lezama, Armando, Gao, Sicun
Other Authors: Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science
Format: Article
Language:English
Published: Springer International Publishing 2021
Online Access:https://hdl.handle.net/1721.1/137908

Internet

https://hdl.handle.net/1721.1/137908

Similar Items