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.
• for Conditional Logic, several examples can be found here.

Note that the examples link to text files, so "Right Click" and "Save As" (or similar depending on the browser) can be used for download.


Back to Tool