Ceci est une ancienne révision du document !


Table des matières

SMT Solvers


haRVey


haRVey is a SMT (Satisfiability Modulo Theories) prover. There are presently two branches of haRVey: haRVey-SAT and haRVey-FOL.

  • haRVey-FOL integrates a First-Order Logic theorem prover (hence its name), i.e. the E-prover. It uses the superposition calculus as implemented by the E-prover, to determine the satisfiability of Boolean combinations of atoms with functions interpreted in a first-order theory with equality.
  • haRVey-SAT is based on congruence closure, the Nelson-Oppen framework, and rudimentary instantiation techniques to decide the satisfiability of a set of atoms written with uninterpreted symbols, linear arithmetics, some lambda-expressions, and some quantifiers. The Boolean engine is a SAT solver (zChaff or MiniSAT), hence its name.

Zenon


Zenon is an automatic theorem that handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.

 
smtsolvers.1327746303.txt.gz · Dernière modification: Le 13/02/2012 à 21:08 (modification externe)     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó