--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Modal/Tthms.ML Fri Feb 05 21:14:17 1999 +0100
@@ -0,0 +1,31 @@
+(* Title: 91/Modal/ex/Tthms
+ ID: $Id$
+ Author: Martin Coen
+ Copyright 1991 University of Cambridge
+*)
+
+(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
+
+try "|- []P --> P";
+try "|- [](P-->Q) --> ([]P-->[]Q)"; (* normality*)
+try "|- (P--<Q) --> []P --> []Q";
+try "|- P --> <>P";
+
+try "|- [](P & Q) <-> []P & []Q";
+try "|- <>(P | Q) <-> <>P | <>Q";
+try "|- [](P<->Q) <-> (P>-<Q)";
+try "|- <>(P-->Q) <-> ([]P--><>Q)";
+try "|- []P <-> ~<>(~P)";
+try "|- [](~P) <-> ~<>P";
+try "|- ~[]P <-> <>(~P)";
+try "|- [][]P <-> ~<><>(~P)";
+try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
+
+try "|- []P | []Q --> [](P | Q)";
+try "|- <>(P & Q) --> <>P & <>Q";
+try "|- [](P | Q) --> []P | <>Q";
+try "|- <>P & []Q --> <>(P & Q)";
+try "|- [](P | Q) --> <>P | []Q";
+try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
+try "|- (P--<Q) & (Q--<R) --> (P--<R)";
+try "|- []P --> <>Q --> <>(P & Q)";