0

1 
(* Title: 91/Modal/S4


2 
ID: $Id$


3 
Author: Martin Coen


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
S4 = Modal0 +


8 
rules


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


10 
(* For system S4: 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,[]P  $G ==> $E, []P, $F  $G"


26 
diaR "$E  $F,P,$G,<>P ==> $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
