We have used several tests for our prover. One can find some of our examples for each of the implemented logics under the following links:

• for K & KD see kkd1 or kkd2.
• for Coalition Logic see cl1 or cl2.
• for Graded Modal Logic gr1 or gr2.
• for Probabilistic Modal Logic pb1 or pb2.
• for Hennesy-Milner Modal Logic hm1 or hm2.
• for Monotonic Modal Logic the examples given for K & KD can be used.

Note that the each example links to a text file, so "Right Click" and "Save As" (or similar depending on the browser) can be used for download.


Back to Tool