## 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/ |