The following pages link to veriT (Q19326):
Displaying 25 items.
- Decision procedures for flat array properties (Q287272) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- Quantifier simplification by unification in SMT (Q831945) (← links)
- Positive solutions of systems of signed parametric polynomial inequalities (Q1798326) (← links)
- Integration of SMT-solvers in B and Event-B development environments (Q1951640) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) (Q2104500) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (Q2360872) (← links)
- Modular strategic SMT solving with \textbf{SMT-RAT} (Q2414693) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation (Q2817292) (← links)
- Building Bridges between Symbolic Computation and Satisfiability Checking (Q2819729) (← links)
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (Q2829996) (← links)
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic (Q2830009) (← links)
- Compression of Propositional Resolution Proofs by Lowering Subproofs (Q2851933) (← links)
- versat: A Verified Modern SAT Solver (Q2891429) (← links)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Congruence Closure with Free Variables (Q3303931) (← links)
