veriT
From MaRDI portal
VeriT
Cited in
(67)- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Flexible proof production in an industrial-strength SMT solver
- Quantifier simplification by unification in SMT
- Scalable fine-grained proofs for formula processing
- 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
- Combining decision procedures by (model-)equality propagation
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Congruence closure with free variables
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SMT-LIB
- libpoly
- GiNaCRA
- Zenon
- SMTInterpol
- CVC Lite
- CLSAT
- OpenSMT
- CPGraph
- CERES
- CVC4
- MathSAT5
- Hadamard
- SMT-RAT
- Beagle
- Lynx
- MathCheck
- raSAT
- TIP
- SageSAT
- nsoks
- Saturate
- GAPT
- Scavenger
- iSAT
- Psyche
- CoqHammer
- FLOTTER
- SMTCoq
- egg
- Ordered_Resolution_Prover
- 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
- Goeland
- SMT proof checking using a logical framework
- Exploiting symmetry in SMT problems
- Integration of SMT-solvers in B and Event-B development environments
- Compression of propositional resolution proofs by lowering subproofs
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- Zephyrus2
- Modular strategic SMT solving with \textbf{SMT-RAT}
- scientific article; zbMATH DE number 7178358 (Why is no real title available?)
- CertiStr
- 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
