equal
deleted
inserted
replaced

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 