changeset 17481 | 75166ebb619b |
parent 2073 | fb0655539d05 |
17480:fd19f77dcf60 | 17481:75166ebb619b |
---|---|
1 (* Title: Modal/S43 |
1 (* Title: Modal/S43 |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen |
3 Author: Martin Coen |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
|
6 This implements Rajeev Gore's sequent calculus for S43. |
|
7 *) |
5 *) |
8 |
6 |
9 local open Modal0_rls S43 |
7 local open Modal0_rls |
10 in structure MP_Rule : MODAL_PROVER_RULE = |
8 in structure MP_Rule : MODAL_PROVER_RULE = |
11 struct |
9 struct |
12 val rewrite_rls = rewrite_rls |
10 val rewrite_rls = rewrite_rls |
13 val safe_rls = safe_rls |
11 val safe_rls = safe_rls |
14 val unsafe_rls = unsafe_rls @ [pi1,pi2] |
12 val unsafe_rls = unsafe_rls @ [pi1,pi2] |
15 val bound_rls = bound_rls @ [boxL,diaR] |
13 val bound_rls = bound_rls @ [boxL,diaR] |
16 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] |
14 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] |
17 end; |
15 end; |
18 end; |
16 end; |
19 structure S43_Prover = Modal_ProverFun(MP_Rule); |
17 structure S43_Prover = Modal_ProverFun(MP_Rule); |