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