Cette page vous donne les différences entre la révision choisie et la version actuelle de la page.

Lien vers cette vue

smtsolvers [Le 28/01/2012 à 11:25]
DavidMentre modification
— (Version actuelle)
Ligne 1: Ligne 1:
-===== 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|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|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.\\ 
-        * License:\\ 
-              * haRVey-FOL: GNU LGPL 2.1\\ 
-                    * haRVey-FOL relies on E-prover (http://eprover.org/): GNU GPL\\ 
-              * haRVey-SAT: BSD like\\ 
-                    * haRVey-SAT relies on %%MiniSat%%(http://minisat.se/): BSD like\\ 
-        * Web site: http://harvey.loria.fr/haRVey.php\\ 
-==== 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|Coq-checkable]] form.\\ 
-        * License: BSD like\\ 
-        * Web site: http://focal.inria.fr/zenon/ 
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ó