% nal.pl
% Non-Axiomatic Logic in Prolog
% Version: 1.0, August 2004
% Author: Pei Wang
% All Rights Reserved

% Inference rules of NAL-1 to NAL1-6

% Format: a judgment has the format of [Statement, Truth-value]

%%% individual inference rules

% There are three types of inference rules in NAL:
% (1) "revision" merges its two premises into a conclusion;
% (2) "choice" selects one of its two premises as a conclusion;
% (3) "inference" generates a conclusion from one or two premises.

% revision

revision([S, T1], [S, T2], [S, T]) :- 
	f_rev(T1, T2, T).

% choice

choice([S, [F1, C1]], [S, [_F2, C2]], [S, [F1, C1]]) :- 
	C1 >= C2.
choice([S, [_F1, C1]], [S, [F2, C2]], [S, [F2, C2]]) :- 
	C1 < C2.
choice([S1, T1], [S2, T2], [S1, T1]) :- 
	S1 \= S2, f_exp(T1, E1), f_exp(T2, E2), E1 >= E2.
choice([S1, T1], [S2, T2], [S2, T2]) :- 
	S1 \= S2, f_exp(T1, E1), f_exp(T2, E2), E1 < E2.

% inference/2

inference([inheritance(S, P), T0], [inheritance(P, S), T]) :- 
	f_cnv(T0, T).

inference([implication(S, P), T0], [implication(P, S), T]) :- 
	f_cnv(T0, T).
inference([implication(negation(S), P), T0], [implication(negation(P), S), T]) :- 
	f_cnt(T0, T).

inference([negation(S), T0], [S, T]) :- 
	f_neg(T0, T).
inference([S, T0], [C, T]) :- 
	C == negation(S), f_neg(T0, T).

inference([S1, T], [S, T]) :-
	equivalence(S1, S); equivalence(S, S1).

inference([S1, T], [S, T]) :-
	reduce(S1, S), S1 \== S.

inference(P, C) :-
	inference(P, [S, [1, 1]], C), call(S).
inference(P, C) :-
	inference([S, [1, 1]], P, C), call(S).


% inference/3

inference([inheritance(M, P), T1], [inheritance(S, M), T2], [inheritance(S, P), T]) :-
	S \= P, f_ded(T1, T2, T).
inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(S, P), T]) :-
	S \= P, f_abd(T1, T2, T).
inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(S, P), T]) :-
	S \= P, f_ind(T1, T2, T).
inference([inheritance(P, M), T1], [inheritance(M, S), T2], [inheritance(S, P), T]) :-
	S \= P, f_exe(T1, T2, T).

inference([inheritance(S, P), T1], [inheritance(P, S), T2], [similarity(S, P), T]) :-
	f_int(T1, T2, T).

inference([inheritance(P, M), T1], [inheritance(S, M), T2], [similarity(S, P), T]) :-
	S \= P, f_com(T1, T2, T).
inference([inheritance(M, P), T1], [inheritance(M, S), T2], [similarity(S, P), T]) :-
	S \= P, f_com(T1, T2, T).
inference([inheritance(M, P), T1], [similarity(S, M), T2], [inheritance(S, P), T]) :-
	S \= P, f_ana(T1, T2, T).
inference([inheritance(P, M), T1], [similarity(S, M), T2], [inheritance(P, S), T]) :-
	S \= P, f_ana(T1, T2, T).
inference([similarity(M, P), T1], [similarity(S, M), T2], [similarity(S, P), T]) :-
	S \= P, f_ded2(T1, T2, T).

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).
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).
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).
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).
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).
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).

