veriT
From MaRDI portal
Software:19326
swMATH7281MaRDI QIDQ19326FDOQ19326
Author name not available (Why is that?)
Cited In (33)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Scalable fine-grained proofs for formula processing
- Flexible proof production in an industrial-strength SMT solver
- Quantifier simplification by unification in SMT
- A Meta-level Annotation Language for Legal Texts
- Towards an Executable Methodology for the Formalization of Legal Texts
- Building bridges between symbolic computation and satisfiability checking
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- A superposition calculus for abductive reasoning
- Decision procedures for flat array properties
- Semi-intelligible Isar proofs from machine-generated proofs
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Combining decision procedures by (model-)equality propagation
- Congruence closure with free variables
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Complexity of translations from resolution to sequent calculus
- Modular SMT proofs for fast reflexive checking inside Coq
- A learning-based fact selector for Isabelle/HOL
- Compression of propositional resolution proofs via partial regularization
- Satisfiability modulo theories
- Positive solutions of systems of signed parametric polynomial inequalities
- Extending SMT solvers to higher-order logic
- Exploiting symmetry in SMT problems
- SMT proof checking using a logical framework
- Integration of SMT-solvers in B and Event-B development environments
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Compression of propositional resolution proofs by lowering subproofs
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- Title not available (Why is that?)
- Modular strategic SMT solving with \textbf{SMT-RAT}
- versat: A Verified Modern SAT Solver
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
This page was built for software: veriT
