equal
deleted
inserted
replaced
|
1 (* Title: 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 |