/*
	evident_state.pl

	Author:	Luu Tran    
	Last modified:	07/12/96 15:07 

	Simple program to calculate 'evident' for states
*/

:- op( 1200, xfy, ('<-')).
:- op( 500, fy, (~)).

/*
 evident( +State, -ClauseTree)
	top predicate; state is allowed only in root of tree.
	ClauseTree is of form
		Term / ContingecySet <- ClauseTree1, ClauseTree2, ... ClauseTreeK
*/

evident( (P | Q), ((P | Q) / [] <- T) ):-  !,
	disjs_to_list( (P|Q), State),
	(Head <- Body),
	% match clause head with some term in state
	member( Head, State),    
	evident( Body, [State], C, T),
	% contigency minus node itself should be {}
	subtract( C, State, []). 
evident( P, T):-
	evident( P, [], [], T).
	
%  evident( +Term, +Ancestors, -Contingencies, -ClauseTree)

evident( true, _, [], true / []).  % true term
evident( [P|[]], A, C, T):-!,      % single term in body
	evident( P, A, C, T).
evident( [P|R], A, C, ( PT, RT)):- % conjunctive term
	evident( P, A, CP, PT),
	evident( R, A, CR, RT),
	append( CP, CR, C).

% fail if term matches an ancestor (repeat)
evident( P, A, _, _):-             
	P \== true, P \== [_|_],
	match_ancestors( P, A), !, fail.

% check for ancestry resolved
evident( P, A, [N], P/[N]):-       
	P \== true, P \== [_|_],
	negated_term( P, N),
	check_ancestors( N, A).

% match term with some clause
evident( P, A, C, ((P/C) <- BT)):- 
	P \== true, P \== [_|_],
	(P <- Body),
	evident( Body, [P|A], BC, BT),
	reduce_contingency( P, BC, C).

check_ancestors( P, [P|_]):-!.
check_ancestors( P, [L|_]):- member( P, L), !.
check_ancestors( P, [_|R]):- check_ancestors( P, R).

match_ancestors( P, [Q|_]):- P == Q, !.
match_ancestors( P, [L|_]):- member( Q, L), P == Q, !.
match_ancestors( P, [_|R]):- match_ancestors( P, R).

reduce_contingency( P, [Q|R],S):- P == Q,  !, reduce_contingency( P,R,S).
reduce_contingency( P, [Q|R], [Q|S]) :- reduce_contingency( P,R,S).
reduce_contingency( _, [], []).

negated_term( ~P, P):-!.
negated_term( P, ~P).

disjs_to_list( (A|R), [A|L]):- disjs_to_list( R, L).
disjs_to_list( A, [A]):- A \= (_|_).


/*
	Sample program

	a(X) | b(X) <- c(X), d(X).
	c(X) | a(X).
	d(X) <- e(X).
	e(1).	e(2).
	g(X,_) <- a(X).
	g(_,X) <- b(X).
	~d(2) <- g(1,1).

	(Contrapositives for disjunctive clauses manually converted)
*/

a(X) <- [~ b(X), c(X), d(X)].
b(X) <- [~ a(X), c(X), d(X)].
~ c(X) <- [~ a(X), ~ b(X), d(X)].
~ d(X) <- [~ a(X), ~ b(X), c(X)].

c(X) <- [~a(X)].		a(X) <- [~c(X)].
d(X) <- [e(X)].		~e(X) <- [~d(X)].
e(1) <- [true].		e(2) <- [true].

g(X,_) <- [a(X)].		~a(X) <- [~g(X,_)].
g(_,X) <- [b(X)].		~b(X) <- [~g(_,X)].

~d(2) <- [g(1,1)].	~g(1,1) <- [d(2)].

===================================

Sample output (reformatted for readability).

?- evident(g(X,X), T). 
T = g(1, 1) / [] <- 
       a(1) / [g(1, 1)] <- 
            ((~ b(1)) / [g(1, 1)] 
                <- (~ g(1, 1)) / [g(1, 1)])
          , (c(1) / [a(1)] 
                <- (~ a(1)) / [a(1)])
          , (d(1) / [] 
                <- e(1) / [] <- 
                      true / [])
X = 1
Yes

?- evident((a(1)|b(1)), T).
T = (a(1) | b(1)) / [] <- 
          (~ b(1)) / [b(1)]
        , (c(1) / [a(1)] <- 
             (~ a(1)) / [a(1)])
        , (d(1) / [] <- 
             e(1) / [] <- 
                  true / [])
Yes