The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
From MaRDI portal
Publication:6076350
DOI10.1016/j.tcs.2023.114125MaRDI QIDQ6076350
Margarita Korovina, Konstantin Korovin, Franz Brauße, Norbert Th. Müller
Publication date: 21 September 2023
Published in: Theoretical Computer Science (Search for Journal in Brave)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A search-based procedure for nonlinear real arithmetic
- Topological properties of real number representations.
- Subtropical satisfiability
- A CDCL-style calculus for solving non-linear constraints
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Using Taylor Models in Exact Real Arithmetic
- raSAT: An SMT Solver for Polynomial Constraints
- Towards Conflict-Driven Learning for Virtual Substitution
- δ-Complete Decision Procedures for Satisfiability over the Reals
- A Model-Constructing Satisfiability Calculus
- Complexity Theory for Operators in Analysis
- Delta-Decidability over the Reals
- Towards Using Exact Real Arithmetic for Initial Value Problems
- Conflict Resolution
- Logical Foundations of Cyber-Physical Systems
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
- Solving Systems of Linear Inequalities by Bound Propagation
- Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>
- Combined Global and Local Search for the Falsification of Hybrid Systems
- Some undecidable problems involving elementary functions of a real variable
