Pages that link to "Item:Q2926635"
From MaRDI portal
The following pages link to A Model-Constructing Satisfiability Calculus (Q2926635):
Displaying 26 items.
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Interpolation and model checking for nonlinear arithmetic (Q832268) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Propagation based local search for bit-precise reasoning (Q1688546) (← links)
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (Q1996869) (← links)
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints (Q2055849) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Solving bitvectors with MCSAT: explanations from bits and pieces (Q2096440) (← links)
- SGGS decision procedures (Q2096457) (← links)
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) (Q2104500) (← links)
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories (Q2234101) (← links)
- Conflict-driven satisfiability for theory combination: transition system and completeness (Q2303254) (← links)
- Editorial: Symbolic computation and satisfiability checking (Q2307620) (← links)
- From simplification to a partial theory solver for non-linear real polynomial constraints (Q2307623) (← links)
- Wombit: a portfolio bit-vector solver using word-level propagation (Q2323450) (← links)
- Cutting to the chase. (Q2351157) (← links)
- Modular strategic SMT solving with \textbf{SMT-RAT} (Q2414693) (← links)
- Deciding Bit-Vector Formulas with mcSAT (Q2818018) (← links)
- A Survey of Satisfiability Modulo Theory (Q2830018) (← links)
- On First-Order Model-Based Reasoning (Q2945706) (← links)
- Solving Nonlinear Integer Arithmetic with MCSAT (Q2961575) (← links)
- SAT-Inspired Eliminations for Superposition (Q5875949) (← links)
- The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints (Q6076350) (← links)
- Unifying splitting (Q6103590) (← links)
- Levelwise construction of a single cylindrical algebraic cell (Q6149151) (← links)
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover (Q6156634) (← links)
