-
Notifications
You must be signed in to change notification settings - Fork 0
/
test-EL.txt
37 lines (29 loc) · 1.21 KB
/
test-EL.txt
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
Base_functions := { }
Extension_functions := { (hi,1), (po,1), (i,1)}
Relations := { (R,2), (M,3) }
Constants := { (V, int), (H, int), (LV, int), (O, int), (D, int) }
% V - Ventricle, H - Heart, LV - Left Ventricle, D - Disease
%hi - hasInflammation, po - partOf, i - is infected
Base :=
(FORALL x, y, z). M[x,y,z] --> R[z, x];
(FORALL x, y, z). M[x,y,z] --> R[z, y];
(FORALL x, y, z, u). M[x, y, z], R[u, x], R[u, y] --> R[u, z];
(FORALL x). R[x, x];
(FORALL x, y). R[x, y], R[y, x] --> y = x;
(FORALL x, y, z). R[x, y], R[y, z] --> R[x, z];
Clauses:=
% Axiom R1
(FORALL x, y). R[x, po(y)] --> R[hi(x), i(y)]; %Instantiate(po, hi, i)
% Monotonicity axioms of f, g, h
(FORALL x, y). R[x, y] --> R[hi(x), hi(y)];
(FORALL x, y). R[x, y] --> R[po(x), po(y)];
(FORALL x, y). R[x, y] --> R[i(x), i(y)];
%part-of axiom:
(FORALL x, y). R[x, po(y)] --> R[po(x), po(y)];
Query:=
R[LV, V]; %the left ventricle is a ventricle
R[V, po(H)];%a ventricle is part of the heart
R[H, O]; %the heart is an organ
R[D, hi(V)];%there is a disease that causes the ventricle to have an inflammation
% Negation of inclusion to be proved:
NOT(R[D, i(O)]);%there is a disease that causes an organ to be infected