Version française
Home     About     Download     Resources     Contact us    

The Caml Hump: RegStab

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/