0

1 
(* Title: 91/Modal/T


2 
ID: $Id$


3 
Author: Martin Coen


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
T = Modal0 +


8 
rules


9 
(* Definition of the star operation using a set of Horn clauses *)


10 
(* For system T: gamma * == {P  []P : gamma} *)


11 
(* delta * == {P  <>P : delta} *)


12 


13 
lstar0 "L>"


14 
lstar1 "$G L> $H ==> []P, $G L> P, $H"


15 
lstar2 "$G L> $H ==> P, $G L> $H"


16 
rstar0 "R>"


17 
rstar1 "$G R> $H ==> <>P, $G R> P, $H"


18 
rstar2 "$G R> $H ==> P, $G R> $H"


19 


20 
(* Rules for [] and <> *)


21 


22 
boxR


23 
"[ $E L> $E'; $F R> $F'; $G R> $G'; \


24 
\ $E'  $F', P, $G'] ==> $E  $F, []P, $G"


25 
boxL "$E, P, $F  $G ==> $E, []P, $F  $G"


26 
diaR "$E  $F, P, $G ==> $E  $F, <>P, $G"


27 
diaL


28 
"[ $E L> $E'; $F L> $F'; $G R> $G'; \


29 
\ $E', P, $F' $G'] ==> $E, <>P, $F  $G"


30 
end
