|
6252
|
1 |
(* Title: 91/Modal/ex/Tthms
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Martin Coen
|
|
|
4 |
Copyright 1991 University of Cambridge
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
|
|
|
8 |
|
|
|
9 |
try "|- []P --> P";
|
|
|
10 |
try "|- [](P-->Q) --> ([]P-->[]Q)"; (* normality*)
|
|
|
11 |
try "|- (P--<Q) --> []P --> []Q";
|
|
|
12 |
try "|- P --> <>P";
|
|
|
13 |
|
|
|
14 |
try "|- [](P & Q) <-> []P & []Q";
|
|
|
15 |
try "|- <>(P | Q) <-> <>P | <>Q";
|
|
|
16 |
try "|- [](P<->Q) <-> (P>-<Q)";
|
|
|
17 |
try "|- <>(P-->Q) <-> ([]P--><>Q)";
|
|
|
18 |
try "|- []P <-> ~<>(~P)";
|
|
|
19 |
try "|- [](~P) <-> ~<>P";
|
|
|
20 |
try "|- ~[]P <-> <>(~P)";
|
|
|
21 |
try "|- [][]P <-> ~<><>(~P)";
|
|
|
22 |
try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
|
|
|
23 |
|
|
|
24 |
try "|- []P | []Q --> [](P | Q)";
|
|
|
25 |
try "|- <>(P & Q) --> <>P & <>Q";
|
|
|
26 |
try "|- [](P | Q) --> []P | <>Q";
|
|
|
27 |
try "|- <>P & []Q --> <>(P & Q)";
|
|
|
28 |
try "|- [](P | Q) --> <>P | []Q";
|
|
|
29 |
try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
|
|
|
30 |
try "|- (P--<Q) & (Q--<R) --> (P--<R)";
|
|
|
31 |
try "|- []P --> <>Q --> <>(P & Q)";
|