-
Notifications
You must be signed in to change notification settings - Fork 0
/
alc-language.maude
109 lines (70 loc) · 2.19 KB
/
alc-language.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
fmod ALC-SYNTAX is
sorts AConcept Concept ARole Role .
subsort AConcept < Concept .
subsort ARole < Role .
ops ALL EXIST : Role Concept -> Concept .
ops CTRUE CFALSE : -> AConcept .
op _&_ : Concept Concept -> Concept [gather (e E) prec 31] .
op _|_ : Concept Concept -> Concept [gather (e E) prec 32] .
op ~_ : Concept -> Concept [prec 30] .
eq ~ CTRUE = CFALSE .
eq ~ CFALSE = CTRUE .
endfm
fmod ALCQI-SYNTAX is
inc ALC-SYNTAX .
inc NAT .
ops AT-MOST AT-LEAST : Nat Role Concept -> Concept .
op INV : Role -> Role .
var R : Role .
var C : Concept .
--- eq AT-LEAST(1, R, C) = EXIST(R, C) .
endfm
fmod LABEL is
inc ALCQI-SYNTAX .
sort Label .
subsort Role < Label .
endfm
view Label from TRIV to LABEL is
sort Elt to Label .
endv
fmod LALC-SYNTAX is
inc LABEL .
inc LIST{Label} .
sort SLabel .
subsort SLabel < Label .
op s : Label List{Label} -> SLabel .
vars L1 L2 L : List{Label} .
vars R S : Role .
vars C : Concept .
eq s(R, nil) = R .
sorts Expression LConcept FzConcept .
subsorts LConcept FzConcept < Expression .
op <_|_|_> : List{Label} Concept List{Label} -> LConcept [ctor] .
op [_,_] : Nat LConcept -> FzConcept .
sort LabelTuple .
op [_,_] : List{Label} List{Label} -> LabelTuple [ctor] .
op join : List{Label} List{Label} Concept -> Concept .
op invert : Concept -> Concept .
op split : List{Label} List{Label} Concept -> LabelTuple .
op neg : List{Label} List{Label} -> LabelTuple .
eq neg(L1, L2) = split(nil, nil, invert(join(L1, L2, CTRUE))) .
eq join(L1, s(R,L1) L2, C) = join(L1, L2, EXIST(R,C)) .
eq join(nil, R L2, C) = join(nil, L2, EXIST(R,C)) .
eq join(L1 R, L2, C) = join(L1, L2, ALL(R,C)) [owise] .
eq join(nil, nil, C) = C .
eq invert(ALL(R, C)) = EXIST(R, invert(C)) .
eq invert(EXIST(R, C)) = ALL(R, invert(C)) .
eq invert(C) = C [owise] .
eq split(L1, L2, ALL(R,C)) = split(L1 R, L2, C) .
eq split(L1, L2, EXIST(R,C)) = split(L1, s(R,L1) L2, C) .
eq split(L1, L2, C) = [L1, L2] [owise] .
endfm
view Expression from TRIV to LALC-SYNTAX is
sort Elt to Expression .
endv
fmod LALCQI-SYNTAX is
inc LALC-SYNTAX .
sort QLabel .
subsort QLabel < Label .
ops gt lt : Nat Label -> QLabel .
endfm