e83ed59502a681713982f25c559aae77a4145734Christian Maedermodule SegExamples where

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiimport ModalLogic

eb483f2216949400bfef8f6deb5320f071445626Christian Maederimport CombLogic

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescuimport GenericSequent

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder-- example Segala

eb483f2216949400bfef8f6deb5320f071445626Christian Maedertest1 = And (At (K (And (At (KD T)) F))) (And (And F (At (K F))) F)

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder--test4 =

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskitest2 = At (K T)

eb483f2216949400bfef8f6deb5320f071445626Christian Maedertest3 = At (KD F)

585094c4284ed39eb8024cc1178c823c403200faChristian Maeder