RegStab
RegSTAB is a SAT-solver able to deal with formula schemas:
you can give it a scheme of formulas such as "/\i=1..n
P_i -> P_i+1" (where n is a variable)
and it will be able to answer you if *all the formulas
of this form (i.e. for every value of n) are unsatisfiable*, i.e. it can treat at once an infinite set of
propositional formulas.
[ Homepage ]
| Author: | Vincent Aravantinos. |
| Last modification date: | 21-May-2012 |
| Version: | 2.0 |
| Development status: | Stable |
| Kind: | Applications written in Caml :: Scientific software |
| License: | Public Domain |
| Topic: | Science :: Maths and Logic |
| Homepage: | http://regstab.forge.ocamlcore.org/ |