This release adds support for SAT solving based on one-step functions as an alternative to the previous one-step tableau rules. Using this feature COOL now can also reason about Graded Modal Logic. However, the tableau-based implementations are currently much more optimized and should be preferably used whenever available.

Internally this release replaces the handwritten formula parser with a generated one based on ocamllex and menhir for easier extensibility.

Precompiled Linux Binaries