The following pages link to veriT (Q19326):
Displaying 33 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)
- MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (Q3454125) (← links)
- A Meta-level Annotation Language for Legal Texts (Q5098747) (← links)
- Towards an Executable Methodology for the Formalization of Legal Texts (Q5098748) (← links)
- Exploiting Symmetry in SMT Problems (Q5200027) (← links)
- Compression of Propositional Resolution Proofs via Partial Regularization (Q5200028) (← links)
- (Q5219923) (← links)
- Complexity of translations from resolution to sequent calculus (Q5236549) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
