API tools faq
paste
Advertisement
logicmoo

NAL.pl

logicmoo
Apr 18th, 2018
273
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 28.06 KB | None | 0 0
raw download clone embed print report
  1. %#!/usr/bin/swipl
  2.  
  3. :- module(logicmoo_nars,[ ]).
  4. % nal.pl
  5. % Non-Axiomatic Logic in Prolog
  6. % Version: 1.1, September 2012
  7. % GNU Lesser General Public License
  8. % Author: Pei Wang
  9.  
  10. % This program covers the inference rules of upto NAL-6 in
  11. % "Non-Axiomatic Logic: A Model of Intelligent Reasoning"
  12. % For the details of syntax, see the "User's Guide of NAL"
  13.  
  14. %%% individual inference rules
  15.  
  16. % There are three types of inference rules in NAL:
  17. % (1) "revision" merges its two premises into a conclusion;
  18. % (2) "choice" selects one of its two premises as a conclusion;
  19. % (3) "inference" generates a conclusion from one or two premises.
  20.  
  21. % revision
  22.  
  23. revision([S, T1], [S, T2], [S, T]) :-
  24.     f_rev(T1, T2, T).
  25.  
  26. % choice
  27.  
  28. choice([S, [F1, C1]], [S, [_F2, C2]], [S, [F1, C1]]) :-
  29.     C1 >= C2, !.
  30. choice([S, [_F1, C1]], [S, [F2, C2]], [S, [F2, C2]]) :-
  31.     C1 < C2, !.
  32. choice([S1, T1], [S2, T2], [S1, T1]) :-
  33.     S1 \= S2, f_exp(T1, E1), f_exp(T2, E2), E1 >= E2, !.
  34. choice([S1, T1], [S2, T2], [S2, T2]) :-
  35.     S1 \= S2, f_exp(T1, E1), f_exp(T2, E2), E1 < E2, !.
  36.  
  37. % simplified version
  38.  
  39. infer(T1, T) :- inference([T1, [1, 0.9]], T).
  40.  
  41. infer(inheritance(W1, ext_image(ext_image(represent, [nil, inheritance(product([X, T2]), R)]), [nil, W2, W3])), inheritance(W1, ext_image(represent, [nil, X])), [inheritance(ext_image(represent, [nil, Y]), ext_image(ext_image(represent, [nil, inheritance(product([Y, T2]), R)]), [nil, W2, W3])), V])  :- f_ind([1,0.9], [1, 0.9], V), !.
  42.  
  43. infer(inheritance(W3, ext_image(ext_image(represent, [nil, inheritance(product([T1, X]), R)]), [W1, W2, nil])), inheritance(W3, ext_image(represent, [nil, X])), [inheritance(ext_image(represent, [nil, Y]), ext_image(ext_image(represent, [nil, inheritance(product([T1, Y]), R)]), [W1, W2, nil])), V])  :- f_ind([1,0.9], [1, 0.9], V), !.
  44.  
  45. infer(T1, T2, T) :- inference([T1, [1, 0.9]], [T2, [1, 0.9]],  T).
  46.  
  47.  
  48. % inference/2
  49.  
  50. %% immediate inference
  51.  
  52. inference([inheritance(S, P), T1], [inheritance(P, S), T]) :-
  53.     f_cnv(T1, T).
  54. inference([implication(S, P), T1], [implication(P, S), T]) :-
  55.     f_cnv(T1, T).
  56. inference([implication(negation(S), P), T1], [implication(negation(P), S), T]) :-
  57.     f_cnt(T1, T).
  58.  
  59. inference([negation(S), T1], [S, T]) :-
  60.     f_neg(T1, T).
  61. inference([S, [F1, C1]], [negation(S), T]) :-
  62.     F1 < 0.5, f_neg([F1, C1], T).
  63.  
  64. %% structural inference
  65.  
  66. inference([S1, T], [S, T]) :-
  67.     reduce(S1, S), S1 \== S, !.
  68. inference([S1, T], [S, T]) :-
  69.     equivalence(S1, S); equivalence(S, S1).
  70.  
  71. inference(P, C) :-
  72.     inference(P, [S, [1, 1]], C), call(S).
  73. inference(P, C) :-
  74.     inference([S, [1, 1]], P, C), call(S).
  75.  
  76.  
  77. % inference/3
  78.  
  79. %% inheritance-based syllogism
  80.  
  81. inference([inheritance(M, P), T1], [inheritance(S, M), T2], [inheritance(S, P), T]) :-
  82.     S \= P, f_ded(T1, T2, T).
  83. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(S, P), T]) :-
  84.     S \= P, f_abd(T1, T2, T).
  85. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(S, P), T]) :-
  86.     S \= P, f_ind(T1, T2, T).
  87. inference([inheritance(P, M), T1], [inheritance(M, S), T2], [inheritance(S, P), T]) :-
  88.     S \= P, f_exe(T1, T2, T).
  89.  
  90. %% similarity from inheritance
  91.  
  92. inference([inheritance(S, P), T1], [inheritance(P, S), T2], [similarity(S, P), T]) :-
  93.     f_int(T1, T2, T).
  94.  
  95. %% similarity-based syllogism
  96.  
  97. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [similarity(S, P), T]) :-
  98.     S \= P, f_com(T1, T2, T).
  99. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [similarity(S, P), T]) :-
  100.     S \= P, f_com(T1, T2, T).
  101. inference([inheritance(M, P), T1], [similarity(S, M), T2], [inheritance(S, P), T]) :-
  102.     S \= P, f_ana(T1, T2, T).
  103. inference([inheritance(P, M), T1], [similarity(S, M), T2], [inheritance(P, S), T]) :-
  104.     S \= P, f_ana(T1, T2, T).
  105. inference([similarity(M, P), T1], [similarity(S, M), T2], [similarity(S, P), T]) :-
  106.     S \= P, f_res(T1, T2, T).
  107.  
  108. %% inheritance-based composition
  109.  
  110. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]) :- S \= P, reduce(int_intersection([P, S]), N), f_int(T1, T2, T).
  111. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]) :- S \= P, reduce(ext_intersection([P, S]), N), f_uni(T1, T2, T).
  112. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]) :- S \= P, reduce(int_difference(P, S), N), f_dif(T1, T2, T).
  113. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]) :- S \= P, reduce(ext_intersection([P, S]), N), f_int(T1, T2, T).
  114. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]) :- S \= P, reduce(int_intersection([P, S]), N), f_uni(T1, T2, T).
  115. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]) :- S \= P, reduce(ext_difference(P, S), N), f_dif(T1, T2, T).
  116.  
  117. %% inheirance-based decomposition
  118.  
  119. inference([inheritance(S, M), T1], [inheritance(int_intersection(L), M), T2], [inheritance(P, M), T]) :-
  120.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(int_intersection(N), P), f_pnn(T1, T2, T).
  121. inference([inheritance(S, M), T1], [inheritance(ext_intersection(L), M), T2], [inheritance(P, M), T]) :-
  122.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(ext_intersection(N), P), f_npp(T1, T2, T).
  123. inference([inheritance(S, M), T1], [inheritance(int_difference(S, P), M), T2], [inheritance(P, M), T]) :-
  124.     atom(S), atom(P), f_pnp(T1, T2, T).
  125. inference([inheritance(S, M), T1], [inheritance(int_difference(P, S), M), T2], [inheritance(P, M), T]) :-
  126.     atom(S), atom(P), f_nnn(T1, T2, T).
  127. inference([inheritance(M, S), T1], [inheritance(M, ext_intersection(L)), T2], [inheritance(M, P), T]) :-
  128.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(ext_intersection(N), P), f_pnn(T1, T2, T).
  129. inference([inheritance(M, S), T1], [inheritance(M, int_intersection(L)), T2], [inheritance(M, P), T]) :-
  130.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(int_intersection(N), P), f_npp(T1, T2, T).
  131. inference([inheritance(M, S), T1], [inheritance(M, ext_difference(S, P)), T2], [inheritance(M, P), T]) :-
  132.     atom(S), atom(P), f_pnp(T1, T2, T).
  133. inference([inheritance(M, S), T1], [inheritance(M, ext_difference(P, S)), T2], [inheritance(M, P), T]) :-
  134.     atom(S), atom(P), f_nnn(T1, T2, T).
  135.  
  136. %% implication-based syllogism
  137.  
  138. inference([implication(M, P), T1], [implication(S, M), T2], [implication(S, P), T]) :-
  139.     S \= P, f_ded(T1, T2, T).
  140. inference([implication(P, M), T1], [implication(S, M), T2], [implication(S, P), T]) :-
  141.     S \= P, f_abd(T1, T2, T).
  142. inference([implication(M, P), T1], [implication(M, S), T2], [implication(S, P), T]) :-
  143.     S \= P, f_ind(T1, T2, T).
  144. inference([implication(P, M), T1], [implication(M, S), T2], [implication(S, P), T]) :-
  145.     S \= P, f_exe(T1, T2, T).
  146.  
  147. %% implication to equivalence
  148.  
  149. inference([implication(S, P), T1], [implication(P, S), T2], [equivalence(S, P), T]) :-
  150.     f_int(T1, T2, T).
  151.  
  152. %% equivalence-based syllogism
  153.  
  154. inference([implication(P, M), T1], [implication(S, M), T2], [equivalence(S, P), T]) :-
  155.     S \= P, f_com(T1, T2, T).
  156. inference([implication(M, P), T1], [implication(M, S), T2], [equivalence(S, P), T]) :-
  157.     S \= P, f_com(T1, T2, T).
  158. inference([implication(M, P), T1], [equivalence(S, M), T2], [implication(S, P), T]) :-
  159.     S \= P, f_ana(T1, T2, T).
  160. inference([implication(P, M), T1], [equivalence(S, M), T2], [implication(P, S), T]) :-
  161.     S \= P, f_ana(T1, T2, T).
  162. inference([equivalence(M, P), T1], [equivalence(S, M), T2], [equivalence(S, P), T]) :-
  163.     S \= P, f_res(T1, T2, T).
  164.  
  165. %% implication-based composition
  166.  
  167. inference([implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]) :-
  168.     S \= P, reduce(disjunction([P, S]), N), f_int(T1, T2, T).
  169. inference([implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]) :-
  170.     S \= P, reduce(conjunction([P, S]), N), f_uni(T1, T2, T).
  171. inference([implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]) :-
  172.     S \= P, reduce(conjunction([P, S]), N), f_int(T1, T2, T).
  173. inference([implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]) :-
  174.     S \= P, reduce(disjunction([P, S]), N), f_uni(T1, T2, T).
  175.  
  176. %% implication-based decomposition
  177.  
  178. inference([implication(S, M), T1], [implication(disjunction(L), M), T2], [implication(P, M), T]) :-
  179.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(disjunction(N), P), f_pnn(T1, T2, T).
  180. inference([implication(S, M), T1], [implication(conjunction(L), M), T2], [implication(P, M), T]) :-
  181.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(conjunction(N), P), f_npp(T1, T2, T).
  182. inference([implication(M, S), T1], [implication(M, conjunction(L)), T2], [implication(M, P), T]) :-
  183.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(conjunction(N), P), f_pnn(T1, T2, T).
  184. inference([implication(M, S), T1], [implication(M, disjunction(L)), T2], [implication(M, P), T]) :-
  185.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(disjunction(N), P), f_npp(T1, T2, T).
  186.  
  187. %% conditional syllogism
  188.  
  189. inference([implication(M, P), T1], [M, T2], [P, T]) :-
  190.     ground(P), f_ded(T1, T2, T).
  191. inference([implication(P, M), T1], [M, T2], [P, T]) :-
  192.     ground(P), f_abd(T1, T2, T).
  193. inference([M, T1], [equivalence(S, M), T2], [S, T]) :-
  194.     ground(S), f_ana(T1, T2, T).
  195.  
  196. %% conditional composition
  197.  
  198. inference([P, T1], [S, T2], [C, T]) :-
  199.     C == implication(S, P), f_ind(T1, T2, T).
  200. inference([P, T1], [S, T2], [C, T]) :-
  201.     C == equivalence(S, P), f_com(T1, T2, T).
  202. inference([P, T1], [S, T2], [C, T]) :-
  203.     reduce(conjunction([P, S]), N), N == C, f_int(T1, T2, T).
  204. inference([P, T1], [S, T2], [C, T]) :-
  205.     reduce(disjunction([P, S]), N), N == C, f_uni(T1, T2, T).
  206.  
  207. %% propositional decomposition
  208.  
  209. inference([S, T1], [conjunction(L), T2], [P, T]) :-
  210.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(conjunction(N), P), f_pnn(T1, T2, T).
  211. inference([S, T1], [disjunction(L), T2], [P, T]) :-
  212.     ground(S), ground(L), member(S, L), delete(L, S, N), reduce(disjunction(N), P), f_npp(T1, T2, T).
  213.  
  214. %% multi-conditional syllogism
  215.  
  216. inference([implication(conjunction(L), C), T1], [M, T2], [implication(P, C), T]) :-
  217.     nonvar(L), member(M, L), subtract(L, [M], A), A \= [], reduce(conjunction(A), P), f_ded(T1, T2, T).
  218. inference([implication(conjunction(L), C), T1], [implication(P, C), T2], [M, T]) :-
  219.     ground(L), member(M, L), subtract(L, [M], A), A \= [], reduce(conjunction(A), P), f_abd(T1, T2, T).
  220. inference([implication(conjunction(L), C), T1], [M, T2], [S, T]) :-
  221.     S == implication(conjunction([M|L]), C), f_ind(T1, T2, T).
  222.  
  223. inference([implication(conjunction(Lm), C), T1], [implication(A, M), T2], [implication(P, C), T]) :-
  224.     nonvar(Lm), replace(Lm, M, La, A), reduce(conjunction(La), P), f_ded(T1, T2, T).
  225. inference([implication(conjunction(Lm), C), T1], [implication(conjunction(La), C), T2], [implication(A, M), T]) :-
  226.     nonvar(Lm), replace(Lm, M, La, A), f_abd(T1, T2, T).
  227. inference([implication(conjunction(La), C), T1], [implication(A, M), T2], [implication(P, C), T]) :-
  228.     nonvar(La), replace(Lm, M, La, A), reduce(conjunction(Lm), P), f_ind(T1, T2, T).
  229.  
  230. %% variable introduction
  231.  
  232. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [implication(inheritance(X, S), inheritance(X, P)), T]) :-
  233.     S \= P, f_ind(T1, T2, T).
  234. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [implication(inheritance(P, X), inheritance(S, X)), T]) :-
  235.     S \= P, f_abd(T1, T2, T).
  236. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [equivalence(inheritance(X, S), inheritance(X, P)), T]) :-
  237.     S \= P, f_com(T1, T2, T).
  238. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [equivalence(inheritance(P, X), inheritance(S, X)), T]) :-
  239.     S \= P, f_com(T1, T2, T).
  240. inference([inheritance(M, P), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)]), T]) :-
  241.     S \= P, f_int(T1, T2, T).
  242. inference([inheritance(P, M), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))]), T]) :-
  243.     S \= P, f_int(T1, T2, T).
  244.  
  245. %% 2nd variable introduction
  246.  
  247. inference([implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [implication(conjunction([A, inheritance(X, S)]), inheritance(X, P)), T]) :-
  248.     S \= P, M1 == M2, A \= inheritance(M2, S), f_ind(T1, T2, T).
  249. inference([implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [conjunction([implication(A, inheritance(var(Y, []), P)), inheritance(var(Y, []), S)]), T]) :-
  250.     S \= P, M1 == M2, A \= inheritance(M2, S), f_int(T1, T2, T).
  251. inference([conjunction(L1), T1], [inheritance(M, S), T2], [implication(inheritance(Y, S), conjunction([inheritance(Y, P2)|L3])), T]) :-
  252.     subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, dependent(P, Y, P2), dependent(L2, Y, L3), f_ind(T1, T2, T).
  253. inference([conjunction(L1), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)|L2]), T]) :-
  254.     subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, f_int(T1, T2, T).
  255.  
  256. inference([implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [implication(conjunction([A, inheritance(P, X)]), inheritance(S, X)), T]) :-
  257.     S \= P, M1 == M2, A \= inheritance(S, M2), f_abd(T1, T2, T).
  258. inference([implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [conjunction([implication(A, inheritance(P, var(Y, []))), inheritance(S, var(Y, []))]), T]) :-
  259.     S \= P, M1 == M2, A \= inheritance(S, M2), f_int(T1, T2, T).
  260. inference([conjunction(L1), T1], [inheritance(S, M), T2], [implication(inheritance(S, Y), conjunction([inheritance(P2, Y)|L3])), T]) :-
  261.     subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, dependent(P, Y, P2), dependent(L2, Y, L3), f_abd(T1, T2, T).
  262. inference([conjunction(L1), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))|L2]), T]) :-
  263.     subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, f_int(T1, T2, T).
  264.  
  265. %% dependent variable elimination
  266.  
  267. inference([conjunction(L1), T1], [inheritance(M, S), T2], [C, T]) :-
  268.     subtract(L1, [inheritance(var(N, D), S)], L2), L1 \= L2,
  269.     replace_var(L2, var(N, D), L3, M), reduce(conjunction(L3), C), f_cnv(T2, T0), f_ana(T1, T0, T).
  270. inference([conjunction(L1), T1], [inheritance(S, M), T2], [C, T]) :-
  271.     subtract(L1, [inheritance(S, var(N, D))], L2), L1 \= L2,
  272.     replace_var(L2, var(N, D), L3, M), reduce(conjunction(L3), C), f_cnv(T2, T0), f_ana(T1, T0, T).
  273.  
  274. replace_var([], _, [], _).
  275. replace_var([inheritance(S1, P)|T1], S1, [inheritance(S2, P)|T2], S2) :-
  276.     replace_var(T1, S1, T2, S2).
  277. replace_var([inheritance(S, P1)|T1], P1, [inheritance(S, P2)|T2], P2) :-
  278.     replace_var(T1, P1, T2, P2).
  279. replace_all([H|T1], H1, [H|T2], H2) :-
  280.     replace_var(T1, H1, T2, H2).
  281.  
  282.  
  283.  
  284. %%% Theorems in IL:
  285.  
  286. % inheritance
  287.  
  288. inheritance(ext_intersection(Ls), P) :-
  289.     include([P], Ls).
  290. inheritance(S, int_intersection(Lp)) :-
  291.     include([S], Lp).
  292. inheritance(ext_intersection(S), ext_intersection(P)) :-
  293.     include(P, S), P \= [_].
  294. inheritance(int_intersection(S), int_intersection(P)) :-
  295.     include(S, P), S \= [_].
  296. inheritance(ext_set(S), ext_set(P)) :-
  297.     include(S, P).
  298. inheritance(int_set(S), int_set(P)) :-
  299.     include(P, S).
  300.  
  301. inheritance(ext_difference(S, P), S) :-
  302.     ground(S), ground(P).
  303. inheritance(S, int_difference(S, P)) :-
  304.     ground(S), ground(P).
  305.  
  306. inheritance(product(L1), R) :-
  307.     ground(L1), member(ext_image(R, L2), L1), replace(L1, ext_image(R, L2), L2).
  308. inheritance(R, product(L1)) :-
  309.     ground(L1), member(int_image(R, L2), L1), replace(L1, int_image(R, L2), L2).
  310.  
  311. % similarity
  312.  
  313. similarity(X, Y) :-
  314.     ground(X), reduce(X, Y), X \== Y, !.
  315.  
  316. similarity(ext_intersection(L1), ext_intersection(L2)) :-
  317.     same_set(L1, L2).
  318. similarity(int_intersection(L1), int_intersection(L2)) :-
  319.     same_set(L1, L2).
  320. similarity(ext_set(L1), ext_set(L2)) :-
  321.     same_set(L1, L2).
  322. similarity(int_set(L1), int_set(L2)) :-
  323.     same_set(L1, L2).
  324.  
  325. % implication
  326.  
  327. implication(similarity(S, P), inheritance(S, P)).
  328. implication(equivalence(S, P), implication(S, P)).
  329.  
  330. implication(conjunction(L), M) :-
  331.     ground(L), member(M, L).
  332. implication(M, disjunction(L)) :-
  333.     ground(L), member(M, L).
  334.  
  335. implication(conjunction(L1), conjunction(L2)) :-
  336.     ground(L1), ground(L2), subset(L2, L1).
  337. implication(disjunction(L1), disjunction(L2)) :-
  338.     ground(L1), ground(L2), subset(L1, L2).
  339.  
  340. implication(inheritance(S, P), inheritance(ext_intersection(Ls), ext_intersection(Lp))):-
  341.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  342. implication(inheritance(S, P), inheritance(int_intersection(Ls), int_intersection(Lp))):-
  343.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  344. implication(similarity(S, P), similarity(ext_intersection(Ls), ext_intersection(Lp))):-
  345.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  346. implication(similarity(S, P), similarity(int_intersection(Ls), int_intersection(Lp))):-
  347.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  348.  
  349. implication(inheritance(S, P), inheritance(ext_difference(S, M), ext_difference(P, M))):-
  350.     ground(M).
  351. implication(inheritance(S, P), inheritance(int_difference(S, M), int_difference(P, M))):-
  352.     ground(M).
  353. implication(similarity(S, P), similarity(ext_difference(S, M), ext_difference(P, M))):-
  354.     ground(M).
  355. implication(similarity(S, P), similarity(int_difference(S, M), int_difference(P, M))):-
  356.     ground(M).
  357. implication(inheritance(S, P), inheritance(ext_difference(M, P), ext_difference(M, S))):-
  358.     ground(M).
  359. implication(inheritance(S, P), inheritance(int_difference(M, P), int_difference(M, S))):-
  360.     ground(M).
  361. implication(similarity(S, P), similarity(ext_difference(M, P), ext_difference(M, S))):-
  362.     ground(M).
  363. implication(similarity(S, P), similarity(int_difference(M, P), int_difference(M, S))):-
  364.     ground(M).
  365.  
  366. implication(inheritance(S, P), negation(inheritance(S, ext_difference(M, P)))) :-
  367.     ground(M).
  368. implication(inheritance(S, ext_difference(M, P)), negation(inheritance(S, P))) :-
  369.     ground(M).
  370. implication(inheritance(S, P), negation(inheritance(int_difference(M, S), P))) :-
  371.     ground(M).
  372. implication(inheritance(int_difference(M, S), P), negation(inheritance(S, P))) :-
  373.     ground(M).
  374.  
  375. implication(inheritance(S, P), inheritance(ext_image(S, M), ext_image(P, M))) :-
  376.     ground(M).
  377. implication(inheritance(S, P), inheritance(int_image(S, M), int_image(P, M))) :-
  378.     ground(M).
  379. implication(inheritance(S, P), inheritance(ext_image(M, Lp), ext_image(M, Ls))) :-
  380.     ground(Ls), ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
  381. implication(inheritance(S, P), inheritance(int_image(M, Lp), int_image(M, Ls))) :-
  382.     ground(Ls), ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
  383.  
  384. implication(negation(M), negation(conjunction(L))) :-
  385.     include([M], L).
  386. implication(negation(disjunction(L)), negation(M)) :-
  387.     include([M], L).
  388.  
  389. implication(implication(S, P), implication(conjunction(Ls), conjunction(Lp))):-
  390.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  391. implication(implication(S, P), implication(disjunction(Ls), disjunction(Lp))):-
  392.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  393. implication(equivalence(S, P), equivalence(conjunction(Ls), conjunction(Lp))):-
  394.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  395. implication(equivalence(S, P), equivalence(disjunction(Ls), disjunction(Lp))):-
  396.     ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
  397.  
  398.  
  399. % equivalence
  400.  
  401. equivalence(X, Y) :-
  402.     ground(X), reduce(X, Y), X \== Y, !.
  403.  
  404. equivalence(similarity(S, P), similarity(P, S)).
  405.  
  406. equivalence(inheritance(S, ext_set([P])), similarity(S, ext_set([P]))).
  407. equivalence(inheritance(int_set([S]), P), similarity(int_set([S]), P)).
  408.  
  409. equivalence(inheritance(S, ext_intersection(Lp)), conjunction(L)) :-
  410.     findall(inheritance(S, P), member(P, Lp), L).
  411. equivalence(inheritance(int_intersection(Ls), P), conjunction(L)) :-
  412.     findall(inheritance(S, P), member(S, Ls), L).
  413.  
  414. equivalence(inheritance(S, ext_difference(P1, P2)),
  415.         conjunction([inheritance(S, P1), negation(inheritance(S, P2))])).
  416. equivalence(inheritance(int_difference(S1, S2), P),
  417.         conjunction([inheritance(S1, P), negation(inheritance(S2, P))])).
  418.  
  419. equivalence(inheritance(product(Ls), product(Lp)), conjunction(L)) :-
  420.     equ_product(Ls, Lp, L).
  421.  
  422. equivalence(inheritance(product([S|L]), product([P|L])), inheritance(S, P)) :-
  423.     ground(L).
  424. equivalence(inheritance(S, P), inheritance(product([H|Ls]), product([H|Lp]))) :-
  425.     ground(H), equivalence(inheritance(product(Ls), product(Lp)), inheritance(S, P)).
  426.  
  427. equivalence(inheritance(product(L), R), inheritance(T, ext_image(R, L1))) :-
  428.     replace(L, T, L1).
  429. equivalence(inheritance(R, product(L)), inheritance(int_image(R, L1), T)) :-
  430.     replace(L, T, L1).
  431.  
  432. equivalence(equivalence(S, P), equivalence(P, S)).
  433.  
  434. equivalence(equivalence(negation(S), P), equivalence(negation(P), S)).
  435.  
  436. equivalence(conjunction(L1), conjunction(L2)) :-
  437.     same_set(L1, L2).
  438. equivalence(disjunction(L1), disjunction(L2)) :-
  439.     same_set(L1, L2).
  440.  
  441. equivalence(implication(S, conjunction(Lp)), conjunction(L)) :-
  442.     findall(implication(S, P), member(P, Lp), L).
  443. equivalence(implication(disjunction(Ls), P), conjunction(L)) :-
  444.     findall(implication(S, P), member(S, Ls), L).
  445.  
  446. equivalence(T1, T2) :-
  447.     not(atom(T1)), not(atom(T2)), ground(T1), ground(T2),
  448.     T1 =.. L1, T2 =.. L2, equivalence_list(L1, L2).
  449.  
  450. equivalence_list(L, L).
  451. equivalence_list([H|L1], [H|L2]) :-
  452.     equivalence_list(L1, L2).
  453. equivalence_list([H1|L1], [H2|L2]) :-
  454.     similarity(H1, H2), equivalence_list(L1, L2).
  455. equivalence_list([H1|L1], [H2|L2]) :-
  456.     equivalence(H1, H2), equivalence_list(L1, L2).
  457.  
  458. % compound term structure reduction
  459.  
  460. reduce(similarity(ext_set([S]), ext_set([P])), similarity(S, P)) :-
  461.     !.
  462. reduce(similarity(int_set([S]), int_set([P])), similarity(S, P)) :-
  463.     !.
  464.  
  465. reduce(instance(S, P), inheritance(ext_set([S]), P)) :-
  466.     !.
  467. reduce(property(S, P), inheritance(S, int_set([P]))) :-
  468.     !.
  469. reduce(inst_prop(S, P), inheritance(ext_set([S]), int_set([P]))) :-
  470.     !.
  471.  
  472. reduce(ext_intersection([T]), T) :-
  473.     !.
  474. reduce(int_intersection([T]), T) :-
  475.     !.
  476.  
  477. reduce(ext_intersection([ext_intersection(L1), ext_intersection(L2)]), ext_intersection(L)) :-
  478.     union(L1, L2, L), !.
  479. reduce(ext_intersection([ext_intersection(L1), L2]), ext_intersection(L)) :-
  480.     union(L1, [L2], L), !.
  481. reduce(ext_intersection([L1, ext_intersection(L2)]), ext_intersection(L)) :-
  482.     union([L1], L2, L), !.
  483. reduce(ext_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)) :-
  484.     intersection(L1, L2, L), !.
  485. reduce(ext_intersection([int_set(L1), int_set(L2)]), int_set(L)) :-
  486.     union(L1, L2, L), !.
  487.  
  488. reduce(int_intersection([int_intersection(L1), int_intersection(L2)]), int_intersection(L)) :-
  489.     union(L1, L2, L), !.
  490. reduce(int_intersection([int_intersection(L1), L2]), int_intersection(L)) :-
  491.     union(L1, [L2], L), !.
  492. reduce(int_intersection([L1, int_intersection(L2)]), int_intersection(L)) :-
  493.     union([L1], L2, L), !.
  494. reduce(int_intersection([int_set(L1), int_set(L2)]), int_set(L)) :-
  495.     intersection(L1, L2, L), !.
  496. reduce(int_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)) :-
  497.     union(L1, L2, L), !.
  498.  
  499. reduce(ext_difference(ext_set(L1), ext_set(L2)), ext_set(L)) :-
  500.     subtract(L1, L2, L), !.
  501. reduce(int_difference(int_set(L1), int_set(L2)), int_set(L)) :-
  502.     subtract(L1, L2, L), !.
  503.  
  504. reduce(product(product(L), T), product(L1)) :-
  505.     append(L, [T], L1), !.
  506.  
  507. reduce(ext_image(product(L1), L2), T1) :-
  508.     member(T1, L1), replace(L1, T1, L2), !.
  509. reduce(int_image(product(L1), L2), T1) :-
  510.     member(T1, L1), replace(L1, T1, L2), !.
  511.  
  512. reduce(negation(negation(S)), S) :-
  513.     !.
  514.  
  515. reduce(conjunction([T]), T) :-
  516.     !.
  517. reduce(disjunction([T]), T) :-
  518.     !.
  519.  
  520. reduce(conjunction([conjunction(L1), conjunction(L2)]), conjunction(L)) :-
  521.     union(L1, L2, L), !.
  522. reduce(conjunction([conjunction(L1), L2]), conjunction(L)) :-
  523.     union(L1, [L2], L), !.
  524. reduce(conjunction([L1, conjunction(L2)]), conjunction(L)) :-
  525.     union([L1], L2, L), !.
  526.  
  527. reduce(disjunction(disjunction(L1), disjunction(L2)), disjunction(L)) :-
  528.     union(L1, L2, L), !.
  529. reduce(disjunction(disjunction(L1), L2), disjunction(L)) :-
  530.     union(L1, [L2], L), !.
  531. reduce(disjunction(L1, disjunction(L2)), disjunction(L)) :-
  532.     union([L1], L2, L), !.
  533.  
  534. reduce(X, X).
  535.  
  536.  
  537. %%% Argument processing
  538.  
  539. equ_product([], [], []).
  540. equ_product([T|Ls], [T|Lp], L) :-
  541.     equ_product(Ls, Lp, L), !.
  542. equ_product([S|Ls], [P|Lp], [inheritance(S, P)|L]) :-
  543.     equ_product(Ls, Lp, L).
  544.  
  545. same_set(L1, L2) :-
  546.     L1 \== [], L1 \== [_], same(L1, L2), L1 \== L2.
  547.  
  548. same([], []).
  549. same(L, [H|T]) :-
  550.     member(H, L), subtract(L, [H], L1), same(L1, T).
  551.  
  552. include(L1, L2) :-
  553.     ground(L2), include1(L1, L2), L1 \== [], L1 \== L2.
  554.  
  555. include1([],_).
  556. include1([H|T1],[H|T2]) :-
  557.     include1(T1,T2).
  558. include1([H1|T1],[H2|T2]) :-
  559.     H2 \== H1, include1([H1|T1], T2).
  560.  
  561. not_member(_, []).
  562. not_member(C, [C|_]) :- !, fail.
  563. not_member([S, T], [[S1, T]|_]) :- equivalence(S, S1), !, fail.
  564. not_member(C, [_|L]) :- not_member(C, L).
  565.  
  566. replace([T|L], T, [nil|L]).
  567. replace([H|L], T, [H|L1]) :-
  568.     replace(L, T, L1).
  569.  
  570. replace([H1|T], H1, [H2|T], H2).
  571. replace([H|T1], H1, [H|T2], H2) :-
  572.     replace(T1, H1, T2, H2).
  573.  
  574. dependent(var(V, L), Y, var(V, [Y|L])) :-
  575.     !.
  576. dependent([H|T], Y, [H1|T1]) :-
  577.     dependent(H, Y, H1), dependent(T, Y, T1), !.
  578. dependent(inheritance(S, P), Y, inheritance(S1, P1)) :-
  579.     dependent(S, Y, S1), dependent(P, Y, P1), !.
  580. dependent(ext_image(R, A), Y, ext_image(R, A1)) :-
  581.     dependent(A, Y, A1), !.
  582. dependent(int_image(R, A), Y, int_image(R, A1)) :-
  583.     dependent(A, Y, A1), !.
  584. dependent(X, _, X).
  585.  
  586.  
  587. %%% Truth-value functions
  588.  
  589. f_rev([F1, C1], [F2, C2], [F, C]) :-
  590.      C1 < 1,
  591.      C2 < 1,
  592.     M1 is C1 / (1 - C1),
  593.     M2 is C2 / (1 - C2),
  594.     F is (M1 * F1 + M2 * F2) / (M1 + M2),
  595.     C is (M1 + M2) / (M1 + M2 + 1).
  596.  
  597. f_exp([F, C], E) :-
  598.     E is C * (F - 0.5) + 0.5.
  599.  
  600. f_neg([F1, C1], [F, C1]) :-
  601.     u_not(F1, F).
  602.  
  603. f_cnv([F1, C1], [1, C]) :-
  604.      u_and([F1, C1], W),
  605.     u_w2c(W, C).
  606.  
  607. f_cnt([F1, C1], [0, C]) :-
  608.     u_not(F1, F0),
  609.      u_and([F0, C1], W),
  610.     u_w2c(W, C).
  611.      
  612. f_ded([F1, C1], [F2, C2], [F, C]) :-
  613.     u_and([F1, F2], F),
  614.     u_and([C1, C2, F], C).
  615.  
  616. f_ana([F1, C1], [F2, C2], [F, C]) :-
  617.     u_and([F1, F2], F),
  618.     u_and([C1, C2, F2], C).
  619.  
  620. f_res([F1, C1], [F2, C2], [F, C]) :-
  621.     u_and([F1, F2], F),
  622.     u_or([F1, F2], F0),
  623.     u_and([C1, C2, F0], C).
  624.  
  625. f_abd([F1, C1], [F2, C2], [F2, C]) :-
  626.     u_and([F1, C1, C2], W),
  627.     u_w2c(W, C).
  628.      
  629. f_ind(T1, T2, T) :-
  630.     f_abd(T2, T1, T).
  631.  
  632. f_exe([F1, C1], [F2, C2], [1, C]) :-
  633.     u_and([F1, C1, F2, C2], W),
  634.     u_w2c(W, C).
  635.  
  636. f_com([0, _C1], [0, _C2], [0, 0]).
  637. f_com([F1, C1], [F2, C2], [F, C]) :-
  638.     u_or([F1, F2], F0),
  639.     F0 > 0,
  640.     F is F1 * F2 / F0,
  641.     u_and([F0, C1, C2], W),
  642.     u_w2c(W, C).
  643.  
  644. f_int([F1, C1], [F2, C2], [F, C]) :-
  645.     u_and([F1, F2], F),
  646.     u_and([C1, C2], C).
  647.  
  648. f_uni([F1, C1], [F2, C2], [F, C]) :-
  649.     u_or([F1, F2], F),
  650.     u_and([C1, C2], C).
  651.  
  652. f_dif([F1, C1], [F2, C2], [F, C]) :-
  653.     u_not(F2, F0),
  654.     u_and([F1, F0], F),
  655.     u_and([C1, C2], C).
  656.  
  657. f_pnn([F1, C1], [F2, C2], [F, C]) :-
  658.     u_not(F2, F2n),
  659.     u_and([F1, F2n], Fn),
  660.     u_not(Fn, F),
  661.     u_and([Fn, C1, C2], C).
  662.  
  663. f_npp([F1, C1], [F2, C2], [F, C]) :-
  664.     u_not(F1, F1n),
  665.     u_and([F1n, F2], F),
  666.     u_and([F, C1, C2], C).
  667.  
  668. f_pnp([F1, C1], [F2, C2], [F, C]) :-
  669.     u_not(F2, F2n),
  670.     u_and([F1, F2n], F),
  671.     u_and([F, C1, C2], C).
  672.  
  673. f_nnn([F1, C1], [F2, C2], [F, C]) :-
  674.     u_not(F1, F1n),
  675.     u_not(F2, F2n),
  676.     u_and([F1n, F2n], Fn),
  677.     u_not(Fn, F),
  678.     u_and([Fn, C1, C2], C).
  679.  
  680. % Utility functions
  681.  
  682. u_not(N0, N) :-
  683.     N is (1 - N0), !.
  684.  
  685. u_and([N], N).
  686. u_and([N0 | Nt], N) :-
  687.     u_and(Nt, N1), N is N0 * N1, !.
  688.  
  689. u_or([N], N).
  690. u_or([N0 | Nt], N) :-
  691.     u_or(Nt, N1), N is (N0 + N1 - N0 * N1), !.
  692.  
  693. u_w2c(W, C) :-
  694.     K = 1, C is (W / (W + K)), !.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!