* [ANN] RegSTAB released
@ 2009-07-06 8:49 Vincent Aravantinos
0 siblings, 0 replies; 2+ messages in thread
From: Vincent Aravantinos @ 2009-07-06 8:49 UTC (permalink / raw)
To: Gurus Ocaml
[-- Attachment #1: Type: text/plain, Size: 735 bytes --]
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.
Link: http://forge.ocamlcore.org/projects/regstab/
RegSTAB is based on a recent paper:
http://membres-liglab.imag.fr/aravantinos/Publis/tableaux2009/tab09.pdf
Cheers,
--
Vincent Aravantinos
PhD Student - LIG - CAPP Team
Grenoble, France
+33.6.11.23.34.72
vincent.aravantinos@imag.fr
http://membres-lig.imag.fr/aravantinos/
[-- Attachment #2: Type: text/html, Size: 4572 bytes --]
^ permalink raw reply [flat|nested] 2+ messages in thread
* [ANN] RegSTAB released
@ 2009-07-06 9:34 vincent aravantinos
0 siblings, 0 replies; 2+ messages in thread
From: vincent aravantinos @ 2009-07-06 9:34 UTC (permalink / raw)
To: caml-list
[Sorry for multiple post]
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.
Link: http://forge.ocamlcore.org/projects/regstab/
Manual: manual
RegSTAB is based on a recent paper:
http://membres-liglab.imag.fr/aravantinos/Publis/tableaux2009/tab09.pdf
Cheers,
--
Vincent Aravantinos
PhD Student - LIG - CAPP Team
Grenoble, France
+33.6.11.23.34.72
vincent.aravantinos@imag.fr
http://membres-lig.imag.fr/aravantinos/
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2009-07-06 9:34 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2009-07-06 8:49 [ANN] RegSTAB released Vincent Aravantinos
2009-07-06 9:34 vincent aravantinos
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).