The \texttt{ksmt} calculus is a -complete decision procedure for non-linear constraints

DOI10.1007/978-3-030-79876-5_7MaRDI QIDQ2055849zbMATH OpenOpenAlexFDO

Authors Franz Brauße, Konstantin Korovin, M. V. Korovina, Norbert Th. Müller

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2104.13269

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• A CDCL-style calculus for solving non-linear constraints
• Evaluating optimised decision procedures for propositional modal \({\mathbf K}_{({\mathbf m})}\) satisfiability
• Evaluating optimized decision procedures for propositional modal K(m) satisfiability
• A \(\rho\)-calculus of explicit constraint application
• A \(\rho\)-calculus of explicit constraint application
• -complete decision procedures for satisfiability over the reals
• scientific article; zbMATH DE number 1759450
• An algebraic description of generalizedk-constraints

Cites work

• -complete decision procedures for satisfiability over the reals
• -decidability over the reals
• A CDCL-style calculus for solving non-linear constraints
• A model-constructing satisfiability calculus
• A search-based procedure for nonlinear real arithmetic
• A tutorial on computable analysis
• Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
• Combined global and local search for the falsification of hybrid systems
• Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
• Conflict Resolution
• Conflict-driven satisfiability for theory combination: transition system and completeness
• scientific article; zbMATH DE number 42077 (Why is no real title available?)
• scientific article; zbMATH DE number 52121 (Why is no real title available?)
• scientific article; zbMATH DE number 1460545 (Why is no real title available?)
• scientific article; zbMATH DE number 1746043 (Why is no real title available?)
• scientific article; zbMATH DE number 3326329 (Why is no real title available?)
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Logical foundations of cyber-physical systems
• raSAT: An SMT Solver for Polynomial Constraints
• Solving non-linear arithmetic
• Solving systems of linear inequalities by bound propagation
• Some undecidable problems involving elementary functions of a real variable
• Subtropical satisfiability
• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Topological properties of real number representations.
• Towards conflict-driven learning for virtual substitution
• Towards using exact real arithmetic for initial value problems

Cited in

(3)

• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• Satisfiability of non-linear transcendental arithmetic as a certificate search problem

This page was built for publication: The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055849)