-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpc.P
249 lines (187 loc) · 14.1 KB
/
pc.P
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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
:- import append/3 from basics.
:- import memberchk/2 from basics.
:- import member/2 from basics.
:- dynamic strictkb/1.
:- dynamic defeasiblekb/1.
:- dynamic definitelykb/1.
:- dynamic defeasiblykb/1.
:- dynamic minusdefinitelykb/1.
:- dynamic minusdefeasiblykb/1.
:- dynamic factkb/1.
:- dynamic check/1.
:- dynamic supkb/1.
%METAPROGRAM
/* definition of rules */
strictRule(Name, Head, Body) :- strictkb(K), member([Name, Head, Body], K).
defeasibleRule(Name, Head, Body) :- defeasiblekb(K), member([Name, Head, Body], K).
supportive_rule(Name, Head, Body) :- strictRule(Name, Head, Body).
supportive_rule(Name, Head, Body) :- defeasibleRule(Name, Head, Body).
/*rule R with head X is unblocked when there is not an undefeated conflicting rule, or no conflicting rule exists*/
unblocked(_,X):- negation(X,X1), xsb_meta_not(supportive_rule(_,X1,_)).
unblocked(_,X):- negation(X,X1), xsb_meta_not(undefeated(X1)).
/*rule R with head X is blocked either if its premises are not defeasibly provable, or if it is defeated*/
blocked(R,X):- supportive_rule(R,X,L), xsb_meta_not(defeasibly_provable(L)).
blocked(R,X):- supportive_rule(R,X,L), defeasibly_provable(L), defeated(R,X,_).
/*a literal is undefeated when it is supported by a defeasible rule which in not blocked*/
undefeated(X):- supportive_rule(S,X,_), xsb_meta_not(blocked(S,X)).
/*rule S with head X is defeated when there is a conflicting rule, which is superior and its premises are defeasibly provable*/
defeated(S,X,T):- negation(X,X1), supportive_rule(T,X1,V), defeasibly_provable(V), sup(T,S).
negation(~(X),X):- !.
negation(X,~(X)).
xsb_meta_not(X) :- not(X).
%check definite
definitely(X) :- definitelyCheck(X, printOn).
definitely(X, R) :- definitelyCheck(X, R, printOn).
definitelyCheck(X, Print):- Print=printOn, factkb(F), memberchk(X, F), addDefinitely(X).
definitelyCheck(X, Print):- Print=printOff, factkb(F), memberchk(X, F).
definitelyCheck(X, _):- definitelykb(K), memberchk(X, K).
definitelyCheck(X, Print):- logError(Print, [X, ' is neither a fact nor has yet been proven.']).
definitelyCheck(X, R, Print):- Print=printOn, stated_strict(R, X, L), definitely_provable(L), addDefinitely(X).
definitelyCheck(X, R, Print):- Print=printOff, stated_strict(R, X, L), definitely_provable(L).
definitelyCheck(X, R, Print):- stated_strict(R, X, L), !, logError(Print,
['Unable to determine if rule ', R, ' can trigger because its conditions [', L, '] have not yet been proven definitely']).
definitelyCheck(X, R, Print):- stated_strict(R, _, _), !, logError(Print, [R, ' has not ', X, ' as head.']).
definitelyCheck(_, R, Print):- logError(Print, [R, ' does not exist.']).
definitely_provable([X1|X2]):- definitely_provable(X1), definitely_provable(X2).
definitely_provable(X):- definitelykb(K), memberchk(X, K).
definitely_provable([]).
not_definitely(X) :- minusdefinitelykb(K), memberchk(X, K).
not_definitely(X) :- stated_strict(R, X, L), not(minus_definitely_list(L)),not(definitely_provable(L)), !, logError(printOn,
['Unable to determine if rule ', R, ' can trigger because its conditions [', L, '] have not yet been proven definitely']).
not_definitely(X) :- not(definitelyCheck(X, printOff)), not(definitelyCheck(X, _, printOff)), addMinusDefinitely(X).
not_definitely(X) :- definitelyCheck(X, printOff), !, logError(printOn, [X, ' is already proven to be definitely true.']).
not_definitely(X) :- definitelyCheck(X, R, printOff), !, logError(printOn, [X, ' can been proven definitely through rule ', R]).
minus_definitely_list(X1):- minusdefinitelykb(K), memberchk(X1, K).
minus_definitely_list([X1|_]):- minusdefinitelykb(K), memberchk(X1, K).
minus_definitely_list([_|X2]):- minus_definitely_list(X2).
%check defeasible
defeasibly(X):- defeasiblyCheck(X, printOn).
defeasibly(X, R):- defeasiblyCheck(X, R, printOn).
defeasiblyCheck(X, _):- defeasiblykb(K), memberchk(X, K).
defeasiblyCheck(X, Print):- Print=printOn, definitelyCheck(X, printOff), addDefeasibly(X).
defeasiblyCheck(X, Print):- Print=printOff, definitelyCheck(X, printOff).
defeasiblyCheck(X, Print):- logError(Print, [X, ' has not yet been proven neither defeasibly nor definitely.']).
% defeasiblyCheck(X, _):- stated_fact(X), addDefeasibly(X). % this is a subcase of the above
defeasiblyCheck(X, R, Print):- Print=printOn, addCheck(X), negation(X,X1), supportive_rule(R,X,L), addCheck(R), defeasibly_provable(L),
xsb_meta_not(definitelyCheck(X1, printOff)), not(hasAttackingRule(X, R, printOn)), addDefeasibly(X).
defeasiblyCheck(X, R, Print):- Print=printOff, addCheck(X), negation(X,X1), supportive_rule(R,X,L), addCheck(R), defeasibly_provable(L),
xsb_meta_not(definitelyCheck(X1, printOff)), not(hasAttackingRule(X, R, printOff)).
defeasiblyCheck(_, R, Print):- not(supportive_rule(R,_,_)), !, logError(Print, ['There is no rule ', R, ' in the theory.']).
defeasiblyCheck(X, R, Print):- not(supportive_rule(R,X,_)), !, logError(Print, ['Rule ', R, ' does not have ', X, ' as head']).
defeasiblyCheck(X, R, Print):- supportive_rule(R,X,L), not(defeasibly_provable(L)), !,
logError(Print, ['Unable to determine if rule ', R, ' can trigger because its conditions [', L, '] have not yet been proven defeasibly']).
defeasiblyCheck(X, _, Print):- negation(X,X1), definitelyCheck(X1, printOff), !,
logError(Print, ['The negation of ', X, ': ', X1 ,' has been proven definitely']).
defeasibly_provable([X1|X2]):- defeasibly_provable(X1), defeasibly_provable(X2).
defeasibly_provable(X):- defeasiblykb(K), memberchk(X, K).
defeasibly_provable([]).
not_defeasibly(X) :- minusdefeasiblykb(K), memberchk(X, K).
not_defeasibly(X) :- supportive_rule(R,X,L), not(minus_defeasibly_list(L)), not(defeasibly_provable(L)), !,
logError(printOn, ['Unable to determine if rule ', R, ' can trigger because its conditions [', L, '] have not yet been proven defeasibly']).
not_defeasibly(X) :- not(defeasiblyCheck(X, printOff)), not(defeasiblyCheck(X, _, printOff)), addMinusDefeasibly(X).
not_defeasibly(X) :- defeasiblyCheck(X, printOff), !, logError(printOn, [X, ' is already proven to be defeasibly true.']).
not_defeasibly(X) :- defeasiblyCheck(X, R, printOff), !, logError(printOn, [X, ' can been proven defeasibly through rule ', R]).
minus_defeasibly_list(X1):- minusdefeasiblykb(K), memberchk(X1, K).
minus_defeasibly_list([X1|_]):- minusdefeasiblykb(K), memberchk(X1, K).
minus_defeasibly_list([_|X2]):- minus_defeasibly_list(X2).
hasAttackingRule(X, R, Print) :- negation(X, NegX), supportive_rule(AttackingR, NegX, _), hasAttackingRule(X, R, AttackingR, Print).
% if AttackingR < R, there is no problem
hasAttackingRule(_, R, AttackingR, _) :- sup(R, AttackingR), !, fail.
% if AttackingR's conditions are not defeasibly provable, there is no problem
hasAttackingRule(X, _, AttackingR, _) :- negation(X, NegX), supportive_rule(AttackingR, NegX, L), minus_defeasibly_list(L), !, fail.
hasAttackingRule(X, R, AttackingR, Print) :- /* no info about connection between rules R and AttackingR... */
/* no suppirior rule exists, so AttackingR attacks R*/ negation(X, NegX),
not(sup(_, AttackingR)), sup(AttackingR, R), supportive_rule(AttackingR, NegX, L), defeasibly_provable(L),
not(logError(Print, ['Rule ', R, ' is defeated by ', AttackingR, '.'])).
hasAttackingRule(_, R, AttackingR, Print) :- not(sup(_, AttackingR)), sup(AttackingR, R),
not(logError(Print, ['Rule ', R, ' may be defeated by ', AttackingR, ' (there is no information about some conditions of ', AttackingR, ').'])).
hasAttackingRule(_, _, AttackingR, Print) :- /* no info about connection between rules R and AttackingR... */
/* no suppirior rule exists, so AttackingR attacks R*/
not(sup(_, AttackingR)),
not(logError(Print, ['Conflict with attacking rule ', AttackingR, '.'])).
hasAttackingRule(X, _, AttackingR, _) :- sup(RNew, AttackingR), supportive_rule(RNew, X, Conditions),
defeasibly_provable(Conditions), !, fail.
hasAttackingRule(_, _, AttackingR, Print) :- sup(RNew, AttackingR),
not(logError(Print, ['Conflict with attacking rule ', AttackingR, '. (', RNew, '>', AttackingR,
', but ', RNew, ' is not triggered.)'])).
%add variable X to the definitely knowledge base
addDefinitely(X) :- definitelykb(K), retractall(definitelykb(_)), append(K, [X], Knew), assert(definitelykb(Knew)), addDefeasibly(X), addCheck(X).
%add variable X to the defeasibly knowledge base
addDefeasibly(X) :- defeasiblykb(K), retractall(defeasiblykb(_)), append(K, [X], Knew), assert(defeasiblykb(Knew)).
%add variable X to the defeasibly knowledge base
addMinusDefeasibly(X) :- minusdefeasiblykb(K), retractall(minusdefeasiblykb(_)), append(K, [X], Knew), assert(minusdefeasiblykb(Knew)).
%add variable X to the defeasibly knowledge base
addMinusDefinitely(X) :- minusdefinitelykb(K), retractall(minusdefinitelykb(_)), append(K, [X], Knew), assert(minusdefinitelykb(Knew)).
%add to checked (for variables AND RULES that are examined).
addCheck(X) :- check(C), (xsb_meta_not(memberchk(X, C)) ->retractall(check(_)), append(C, [X], Cnew), assert(check(Cnew))
;1=1).
%ask if X is checked
checked([X1|X2]):- checked(X1), checked(X2).
checked(X) :- check(C), memberchk(X, C).
checked([]).
/*RULES*/
%check if a strict/defeasible rule has been stated
stated_strict(N,H,B) :- xsb_meta_not(strict_warning([N,H,B])), strictkb(F), memberchk([N,H,B], F), check(C), memberchk([N,H,B], C).
stated_defeasible(N,H,B) :- xsb_meta_not(defeasible_warning([N,H,B])), defeasiblekb(D), memberchk([N,H,B], D), check(C), memberchk([N,H,B], C).
%warning if there is such rule (which can trigger), but its not stated in the proof
strict_warning([N, H, B]) :- strictkb(S), memberchk([N, H, B], S), /*Rule is in theory*/
check(C), xsb_meta_not(memberchk([N, H, B], C)), /*Rule is stated in proof*/
memberchk(B, C), definitely_provable(B), /*Rule can trigger*/
logWarning(printOn, ['You have not mentioned strict rule ', N]).
defeasible_warning([N, H, B]) :- defeasiblekb(D), memberchk([N, H, B], D), /*Rule is in theory*/
check(C), xsb_meta_not(memberchk([N, H, B], C)), /*Rule is stated in proof*/
memberchk(B, C), defeasibly_provable(B), /*Rule can trigger*/
logWarning(printOn, ['You have not mentioned defeasible rule ', N]).
%check if a strict/defeasible rule exists in the theory
strict_error(Name, Head, Body) :- strictkb(S), xsb_meta_not(memberchk([Name, Head, Body], S)),
logError(printOn, ['Strict rule ', Name, ' does not exist in the theory!']).
defeasible_error(Name, Head, Body) :- defeasiblekb(D), xsb_meta_not(memberchk([Name, Head, Body], D)),
logError(printOn, ['Defeasible rule ', Name, ' does not exist in the theory!']), nl.
%add strict/defeasible rules (no duplicates)
addStrict(Name, Head, Body) :- strictkb(S), (xsb_meta_not(memberchk([Name, Head, Body], S)) ->
retractall(strictkb(_)), append(S, [[Name, Head, Body]], Snew), assert(strictkb(Snew));1=1),
strict(Name, Head, Body).
addDefeasible(Name, Head, Body) :- defeasiblekb(D), (xsb_meta_not(memberchk([Name, Head, Body], D)) -> retractall(defeasiblekb(_)),
append(D, [[Name, Head, Body]], Dnew), assert(defeasiblekb(Dnew));1=1), defeasible(Name, Head, Body).
%proof claims that a rule is strict/defeasible. If its true, add the rule to the stated rules.
strict(Name, Head, Body) :- addCheck([Name, Head, Body]).
defeasible(Name, Head, Body) :- addCheck([Name, Head, Body]).
%add priorities (avoid duplicates)
addSup(R1, R2) :- supkb(S), (xsb_meta_not(memberchk([R1, R2], S)) ->
retractall(supkb(_)), append(S, [[R1, R2]], Snew), assert(supkb(Snew));1=1).
%check priorities
sup(R1, R2) :- supkb(S), memberchk([R1, R2], S).
/*FACTS */
%check if X is a fact and if it has been stated
stated_fact(X) :- xsb_meta_not(fact_warning(X)), factkb(F), memberchk(X, F), check(C), memberchk(X, C).
%warning if X is a fact but not stated
fact_warning(X) :- factkb(F), memberchk(X, F), check(C), xsb_meta_not(memberchk(X, C)),
logWarning(printOn, ['You have not stated that ', X, ' is a fact!']).
%check if a fact in the proof is a fact in the theory
fact_error(X) :- factkb(F), memberchk(X, F).
fact_error(X) :- logError(printOn, [X, ' is not a fact!']).
%add fact
addFact(X) :- factkb(F), (xsb_meta_not(memberchk(X, F)) -> retractall(factkb(_)),
append(F, [X], Fnew), assert(factkb(Fnew));
1=1).
%proof claims that X is a fact. If its true, add the fact to the stated facts.
fact(X) :- fact_error(X), addDefinitely(X).
%initialize knowledge bases, also load theory
init :- retractall(definitelykb(_)),retractall(defeasiblykb(_)), retractall(minusdefinitelykb(_)),retractall(minusdefeasiblykb(_)),
retractall(check(_)), retractall(strictkb(_)), retractall(defeasiblekb(_)), retractall(factkb(_)), retractall(supkb(_)),
assert(definitelykb([])), assert(defeasiblykb([])), assert(minusdefinitelykb([])), assert(minusdefeasiblykb([])), assert(check([])),
assert(strictkb([])), assert(defeasiblekb([])), assert(factkb([])), assert(supkb([])).
logError(Print, ErrorMsg) :- Print = 'printOn', append(['ERROR: '], ErrorMsg, L), writeAll(L), !, fail.
logError(Print, _) :- Print = 'printOff', !, fail.
logError(Print, Y) :- write('Illegal call to logError '), write(Print), write(' '), write(Y), nl, fail.
logWarning(printOn, WarningMsg) :- append(['Warning: '], WarningMsg, L), writeAll(L).
logWarning(Print, _) :- Print = 'printOff'.
logWarning(Print, Y) :- write('Illegal call to logWarning '), write(Print), write(' '), write(Y), nl, fail.
writeAll([H | T]) :- write(H), writeAll(T).
writeAll([]) :- nl.
%IGNORE
%avoid errors by declaring those dummies (avoid "no usermod strict/3 exists" etc)
%strict(dum1,dum2,dum3).
%defeasible(dum4,dum5,dum6).
%sup(dum4,dum1).
%fact(dum7).