7 citations · 13 across the 16 of their papers we have counts for
8 papers · 1 filter
Deciding Predicate Logical Theories of Real-Valued Functions
Stefan Ratschan
The notion of a real-valued function is central to mathematics, computer science, and many other scientific fields. Despite this importance, there are hardly any positive results o…
Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
Enrico Lipparini, Stefan Ratschan
For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satis…
Proceedings 6th International Workshop on Symbolic-Numeric methods for Reasoning about CPS and IoT
Thao Dang, Stefan Ratschan
The proceedings of the 6th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2020) contains papers underlying talks presented at the workshop.…
Efficient Solution of a Class of Quantified Constraints with Quantifier Prefix Exists-Forall
Milan Hladík, Stefan Ratschan
In various applications the search for certificates for certain properties (e.g., stability of dynamical systems, program termination) can be formulated as a quantified constraint…
Applications of Quantified Constraint Solving over the Reals -- Bibliography
Stefan Ratschan
Quantified constraints over the reals appear in numerous contexts. Usually existential quantification occurs when some parameter can be chosen by the user of a system, and univeral…
Efficient Solving of Quantified Inequality Constraints over the Real Numbers
Stefan Ratschan
Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols…
Convergent Approximate Solving of First-Order Constraints by Approximate Quantifiers
Stefan Ratschan
Exactly solving first-order constraints (i.e., first-order formulas over a certain predefined structure) can be a very hard, or even undecidable problem. In continuous structures l…
Solving Composed First-Order Constraints from Discrete-Time Robust Control
Stefan Ratschan, Luc Jaulin
This paper deals with a problem from discrete-time robust control which requires the solution of constraints over the reals that contain both universal and existential quantifiers.…