Dear list,

I am pleased to announce the first release of 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.

RegSTAB is based on a recent paper:

Cheers,

Vincent Aravantinos

PhD Student - LIG - CAPP Team

Grenoble, France

+33.6.11.23.34.72