0

1 
(* Title: 91/Modal/S43


2 
ID: $Id$


3 
Author: Martin Coen


4 
Copyright 1991 University of Cambridge


5 


6 
This implements Rajeev Gore's sequent calculus for S43.


7 
*)


8 


9 
S43 = Modal0 +


10 


11 
consts


12 
S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,\


13 
\ sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"


14 
"@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,\


15 
\ sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)


16 


17 
rules


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


19 
(* For system S43: gamma * == {[]P  []P : gamma} *)


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


21 


22 
lstar0 "L>"


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


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


25 
rstar0 "R>"


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


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


28 


29 
(* Set of Horn clauses to generate the antecedents for the S43 pi rule *)


30 
(* ie *)


31 
(* S1...Sk,Sk+1...Sk+m *)


32 
(*  *)


33 
(* <>P1...<>Pk, $G  $H, []Q1...[]Qm *)


34 
(* *)


35 
(* where Si == <>P1...<>Pi1,<>Pi+1,..<>Pk,Pi, $G *  $H *, []Q1...[]Qm *)


36 
(* and Sj == <>P1...<>Pk, $G *  $H *, []Q1...[]Qj1,[]Qj+1...[]Qm,Qj *)


37 
(* and 1<=i<=k and k<j<=k+m *)


38 


39 
S43pi0 "S43pi $L;; $R;; $Lbox; $Rdia"


40 
S43pi1


41 
"[ (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox  $R,$Rdia ] ==> \


42 
\ S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia"


43 
S43pi2


44 
"[ (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox  $R',P,$R,$Rdia ] ==> \


45 
\ S43pi $L';; $R'; []P,$R; $Lbox;$Rdia"


46 


47 
(* Rules for [] and <> for S43 *)


48 


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


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


51 
pi1


52 
"[ $L1,<>P,$L2 L> $Lbox; $L1,<>P,$L2 R> $Ldia; $R L> $Rbox; $R R> $Rdia; \


53 
\ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia ] ==> \


54 
\ $L1, <>P, $L2  $R"


55 
pi2


56 
"[ $L L> $Lbox; $L R> $Ldia; $R1,[]P,$R2 L> $Rbox; $R1,[]P,$R2 R> $Rdia; \


57 
\ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia ] ==> \


58 
\ $L  $R1, []P, $R2"


59 
end


60 


61 
ML


62 


63 
local


64 


65 
val S43pi = "S43pi";


66 
val SS43pi = "@S43pi";


67 


68 
val tr = LK.seq_tr1;


69 
val tr' = LK.seq_tr1';


70 


71 
fun s43pi_tr[s1,s2,s3,s4,s5,s6]=


72 
Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;


73 
fun s43pi_tr'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3),


74 
Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =


75 
Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;


76 
in


77 
val parse_translation = [(SS43pi,s43pi_tr)];


78 
val print_translation = [(S43pi,s43pi_tr')]


79 
end
