Efficient solving of quantified inequality constraints over the real numbers
From MaRDI portal
Publication:5277761
DOI10.1145/1183278.1183282zbMath1367.68270MaRDI QIDQ5277761
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1183278.1183282
03B70: Logic in computer science
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Related Items
Fuzzy answer set computation via satisfiability modulo theories, Relating syntactic and semantic perturbations of hybrid automata, Real World Verification, Hybrid Automata in Systems Biology: How Far Can We Go?, On the complexity of quantified linear systems, Polynomial function intervals for floating-point software verification, Efficient solution of a class of quantified constraints with quantifier prefix exists-forall, A complexity perspective on entailment of parameterized linear constraints, Analyzing restricted fragments of the theory of linear arithmetic, Construction of parametric barrier functions for dynamical systems using interval analysis, Computational complexity of determining which statements about causality hold in different space-time models, Hybrid automata, reachability, and systems biology, Tightened reachability constraints for the verification of linear hybrid systems, raSAT: an SMT solver for polynomial constraints, Quasi-decidability of a fragment of the first-order theory of real numbers, Vector barrier certificates and comparison systems, On quantified linear implications, Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic, Solving quantified constraint satisfaction problems, Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates, raSAT: An SMT Solver for Polynomial Constraints, Incremental Computation of Succinct Abstractions for Hybrid Systems
Uses Software