-
Notifications
You must be signed in to change notification settings - Fork 0
/
alc-system-frozen.maude
197 lines (140 loc) · 9.21 KB
/
alc-system-frozen.maude
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
in sequent-calculus.maude
mod LALC-SYSTEM is
inc SEQUENT-CALCULUS .
vars ALFA GAMMA FALFA FGAMMA : Set{Expression} .
vars X Y N : Nat .
var XS : Set{Nat} .
vars A B C D : Concept .
vars R S : Role .
var AT : AConcept .
var Q : Qid .
vars L L1 L2 L3 L4 : List{Label} .
--- rl [initial] :
--- [ X from Y by Q is FALFA : ALFA, < nil | AT | nil > |- < nil | AT | nil >, GAMMA : FGAMMA ] goals((X, XS)) =>
--- [ X from Y by Q is FALFA : ALFA, < nil | AT | nil > |- < nil | AT | nil >, GAMMA : FGAMMA ] goals((XS)) .
eq [ X from Y by Q is FALFA : ALFA, < nil | AT | nil > |- < nil | AT | nil >, GAMMA : FGAMMA ] goals((X, XS)) =
[ X from Y by Q is FALFA : ALFA, < nil | AT | nil > |- < nil | AT | nil >, GAMMA : FGAMMA ] goals((XS)) .
rl [and-r] :
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L | A & B | nil > : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L | A & B | nil > : FGAMMA ] next(N + 2) goals((XS, N, N + 1))
[ N from X by 'and-r is FALFA : ALFA |- GAMMA, < L | A | nil > : FGAMMA ]
[ N + 1 from X by 'and-r is FALFA : ALFA |- GAMMA, < L | B | nil > : FGAMMA ] .
rl [and-l] :
[ X from Y by Q is FALFA : ALFA, < L | A & B | nil > |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA, < L | A & B | nil > |- GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'and-l is FALFA : ALFA, < L | A | nil >, < L | B | nil > |- GAMMA : FGAMMA ] .
rl [or-l] :
[ X from Y by Q is FALFA : ALFA, < nil | (A | B) | L > |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA, < nil | (A | B) | L > |- GAMMA : FGAMMA ] next(N + 2) goals((XS, N, N + 1))
[ N from X by 'or-l is FALFA : ALFA, < nil | A | L > |- GAMMA : FGAMMA ]
[ N + 1 from X by 'or-l is FALFA : ALFA, < nil | B | L > |- GAMMA : FGAMMA ] .
rl [or-r] :
[ X from Y by Q is FALFA : ALFA |- GAMMA, < nil | (A | B) | L > : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- GAMMA, < nil | (A | B) | L > : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'or-r is FALFA : ALFA |- GAMMA, < nil | A | L >, < nil | B | L > : FGAMMA ] .
crl [neg-l] :
[ X from Y by Q is FALFA : ALFA, < L1 | ~ A | L2 > |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA, < L1 | ~ A | L2 > |- GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'neg-l is FALFA : ALFA |- GAMMA, < L3 | A | L4 > : FGAMMA ]
if [L3, L4] := neg(L1, L2) .
crl [neg-r] :
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L1 | ~ A | L2 > : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L1 | ~ A | L2 > : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'neg-r is FALFA : ALFA, < L3 | A | L4 > |- GAMMA : FGAMMA ]
if [L3, L4] := neg(L1, L2) .
rl [forall-r] :
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L1 | ALL(R, A) | L2 > : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L1 | ALL(R, A) | L2 > : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'forall-r is FALFA : ALFA |- GAMMA, < L1 R | A | L2 > : FGAMMA ] .
rl [forall-l] :
[ X from Y by Q is FALFA : ALFA, < L1 | ALL(R, A) | L2 > |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA, < L1 | ALL(R, A) | L2 > |- GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'forall-l is FALFA : ALFA, < L1 R | A | L2 > |- GAMMA : FGAMMA ] .
rl [exist-r] :
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L1 | EXIST(R, A) | L2 > : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- GAMMA, < L1 | EXIST(R, A) | L2 > : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'exist-r is FALFA : ALFA |- GAMMA, < L1 | A | s(R, L1) L2 > : FGAMMA ] .
rl [exist-l] :
[ X from Y by Q is FALFA : ALFA, < L1 | EXIST(R, A) | L2 > |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA, < L1 | EXIST(R, A) | L2 > |- GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'exist-l is FALFA : ALFA, < L1 | A | s(R, L1) L2 > |- GAMMA : FGAMMA ] .
------------------------------------------------------------------------------------------------------------------
--- The promotional rules now have to freze formulas that do not
--- participate in the promotional of labels.
------------------------------------------------------------------------------------------------------------------
vars LA LB : LConcept .
vars GAMMA1 GAMMA2 GAMMA' ALFA' ALFA1 ALFA2 : Set{Expression} .
vars FS FS1 FS2 : Set{Expression} .
op freeze : Set{Expression} Nat Set{Expression} -> Set{Expression} .
eq freeze((LA, FS1), N:Nat, FS) =
freeze(FS1, N:Nat, insert([N:Nat , LA], FS)) .
eq freeze(empty, N:Nat, FS) = FS .
sort FormulasTuple .
op [_,_] : Set{Expression} Set{Expression} -> FormulasTuple [ctor] .
op split-formulas-exist : Set{Expression} Label FormulasTuple -> FormulasTuple .
eq split-formulas-exist((< L1 | A | L2 R >, FS), R, [FS1, FS2]) =
split-formulas-exist(FS, R, [(< L1 | A | L2 R >, FS1), FS2]) .
eq split-formulas-exist((< L1 | A | L2 >, FS), R, [FS1, FS2]) =
split-formulas-exist(FS, R, [FS1, (< L1 | A | L2 >, FS2)]) [owise] .
eq split-formulas-exist(empty, R, [FS1, FS2]) = [FS1, FS2] .
op remove-label-exist : Set{Expression} Label Set{Expression} -> Set{Expression} .
eq remove-label-exist((< L1 | A | L2 R >, FS1), R, FS2) =
remove-label-exist(FS1, R, insert(< L1 | A | L2 >, FS2)) .
eq remove-label-exist(empty, R, FS) = FS .
crl [prom-exist] :
[ X from Y by Q is FALFA : ALFA, < L1 | A | L2 R > |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA, < L1 | A | L2 R > |- GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'prom-exist is freeze(ALFA, 0, FALFA) : < L1 | A | L2 > |- GAMMA' : freeze(GAMMA, 0, FGAMMA) ]
if [GAMMA1, GAMMA2] := split-formulas-exist(GAMMA, R, [empty, empty]) /\
GAMMA' := remove-label-exist(GAMMA1, R, empty) .
op split-formulas-all : Set{Expression} Label FormulasTuple -> FormulasTuple .
eq split-formulas-all((< R L1 | A | nil >, FS), R, [FS1, FS2]) =
split-formulas-all(FS, R, [insert(< R L1 | A | nil >, FS1), FS2]) .
eq split-formulas-all((< R L L1 | A | L2 s(S, R L) >, FS), R, [FS1, FS2]) =
split-formulas-all(FS, R, [insert(< R L L1 | A | L2 s(S, R L) >, FS1), FS2]) .
eq split-formulas-all((< L1 | A | L2 >, FS), R, [FS1, FS2]) =
split-formulas-all(FS, R, [FS1, insert(< L1 | A | L2 >, FS2)]) [owise] .
eq split-formulas-all(empty, R, [FS1, FS2]) = [FS1, FS2] .
op remove-label-all : Set{Expression} Label Set{Expression} -> Set{Expression} .
eq remove-label-all((< R L1 | A | nil >, FS1), R, FS) =
remove-label-all(FS1, R, insert(< L1 | A | nil >, FS)) .
eq remove-label-all((< R L L1 | A | L2 s(S, R L) >, FS1), R, FS) =
remove-label-all(FS1, R, insert(< L L1 | A | L2 s(S, L) >, FS)) .
eq remove-label-all(empty, R, FS) = FS .
crl [prom-all-esp] :
[ X from Y by Q is FALFA : ALFA |- < R L1 | A | nil >, GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- < R L1 | A | nil >, GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'prom-all-esp is freeze(ALFA, 0, FALFA) : ALFA' |- < L1 | A | nil > : freeze(GAMMA, 0, FGAMMA) ]
if [ALFA1, ALFA2] := split-formulas-all(ALFA, R, [empty, empty]) /\
ALFA' := remove-label-all(ALFA1, R, empty) .
crl [prom-all] :
[ X from Y by Q is FALFA : ALFA |- < R L L1 | A | L2 s(S, R L) >, GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- < R L L1 | A | L2 s(S, R L) >, GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'prom-all is freeze(ALFA, 0, FALFA) : ALFA' |- < L1 | A | L2 s(S, L) > : freeze(GAMMA, 0, FGAMMA) ]
if [ALFA1, ALFA2] := split-formulas-all(ALFA, R, [empty, empty]) /\
ALFA' := remove-label-all(ALFA1, R, empty) .
op max-frozen : Set{Expression} Nat -> Nat .
eq max-frozen(([N1:Nat, < L1 | A | L2 >], FS), N2:Nat) =
max-frozen(FS, max(N1:Nat, N2:Nat)) .
eq max-frozen(empty, N:Nat) = N:Nat .
op is-atomic : Set{Expression} -> Bool .
eq is-atomic((< L1 | F:AConcept | L2 >, FS)) = is-atomic(FS) .
eq is-atomic(empty) = true .
eq is-atomic((< L1 | A | L2 >, FS)) = false [owise] .
op unfreeze : Set{Expression} FormulasTuple -> FormulasTuple .
eq unfreeze(([0 , LA], FS), [FS1, FS2]) =
unfreeze(FS, [insert(LA, FS1), FS2]) .
eq unfreeze((F:FzConcept, FS), [FS1, FS2]) =
unfreeze(FS, [FS1, insert(F:FzConcept, FS2)]) [owise] .
eq unfreeze(empty, FT:FormulasTuple) = FT:FormulasTuple .
crl [frozen-exchange] :
[ X from Y by Q is FALFA : ALFA |- GAMMA : FGAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is FALFA : ALFA |- GAMMA : FGAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'frozen-exchange is
freeze(ALFA, M:Nat, ALFA2) : ALFA1 |- GAMMA1 : freeze(GAMMA, M:Nat, GAMMA2) ]
if is-atomic((ALFA, GAMMA)) = true /\
M:Nat := max-frozen(union(FALFA, FGAMMA), 0) + 1 /\
[ALFA1, ALFA2] := unfreeze(FALFA, [empty, empty]) /\
[GAMMA1, GAMMA2] := unfreeze(FGAMMA, [empty, empty]) /\
union(ALFA1, GAMMA1) =/= empty .
endm