A model-constructing satisfiability calculus
From MaRDI portal
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Recommendations
Cited in
(53)- Editorial: Symbolic computation and satisfiability checking
- The QSMA algorithm for quantifiers in SMT
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- scientific article; zbMATH DE number 1330425 (Why is no real title available?)
- Quantifier elimination for normal cone computations
- Wombit: a portfolio bit-vector solver using word-level propagation
- Levelwise construction of a single cylindrical algebraic cell
- Automatic decidability: a schematic calculus for theories with counting operators
- Semantically-guided goal-sensitive reasoning: model representation
- Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
- Solving nonlinear integer arithmetic with MCSAT
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- SMT solving over finite field arithmetic
- The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Satisfiability modulo bounded checking
- A calculus combining resolution and enumeration for building finite models
- A formal model to prove instantiation termination for E-matching-based axiomatisations
- MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)
- scientific article; zbMATH DE number 1931669 (Why is no real title available?)
- Deciding Bit-Vector Formulas with mcSAT
- On First-Order Model-Based Reasoning
- The model evolution calculus.
- Unifying splitting
- Satisfiability calculus: the semantic counterpart of a proof calculus in general logics
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- A survey of satisfiability modulo theory
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- More is less: adding polynomials for faster explanations in NLSAT
- Boosting MCSat modulo nonlinear integer arithmetic via local search
- scientific article; zbMATH DE number 1696822 (Why is no real title available?)
- Decidability Results for Saturation-Based Model Building
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Propagation based local search for bit-precise reasoning
- The CDSAT method for satisfiability modulo theories and assignment: an exposition
- Cutting to the chase.
- SAT Modulo Differential Equation Simulations
- SAT-Inspired Eliminations for Superposition
- A unifying splitting framework
- From simplification to a partial theory solver for non-linear real polynomial constraints
- ALASCA: reasoning in quantified linear arithmetic
- Local search for solving satisfiability of polynomial formulas
- Satisfiability modulo finite fields
- Modular strategic SMT solving with \textbf{SMT-RAT}
- SGGS decision procedures
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- Introducing asynchronicity to probabilistic hyperproperties
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
This page was built for publication: A model-constructing satisfiability calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2926635)
