veriT

swMATH7281MaRDI QIDQ19326FDOQ19326

Author name not available (Why is that?)

Official website: http://rd.springer.com/chapter/10.1007/978-3-642-02959-2_12

Cited In (67)

• 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
• Zephyrus2
• 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
• SMT-LIB
• libpoly
• GiNaCRA
• Zenon
• SMTInterpol
• CVC Lite
• CLSAT
• OpenSMT
• CPGraph
• CERES
• CVC4
• MathSAT5
• Hadamard
• SMT-RAT
• Beagle
• Lynx
• MathCheck
• raSAT
• A learning-based fact selector for Isabelle/HOL
• Compression of propositional resolution proofs via partial regularization
• TIP
• SageSAT
• nsoks
• Saturate
• GAPT
• Scavenger
• iSAT
• Psyche
• CoqHammer
• FLOTTER
• SMTCoq
• Satisfiability modulo theories
• Positive solutions of systems of signed parametric polynomial inequalities
• egg
• Ordered_Resolution_Prover
• Extending SMT solvers to higher-order logic
• Exploiting symmetry in SMT problems
• SMT proof checking using a logical framework
• Goeland
• CertiStr
• 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