The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
From MaRDI portal
Publication:2055849
DOI10.1007/978-3-030-79876-5_7OpenAlexW3183167184MaRDI QIDQ2055849
Norbert Th. Müller, Margarita Korovina, Franz Brauße, Konstantin Korovin
Publication date: 1 December 2021
Full work available at URL: https://arxiv.org/abs/2104.13269
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
Cites Work
- 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
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- A CDCL-style calculus for solving non-linear constraints
- Conflict-driven satisfiability for theory combination: transition system and completeness
- raSAT: An SMT Solver for Polynomial Constraints
- Towards Conflict-Driven Learning for Virtual Substitution
- δ-Complete Decision Procedures for Satisfiability over the Reals
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- 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
This page was built for publication: The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
