veriT
From MaRDI portal
Software:19326
No author found.
Related Items (33)
Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ versat: A Verified Modern SAT Solver ⋮ Decision procedures for flat array properties ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Quantifier simplification by unification in SMT ⋮ Satisfiability Modulo Theories ⋮ MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Unnamed Item ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ A Meta-level Annotation Language for Legal Texts ⋮ Towards an Executable Methodology for the Formalization of Legal Texts ⋮ Combining decision procedures by (model-)equality propagation ⋮ Integration of SMT-solvers in B and Event-B development environments ⋮ SMT proof checking using a logical framework ⋮ Congruence Closure with Free Variables ⋮ A superposition calculus for abductive reasoning ⋮ Exploiting Symmetry in SMT Problems ⋮ Compression of Propositional Resolution Proofs via Partial Regularization ⋮ Positive solutions of systems of signed parametric polynomial inequalities ⋮ Scalable fine-grained proofs for formula processing ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Extending SMT solvers to higher-order logic ⋮ Building Bridges between Symbolic Computation and Satisfiability Checking ⋮ MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Complexity of translations from resolution to sequent calculus ⋮ Compression of Propositional Resolution Proofs by Lowering Subproofs ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
This page was built for software: veriT
