|
Welcome to RegSTAB Home Page!
RegSTAB is a SAT-Solver able to deal with formulae patterns.
e.g. any SAT-Solver can tell you that each of the following formulae is unsatisfiable:
- P1 Λ (P1 → P2) Λ ¬P2
- P1 Λ (P1 → P2)
Λ (P2 → P3) Λ ¬P3
- P1 Λ (P1 → P2)
Λ (P2 → P3)
Λ (P3 → P4)
Λ ¬P4
- …
But RegSTAB can tell you directly that this is unsatisfiable for all n≥0:
P1 Λ (Λi=1..n Pi → Pi+1) Λ ¬Pn+1
This may be useful e.g. to prove circuit specifications independently of the number of bits.
(if display is still weird click here)
Download RegSTAB
Documentation and Publications
Contact
|
