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'; \

132

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

0

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

132

26 

0

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


28 
diaL


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

132

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

0

31 
end
