This is the web interface of modal-tableau-interpolation (borzechowski branch).

Please enter a formula below or choose an example: [(a u b)*](p ^ q) -> [b*]q [(a u b)*]p -> [a*]p [a*]p -> [a**]p [a**]p -> [a*]p [(a u b)*](p ^ q) -> ([b*]q v [b*]r) [a* u ?p]q -> [a u ?r]q [a*]q -> [(a u ?p)*]q ~[(a u ?p)*]q -> ~[a*]q [(a; a)*](p ^ [a; (b u c)]F) -> [a*](p v [c]q) ~[a*](p v [c]q) -> ~[(a; a)*](p ^ [a; (b u c)]F) (p ∧ [a][a*](p ∨ [a*]p)) -> [a][a*]p [a*]p -> [a* ; b*]p [a*]<a>p ~[a*]<a>p [](p ^ q) -> ([]q | []r) [][][][]T ~<><><>F ~~~~F []p -> [][]p