inference([inheritance(S, M), T1], [inheritance(int_intersection(L), M), T2], [inheritance(P, M), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(int_intersection(N), P), f_pnn(T1, T2, T).
inference([inheritance(S, M), T1], [inheritance(ext_intersection(L), M), T2], [inheritance(P, M), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(ext_intersection(N), P), f_npp(T1, T2, T).
inference([inheritance(S, M), T1], [inheritance(int_difference(S, P), M), T2], [inheritance(P, M), T]) :-
	atom(S), atom(P), f_pnp(T1, T2, T).
inference([inheritance(S, M), T1], [inheritance(int_difference(P, S), M), T2], [inheritance(P, M), T]) :-
	atom(S), atom(P), f_nnn(T1, T2, T).
inference([inheritance(M, S), T1], [inheritance(M, ext_intersection(L)), T2], [inheritance(M, P), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(ext_intersection(N), P), f_pnn(T1, T2, T).
inference([inheritance(M, S), T1], [inheritance(M, int_intersection(L)), T2], [inheritance(M, P), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(int_intersection(N), P), f_npp(T1, T2, T).
inference([inheritance(M, S), T1], [inheritance(M, ext_difference(S, P)), T2], [inheritance(M, P), T]) :-
	atom(S), atom(P), f_pnp(T1, T2, T).
inference([inheritance(M, S), T1], [inheritance(M, ext_difference(P, S)), T2], [inheritance(M, P), T]) :-
	atom(S), atom(P), f_nnn(T1, T2, T).

inference([implication(M, P), T1], [implication(S, M), T2], [implication(S, P), T]) :-
	S \= P, f_ded(T1, T2, T).
inference([implication(P, M), T1], [implication(S, M), T2], [implication(S, P), T]) :-
	S \= P, f_abd(T1, T2, T).
inference([implication(M, P), T1], [implication(M, S), T2], [implication(S, P), T]) :-
	S \= P, f_ind(T1, T2, T).
inference([implication(P, M), T1], [implication(M, S), T2], [implication(S, P), T]) :-
	S \= P, f_exe(T1, T2, T).

inference([implication(S, P), T1], [implication(P, S), T2], [equivalence(S, P), T]) :-
	f_int(T1, T2, T).

inference([implication(P, M), T1], [implication(S, M), T2], [equivalence(S, P), T]) :-
	S \= P, f_com(T1, T2, T).
inference([implication(M, P), T1], [implication(M, S), T2], [equivalence(S, P), T]) :-
	S \= P, f_com(T1, T2, T).
inference([implication(M, P), T1], [equivalence(S, M), T2], [implication(S, P), T]) :-
	S \= P, f_ana(T1, T2, T).
inference([implication(P, M), T1], [equivalence(S, M), T2], [implication(P, S), T]) :-
	S \= P, f_ana(T1, T2, T).
inference([equivalence(M, P), T1], [equivalence(S, M), T2], [equivalence(S, P), T]) :-
	S \= P, f_ded2(T1, T2, T).

inference([implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]) :-
	S \= P, reduce(disjunction([P, S]), N), f_int(T1, T2, T).
inference([implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]) :-
	S \= P, reduce(conjunction([P, S]), N), f_uni(T1, T2, T).
inference([implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]) :-
	S \= P, reduce(conjunction([P, S]), N), f_int(T1, T2, T).
inference([implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]) :-
	S \= P, reduce(disjunction([P, S]), N), f_uni(T1, T2, T).

inference([implication(S, M), T1], [implication(disjunction(L), M), T2], [implication(P, M), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(disjunction(N), P), f_pnn(T1, T2, T).
inference([implication(S, M), T1], [implication(conjunction(L), M), T2], [implication(P, M), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(conjunction(N), P), f_npp(T1, T2, T).
inference([implication(M, S), T1], [implication(M, conjunction(L)), T2], [implication(M, P), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(conjunction(N), P), f_pnn(T1, T2, T).
inference([implication(M, S), T1], [implication(M, disjunction(L)), T2], [implication(M, P), T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(disjunction(N), P), f_npp(T1, T2, T).

inference([implication(M, P), T1], [M, T2], [P, T]) :-
	ground(P), f_ded(T1, T2, T).
inference([implication(P, M), T1], [M, T2], [P, T]) :-
	ground(P), f_abd(T1, T2, T).
inference([M, T1], [equivalence(S, M), T2], [S, T]) :-
	ground(S), f_ana(T1, T2, T).

inference([P, T1], [S, T2], [C, T]) :-
	C == implication(S, P), f_ind(T1, T2, T).
inference([P, T1], [S, T2], [C, T]) :-
	C == equivalence(S, P), f_com(T1, T2, T).
inference([P, T1], [S, T2], [C, T]) :-
	reduce(conjunction([P, S]), N), N == C, f_int(T1, T2, T).
inference([P, T1], [S, T2], [C, T]) :-
	reduce(disjunction([P, S]), N), N == C, f_uni(T1, T2, T).

inference([S, T1], [conjunction(L), T2], [P, T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(conjunction(N), P), f_pnn(T1, T2, T).
inference([S, T1], [disjunction(L), T2], [P, T]) :-
	ground(S), ground(L), member(S, L), delete(L, S, N), reduce(disjunction(N), P), f_npp(T1, T2, T).

inference([implication(conjunction(L), C), T1], [M, T2], [implication(P, C), T]) :-
	nonvar(L), member(M, L), subtract(L, [M], A), A \= [], reduce(conjunction(A), P), f_ded(T1, T2, T).
inference([implication(conjunction(L), C), T1], [implication(P, C), T2], [M, T]) :-
	member(M, L), subtract(L, [M], A), A \= [], reduce(conjunction(A), P), f_abd(T1, T2, T).
inference([implication(conjunction(L), C), T1], [M, T2], [S, T]) :-
	S == implication(conjunction([M|L]), C), f_ind(T1, T2, T).

inference([implication(conjunction(Lm), C), T1], [implication(A, M), T2], [implication(P, C), T]) :-
	nonvar(Lm), replace(Lm, M, La, A), reduce(conjunction(La), P), f_ded(T1, T2, T).
inference([implication(conjunction(Lm), C), T1], [implication(conjunction(La), C), T2], [implication(A, M), T]) :-
	nonvar(Lm), replace(Lm, M, La, A), f_abd(T1, T2, T).
inference([implication(conjunction(La), C), T1], [implication(A, M), T2], [implication(P, C), T]) :-
	nonvar(La), replace(Lm, M, La, A), reduce(conjunction(Lm), P), f_ind(T1, T2, T).

inference([A1, T1], [A2, T2], [C, T]) :-
	implication([A1, A2], C), f_ded(T1, T2, T).

inference([inheritance(M, P), T1], [inheritance(M, S), T2], [implication(inheritance(X, S), inheritance(X, P)), T]) :-
	S \= P, f_ind(T1, T2, T).
inference([inheritance(P, M), T1], [inheritance(S, M), T2], [implication(inheritance(P, X), inheritance(S, X)), T]) :-
	S \= P, f_abd(T1, T2, T).
inference([inheritance(M, P), T1], [inheritance(M, S), T2], [equivalence(inheritance(X, S), inheritance(X, P)), T]) :-
	S \= P, f_com(T1, T2, T).
inference([inheritance(P, M), T1], [inheritance(S, M), T2], [equivalence(inheritance(P, X), inheritance(S, X)), T]) :-
	S \= P, f_com(T1, T2, T).
inference([inheritance(M, P), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)]), T]) :-
	S \= P, f_int(T1, T2, T).
inference([inheritance(P, M), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))]), T]) :-
	S \= P, f_int(T1, T2, T).

inference([implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [implication(conjunction([A, inheritance(X, S)]), inheritance(X, P)), T]) :-
	S \= P, M1 == M2, A \= inheritance(M2, S), f_ind(T1, T2, T).
inference([implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [conjunction([implication(A, inheritance(var(Y, []), P)), inheritance(var(Y, []), S)]), T]) :-
	S \= P, M1 == M2, A \= inheritance(M2, S), f_int(T1, T2, T).
inference([conjunction(L1), T1], [inheritance(M, S), T2], [implication(inheritance(Y, S), conjunction([inheritance(Y, P2)|L3])), T]) :-
	subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, dependent(P, Y, P2), dependent(L2, Y, L3), f_ind(T1, T2, T).
inference([conjunction(L1), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)|L2]), T]) :-
	subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, f_int(T1, T2, T).

inference([implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [implication(conjunction([A, inheritance(P, X)]), inheritance(S, X)), T]) :-
	S \= P, M1 == M2, A \= inheritance(S, M2), f_abd(T1, T2, T).
inference([implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [conjunction([implication(A, inheritance(P, var(Y, []))), inheritance(S, var(Y, []))]), T]) :-
	S \= P, M1 == M2, A \= inheritance(S, M2), f_int(T1, T2, T).
inference([conjunction(L1), T1], [inheritance(S, M), T2], [implication(inheritance(S, Y), conjunction([inheritance(P2, Y)|L3])), T]) :-
	subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, dependent(P, Y, P2), dependent(L2, Y, L3), f_abd(T1, T2, T).
inference([conjunction(L1), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))|L2]), T]) :-
	subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, f_int(T1, T2, T).

inference([conjunction(L1), T1], [inheritance(M, S), T2], [C, T]) :-
	subtract(L1, [inheritance(var(N, D), S)], L2), L1 \= L2, 
	replace_var(L2, var(N, D), L3, M), reduce(conjunction(L3), C), f_ind(T1, T2, T).
inference([conjunction(L1), T1], [inheritance(S, M), T2], [C, T]) :-
	subtract(L1, [inheritance(S, var(N, D))], L2), L1 \= L2, 
	replace_var(L2, var(N, D), L3, M), reduce(conjunction(L3), C), f_ind(T1, T2, T).

replace_var([], _, [], _).
replace_var([inheritance(S1, P)|T1], S1, [inheritance(S2, P)|T2], S2) :-
	replace_var(T1, S1, T2, S2).
replace_var([inheritance(S, P1)|T1], P1, [inheritance(S, P2)|T2], P2) :-
	replace_var(T1, P1, T2, P2).
replace_all([H|T1], H1, [H|T2], H2) :-
	replace_var(T1, H1, T2, H2).



%%% literial truth in Narsese:

% inheritance

inheritance(ext_intersection(Ls), P) :-
	include([P], Ls).
inheritance(S, int_intersection(Lp)) :-
	include([S], Lp).
inheritance(ext_intersection(S), ext_intersection(P)) :-
	include(P, S), P \= [_].
inheritance(int_intersection(S), int_intersection(P)) :-
	include(S, P), S \= [_].

inheritance(ext_difference(S, P), S) :-
	ground(S), ground(P).
inheritance(S, int_difference(S, P)) :-
	ground(S), ground(P).

inheritance(ext_set(S), ext_set(P)) :-
	include(S, P).
inheritance(int_set(S), int_set(P)) :-
	include(P, S).

inheritance(product(L1), R) :-
	ground(L1), member(ext_image(R, L2), L1), replace(L1, ext_image(R, L2), L2).
inheritance(R, product(L1)) :-
	ground(L1), member(int_image(R, L2), L1), replace(L1, int_image(R, L2), L2).

% similarity

similarity(X, Y) :-
	ground(X), reduce(X, Y), X \== Y, !.

similarity(ext_intersection(L1), ext_intersection(L2)) :-
	same_set(L1, L2).
similarity(int_intersection(L1), int_intersection(L2)) :-
	same_set(L1, L2).
similarity(ext_set(L1), ext_set(L2)) :-
	same_set(L1, L2).
similarity(int_set(L1), int_set(L2)) :-
	same_set(L1, L2).

% implication

implication(similarity(S, P), inheritance(S, P)).
implication(equivalence(S, P), implication(S, P)).

implication(inheritance(S, P), inheritance(ext_intersection(Ls), ext_intersection(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
implication(inheritance(S, P), inheritance(int_intersection(Ls), int_intersection(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
implication(similarity(S, P), similarity(ext_intersection(Ls), ext_intersection(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
implication(similarity(S, P), similarity(int_intersection(Ls), int_intersection(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).

implication(inheritance(S, P), inheritance(ext_difference(S, M), ext_difference(P, M))):-
	ground(M).
implication(inheritance(S, P), inheritance(int_difference(S, M), int_difference(P, M))):-
	ground(M).
implication(similarity(S, P), similarity(ext_difference(S, M), ext_difference(P, M))):-
	ground(M).
implication(similarity(S, P), similarity(int_difference(S, M), int_difference(P, M))):-
	ground(M).
implication(inheritance(S, P), inheritance(ext_difference(M, P), ext_difference(M, S))):-
	ground(M).
implication(inheritance(S, P), inheritance(int_difference(M, P), int_difference(M, S))):-
	ground(M).
implication(similarity(S, P), similarity(ext_difference(M, P), ext_difference(M, S))):-
	ground(M).
implication(similarity(S, P), similarity(int_difference(M, P), int_difference(M, S))):-
	ground(M).

implication(inheritance(S, P), negation(inheritance(S, ext_difference(M, P)))) :-
	ground(M).
implication(inheritance(S, ext_difference(M, P)), negation(inheritance(S, P))) :-
	ground(M).
implication(inheritance(S, P), negation(inheritance(int_difference(M, S), P))) :-
	ground(M).
implication(inheritance(int_difference(M, S), P), negation(inheritance(S, P))) :-
	ground(M).

implication(inheritance(S, P), inheritance(ext_image(S, M), ext_image(P, M))) :-
	ground(M).
implication(inheritance(S, P), inheritance(int_image(S, M), int_image(P, M))) :-
	ground(M).
implication(inheritance(S, P), inheritance(ext_image(M, Lp), ext_image(M, Ls))) :-
	ground(Ls), ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
implication(inheritance(S, P), inheritance(int_image(M, Lp), int_image(M, Ls))) :-
	ground(Ls), ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).

implication(conjunction(L), M) :-
	ground(L), member(M, L).
implication(M, disjunction(L)) :-
	ground(L), member(M, L).

implication(conjunction(L1), conjunction(L2)) :-
	ground(L1), ground(L2), subset(L2, L1).
implication(disjunction(L1), disjunction(L2)) :-
	ground(L1), ground(L2), subset(L1, L2).

implication(negation(M), negation(conjunction(L))) :-
	include([M], L).
implication(negation(disjunction(L)), negation(M)) :-
	include([M], L).

implication([A, negation(conjunction(L))], negation(conjunction(L1))) :-
	ground(A), member(A, L), subtract(L, [A], L1), !, L1 \= [].
implication([negation(A), disjunction(L)], disjunction(L1)) :-
	ground(A), member(A, L), subtract(L, [A], L1), !, L1 \= [].

implication(implication(S, P), implication(conjunction(Ls), conjunction(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
implication(implication(S, P), implication(disjunction(Ls), disjunction(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
implication(equivalence(S, P), equivalence(conjunction(Ls), conjunction(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).
implication(equivalence(S, P), equivalence(disjunction(Ls), disjunction(Lp))):-
	ground(Ls), ground(Lp), replace(Ls, S, L, P), same(L, Lp).


% equivalence

equivalence(X, Y) :-
	ground(X), reduce(X, Y), X \== Y, !.

equivalence(similarity(S, P), similarity(P, S)).

equivalence(inheritance(S, ext_set([P])), similarity(S, ext_set([P]))).
equivalence(inheritance(int_set([S]), P), similarity(int_set([S]), P)).

equivalence(inheritance(S, ext_intersection(Lp)), conjunction(L)) :-
	findall(inheritance(S, P), member(P, Lp), L).
equivalence(inheritance(int_intersection(Ls), P), conjunction(L)) :-
	findall(inheritance(S, P), member(S, Ls), L).

equivalence(inheritance(S, ext_difference(P1, P2)), 
	    conjunction([inheritance(S, P1), negation(inheritance(S, P2))])).
equivalence(inheritance(int_difference(S1, S2), P), 
	    conjunction([inheritance(S1, P), negation(inheritance(S2, P))])).

equivalence(inheritance(product(Ls), product(Lp)), conjunction(L)) :-
	equ_product(Ls, Lp, L).

equivalence(inheritance(product([S|L]), product([P|L])), inheritance(S, P)) :-
	ground(L).
equivalence(inheritance(S, P), inheritance(product([H|Ls]), product([H|Lp]))) :-
	ground(H), equivalence(inheritance(product(Ls), product(Lp)), inheritance(S, P)).

equivalence(inheritance(product(L), R), inheritance(T, ext_image(R, L1))) :-
	replace(L, T, L1).
equivalence(inheritance(R, product(L)), inheritance(int_image(R, L1), T)) :-
	replace(L, T, L1).

equivalence(equivalence(S, P), equivalence(P, S)).

equivalence(equivalence(negation(S), P), equivalence(negation(P), S)).

equivalence(conjunction(L1), conjunction(L2)) :-
	same_set(L1, L2).
equivalence(disjunction(L1), disjunction(L2)) :-
	same_set(L1, L2).

equivalence(implication(S, conjunction(Lp)), conjunction(L)) :-
	findall(implication(S, P), member(P, Lp), L).
equivalence(implication(disjunction(Ls), P), conjunction(L)) :-
	findall(implication(S, P), member(S, Ls), L).

equivalence(T1, T2) :- 
	negation(atom(T1)), negation(atom(T2)), ground(T1), ground(T2),
	T1 =.. L1, T2 =.. L2, equivalence_list(L1, L2).

equivalence_list(L, L).
equivalence_list([H|L1], [H|L2]) :- 
	equivalence_list(L1, L2).
equivalence_list([H1|L1], [H2|L2]) :- 
	similarity(H1, H2), equivalence_list(L1, L2).
equivalence_list([H1|L1], [H2|L2]) :- 
	equivalence(H1, H2), equivalence_list(L1, L2).

% compound term structure reduction

reduce(similarity(ext_set([S]), ext_set([P])), similarity(S, P)) :-
	!.
reduce(similarity(int_set([S]), int_set([P])), similarity(S, P)) :-
	!.

reduce(instance(S, P), inheritance(ext_set([S]), P)) :-
	!.
reduce(property(S, P), inheritance(S, int_set([P]))) :-
	!.
reduce(inst_prop(S, P), inheritance(ext_set([S]), int_set([P]))) :-
	!.

reduce(ext_intersection([T]), T) :-
	!.
reduce(int_intersection([T]), T) :-
	!.

reduce(ext_intersection([ext_intersection(L1), ext_intersection(L2)]), ext_intersection(L)) :-
	union(L1, L2, L), !.
reduce(ext_intersection([ext_intersection(L1), L2]), ext_intersection(L)) :-
	union(L1, [L2], L), !.
reduce(ext_intersection([L1, ext_intersection(L2)]), ext_intersection(L)) :-
	union([L1], L2, L), !.
reduce(ext_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)) :-
	intersection(L1, L2, L), !.
reduce(ext_intersection([int_set(L1), int_set(L2)]), int_set(L)) :-
	union(L1, L2, L), !.

reduce(int_intersection([int_intersection(L1), int_intersection(L2)]), int_intersection(L)) :-
	union(L1, L2, L), !.
reduce(int_intersection([int_intersection(L1), L2]), int_intersection(L)) :-
	union(L1, [L2], L), !.
reduce(int_intersection([L1, int_intersection(L2)]), int_intersection(L)) :-
	union([L1], L2, L), !.
reduce(int_intersection([int_set(L1), int_set(L2)]), int_set(L)) :-
	intersection(L1, L2, L), !.
reduce(int_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)) :-
	union(L1, L2, L), !.

reduce(ext_difference(ext_set(L1), ext_set(L2)), ext_set(L)) :-
	subtract(L1, L2, L), !.
reduce(int_difference(int_set(L1), int_set(L2)), int_set(L)) :-
	subtract(L1, L2, L), !.

reduce(product(product(L), T), product(L1)) :- 
	append(L, [T], L1), !.

reduce(ext_image(product(L1), L2), T1) :-
	member(T1, L1), replace(L1, T1, L2), !.
reduce(int_image(product(L1), L2), T1) :-
	member(T1, L1), replace(L1, T1, L2), !.

reduce(negation(negation(S)), S) :-
	!.

reduce(conjunction([T]), T) :-
	!.
reduce(disjunction([T]), T) :-
	!.

reduce(conjunction([conjunction(L1), conjunction(L2)]), conjunction(L)) :-
	union(L1, L2, L), !.
reduce(conjunction([conjunction(L1), L2]), conjunction(L)) :-
	union(L1, [L2], L), !.
reduce(conjunction([L1, conjunction(L2)]), conjunction(L)) :-
	union([L1], L2, L), !.

reduce(disjunction(disjunction(L1), disjunction(L2)), disjunction(L)) :-
	union(L1, L2, L), !.
reduce(disjunction(disjunction(L1), L2), disjunction(L)) :-
	union(L1, [L2], L), !.
reduce(disjunction(L1, disjunction(L2)), disjunction(L)) :-
	union([L1], L2, L), !.

reduce(X, X).


%%% Argument processing

equ_product([], [], []).
equ_product([T|Ls], [T|Lp], L) :-
	equ_product(Ls, Lp, L), !.
equ_product([S|Ls], [P|Lp], [inheritance(S, P)|L]) :-
	equ_product(Ls, Lp, L).

same_set(L1, L2) :-
	L1 \== [], L1 \== [_], same(L1, L2), L1 \== L2.

same([], []).
same(L, [H|T]) :-
	member(H, L), subtract(L, [H], L1), same(L1, T).

include(L1, L2) :-
	ground(L2), include1(L1, L2), L1 \== [], L1 \== L2.

include1([],_).
include1([H|T1],[H|T2]) :-
	include1(T1,T2).
include1([H1|T1],[H2|T2]) :- 
	H2 \== H1, include1([H1|T1], T2).

not_member(_, []).
not_member(C, [C|_]) :- !, fail.
not_member([S, T], [[S1, T]|_]) :- equivalence(S, S1), !, fail.
not_member(C, [_|L]) :- not_member(C, L).

replace([T|L], T, [nil|L]).
replace([H|L], T, [H|L1]) :-
	replace(L, T, L1).

replace([H1|T], H1, [H2|T], H2).
replace([H|T1], H1, [H|T2], H2) :-
	replace(T1, H1, T2, H2).

dependent(var(V, L), Y, var(V, [Y|L])) :-
	!.
dependent([H|T], Y, [H1|T1]) :-
	dependent(H, Y, H1), dependent(T, Y, T1), !.
dependent(inheritance(S, P), Y, inheritance(S1, P1)) :-
	dependent(S, Y, S1), dependent(P, Y, P1), !.
dependent(ext_image(R, A), Y, ext_image(R, A1)) :-
	dependent(A, Y, A1), !.
dependent(int_image(R, A), Y, int_image(R, A1)) :-
	dependent(A, Y, A1), !.
dependent(X, _, X).


%%% Truth-value functions

f_exp([F, C], E) :- 
	E is C * (F - 0.5) + 0.5.

f_rev([F1, C1], [F2, C2], [F, C]) :- 
	M1 is C1 / (1 - C1), 
	M2 is C2 / (1 - C2),
	F is (M1 * F1 + M2 * F2) / (M1 + M2),
	C is (M1 + M2) / (M1 + M2 + 1).

f_cnv([F0, C0], [1, C]) :- 
	u_w2c(F0 * C0, C).

f_cnt([F0, C0], [0, C]) :- 
	u_w2c((1 - F0) * C0, C).
	
f_ded([F1, C1], [F2, C2], [F, C]) :- 
	u_and([F1, F2], F),
	u_and([C1, C2, F], C).

f_ded2([F1, C1], [F2, C2], [F, C]) :- 
	u_and([F1, F2], F),
	u_or([F1, F2], F0),
	u_and([C1, C2, F0], C).

f_abd([F1, C1], [F2, C2], [F2, C]) :- 
	u_and([F1, C1, C2], W),
	u_w2c(W, C).
	
f_ind(T1, T2, T) :- 
	f_abd(T2, T1, T).

f_exe([F1, C1], [F2, C2], [1, C]) :- 
	u_and([F1, C1, F2, C2], W),
	u_w2c(W, C).

f_com([0, _C1], [0, _C2], [0, 0]). 
f_com([F1, C1], [F2, C2], [F, C]) :- 
	u_or([F1, F2], F0),
	F0 > 0,
	F is F1 * F2 / F0,
	u_and([F0, C1, C2], W),
	u_w2c(W, C).

f_ana([F1, C1], [F2, C2], [F, C]) :- 
	F is F1 * F2,
	C is C1 * F2 * F2 * C2 * C2.

f_int([F1, C1], [F2, C2], [F, C]) :- 
	u_and([F1, F2], F),
	u_not(F1, F1n),
	u_not(F2, F2n),
	u_and([F1n, C1], X1),
	u_and([F2n, C2], X2),
	u_and([C1, C2], X3),

	u_or([X1, X2, X3], C).

f_uni([F1, C1], [F2, C2], [F, C]) :- 
	u_or([F1, F2], F),
	u_and([F1, C1], X1),
	u_and([F2, C2], X2),
	u_and([C1, C2], X3),

	u_or([X1, X2, X3], C).

f_dif([F1, C1], [F2, C2], [F, C]) :- 
	u_not(F1, F1n),
	u_not(F2, F2n),
	u_and([F1, F2n], F),
	u_and([F1n, C1], X1),
	u_and([F2, C2], X2),
	u_and([C1, C2], X3),

	u_or([X1, X2, X3], C).

f_pnn([F1, C1], [F2, C2], [F, C]) :- 
	u_not(F2, F2n),
	u_and([F1, F2n], Fn),
	u_not(Fn, F),
	u_and([Fn, C1, C2], C).

f_npp([F1, C1], [F2, C2], [F, C]) :- 
	u_not(F1, F1n),
	u_and([F1n, F2], F),
	u_and([F, C1, C2], C).

f_pnp([F1, C1], [F2, C2], [F, C]) :- 
	u_not(F2, F2n),
	u_and([F1, F2n], F),
	u_and([F, C1, C2], C).

f_nnn([F1, C1], [F2, C2], [F, C]) :- 
	u_not(F1, F1n),
	u_not(F2, F2n),
	u_and([F1n, F2n], Fn),
	u_not(Fn, F),
	u_and([Fn, C1, C2], C).

f_neg([F0, C0], [F, C0]) :- 
	u_not(F0, F).

% Utility functions

u_not(N0, N) :-
	N is (1 - N0), !.

u_and([N0], N0).
u_and([N0 | Nt], N) :-
	u_and(Nt, N1), N is N0 * N1, !.

u_or([N0], N0).
u_or([N0 | Nt], N) :-
	u_or(Nt, N1), N is (N0 + N1 - N0 * N1), !.

u_w2c(W, C) :-
	K = 1, C is (W / (W + K)), !.


