-
Notifications
You must be signed in to change notification settings - Fork 0
/
alc-system.maude
156 lines (115 loc) · 6.4 KB
/
alc-system.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
in sequent-calculus.maude
mod LALC-SYSTEM is
inc SEQUENT-CALCULUS .
vars ALFA GAMMA : Set{Expression} .
var E : 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 ALFA, < nil | AT | nil > |- < nil | AT | nil >, GAMMA ] goals((X, XS)) =>
[ X from Y by Q is ALFA, < nil | AT | nil > |- < nil | AT | nil >, GAMMA ] goals((XS)) .
rl [initial] :
[ X from Y by Q is < nil | CFALSE | nil > |- empty ] goals((X, XS)) =>
[ X from Y by Q is < nil | CFALSE | nil > |- empty ] goals((XS)) .
--- Even if considering the initial rules above, the weak-l and weak-r
--- rules are necessary to the completeness of the system.
rl [weak-l] :
[ X from Y by Q is ALFA, E |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA, E |- GAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'weak-l is ALFA |- GAMMA ] .
rl [weak-r] :
[ X from Y by Q is ALFA |- GAMMA, E ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- GAMMA, E ] next(N + 1) goals((XS, N))
[ N from X by 'weak-r is ALFA |- GAMMA ] .
rl [and-r] :
[ X from Y by Q is ALFA |- GAMMA, < L | A & B | nil > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- GAMMA, < L | A & B | nil > ] next(N + 2) goals((XS, N, N + 1))
[ N from X by 'and-r is ALFA |- GAMMA, < L | A | nil > ]
[ N + 1 from X by 'and-r is ALFA |- GAMMA, < L | B | nil > ] .
rl [and-l] :
[ X from Y by Q is ALFA, < L | A & B | nil > |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA, < L | A & B | nil > |- GAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'and-l is ALFA, < L | A | nil >, < L | B | nil > |- GAMMA ] .
rl [or-l] :
[ X from Y by Q is ALFA, < nil | (A | B) | L > |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA, < nil | (A | B) | L > |- GAMMA ] next(N + 2) goals((XS, N, N + 1))
[ N from X by 'or-l is ALFA, < nil | A | L > |- GAMMA ]
[ N + 1 from X by 'or-l is ALFA, < nil | B | L > |- GAMMA ] .
rl [or-r] :
[ X from Y by Q is ALFA |- GAMMA, < nil | (A | B) | L > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- GAMMA, < nil | (A | B) | L > ] next(N + 1) goals((XS, N))
[ N from X by 'or-r is ALFA |- GAMMA, < nil | A | L >, < nil | B | L > ] .
crl [neg-l] :
[ X from Y by Q is ALFA, < L1 | ~ A | L2 > |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA, < L1 | ~ A | L2 > |- GAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'neg-l is ALFA |- GAMMA, < L3 | A | L4 > ]
if [L3, L4] := neg(L1, L2) .
crl [neg-r] :
[ X from Y by Q is ALFA |- GAMMA, < L1 | ~ A | L2 > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- GAMMA, < L1 | ~ A | L2 > ] next(N + 1) goals((XS, N))
[ N from X by 'neg-r is ALFA, < L3 | A | L4 > |- GAMMA ]
if [L3, L4] := neg(L1, L2) .
rl [forall-r] :
[ X from Y by Q is ALFA |- GAMMA, < L1 | ALL(R, A) | L2 > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- GAMMA, < L1 | ALL(R, A) | L2 > ] next(N + 1) goals((XS, N))
[ N from X by 'forall-r is ALFA |- GAMMA, < L1 R | A | L2 > ] .
rl [forall-l] :
[ X from Y by Q is ALFA, < L1 | ALL(R, A) | L2 > |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA, < L1 | ALL(R, A) | L2 > |- GAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'forall-l is ALFA, < L1 R | A | L2 > |- GAMMA ] .
rl [exist-r] :
[ X from Y by Q is ALFA |- GAMMA, < L1 | EXIST(R, A) | L2 > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- GAMMA, < L1 | EXIST(R, A) | L2 > ] next(N + 1) goals((XS, N))
[ N from X by 'exist-r is ALFA |- GAMMA, < L1 | A | s(R, L1) L2 > ] .
rl [exist-l] :
[ X from Y by Q is ALFA, < L1 | EXIST(R, A) | L2 > |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA, < L1 | EXIST(R, A) | L2 > |- GAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'exist-l is ALFA, < L1 | A | s(R, L1) L2 > |- GAMMA ] .
op all-label-exist : Set{Expression} Label -> Bool .
op remove-label-exist : Set{Expression} Label Set{Expression} -> Set{Expression} .
vars LA LB : LConcept .
var GAMMA' ALFA' : Set{Expression} .
vars FS FS1 FS2 : Set{Expression} .
var LS : Set{Label} .
eq all-label-exist((< L1 | A | L2 R >, GAMMA), R) =
all-label-exist(GAMMA, R) .
eq all-label-exist(empty, R) = true .
eq all-label-exist(GAMMA, R) = false [owise] .
eq remove-label-exist((< L1 | A | L2 R >, GAMMA), R, GAMMA') =
remove-label-exist(GAMMA, R, (GAMMA', < L1 | A | L2 >)) .
eq remove-label-exist(empty, R, GAMMA) = GAMMA .
crl [prom-exist] :
[ X from Y by Q is < L1 | A | L2 R > |- GAMMA ] next(N) goals((X, XS)) =>
[ X from Y by Q is < L1 | A | L2 R > |- GAMMA ] next(N + 1) goals((XS, N))
[ N from X by 'prom-exist is < L1 | A | L2 > |- GAMMA' ]
if all-label-exist(GAMMA, R) = true /\
GAMMA' := remove-label-exist(GAMMA, R, empty) .
op all-label-all : Set{Expression} Label -> Bool .
op remove-label-all : Set{Expression} Label Set{Expression} -> Set{Expression} .
eq all-label-all((< R L L1 | A | L2 s(S, R L) >, ALFA), R) =
all-label-all(ALFA, R) .
eq all-label-all((< R L1 | A | nil >, ALFA), R) =
all-label-all(ALFA, R) .
eq all-label-all(empty, R) = true .
eq all-label-all(ALFA, R) = false [owise] .
eq remove-label-all((< R L1 | A | nil >, ALFA), R, ALFA') =
remove-label-all(ALFA, R, (ALFA', < L1 | A | nil >)) .
eq remove-label-all((< R L L1 | A | L2 s(S, R L) >, ALFA), R, ALFA') =
remove-label-all(ALFA, R, (ALFA', < L L1 | A | L2 s(S, L) >)) .
eq remove-label-all(empty, R, ALFA) = ALFA .
crl [prom-all-esp] :
[ X from Y by Q is ALFA |- < R L1 | A | nil > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- < R L1 | A | nil > ] next(N + 1) goals((XS, N))
[ N from X by 'prom-all-esp is ALFA' |- < L1 | A | nil > ]
if all-label-all(ALFA, R) = true /\ ALFA' := remove-label-all(ALFA, R, empty) .
crl [prom-all] :
[ X from Y by Q is ALFA |- < R L L1 | A | L2 s(S, R L) > ] next(N) goals((X, XS)) =>
[ X from Y by Q is ALFA |- < R L L1 | A | L2 s(S, R L) > ] next(N + 1) goals((XS, N))
[ N from X by 'prom-all is ALFA' |- < L1 | A | L2 s(S, L) > ]
if all-label-all(ALFA, R) = true /\ ALFA' := remove-label-all(ALFA, R, empty) .
endm