% File : pfcjust.pl
% Author : Tim Finin, finin@prc.unisys.com
% Author : Dave Matuszek, dave@prc.unisys.com
% Updated:
% Purpose: predicates for accessing Pfc justifications.
% Status: more or less working.
% Bugs:
%% *** predicates for exploring supports of a fact *****
:- use_module(library(lists)).
justification(F,J) :- supports(F,J).
justifications(F,Js) :- bagof(J,justification(F,J),Js).
%% base(P,L) - is true iff L is a list of "base" facts which, taken
%% together, allows us to deduce P. A base fact is an axiom (a fact
%% added by the user or a raw Prolog fact (i.e. one w/o any support))
%% or an assumption.
base(F,[F]) :- (axiom(F) ; assumption(F)),!.
base(F,L) :-
% i.e. (reduce 'append (map 'base (justification f)))
justification(F,Js),
bases(Js,L).
%% bases(L1,L2) is true if list L2 represents the union of all of the
%% facts on which some conclusion in list L1 is based.
bases([],[]).
bases([X|Rest],L) :-
base(X,Bx),
bases(Rest,Br),
pfcUnion(Bx,Br,L).
axiom(F) :-
pfcGetSupport(F,(user,user));
pfcGetSupport(F,(god,god)).
%% an assumption is a failed goal, i.e. were assuming that our failure to
%% prove P is a proof of not(P)
assumption(P) :- pfc_negation(P,_).
%% assumptions(X,As) if As is a set of assumptions which underly X.
assumptions(X,[X]) :- assumption(X).
assumptions(X,[]) :- axiom(X).
assumptions(X,L) :-
justification(X,Js),
assumptions1(Js,L).
assumptions1([],[]).
assumptions1([X|Rest],L) :-
assumptions(X,Bx),
assumptions1(Rest,Br),
pfcUnion(Bx,Br,L).
%% pfcProofTree(P,T) the proof tree for P is T where a proof tree is
%% of the form
%%
%% [P , J1, J2, ;;; Jn] each Ji is an independent P justifier.
%% ^ and has the form of
%% [J11, J12,... J1n] a list of proof trees.
% pfcChild(P,Q) is true iff P is an immediate justifier for Q.
% mode: pfcChild(+,?)
pfcChild(P,Q) :-
pfcGetSupport(Q,(P,_)).
pfcChild(P,Q) :-
pfcGetSupport(Q,(_,Trig)),
pfcType(Trig,trigger),
pfcChild(P,Trig).
pfcChildren(P,L) :- bagof(C,pfcChild(P,C),L).
% pfcDescendant(P,Q) is true iff P is a justifier for Q.
pfcDescendant(P,Q) :-
pfcDescendant1(P,Q,[]).
pfcDescendant1(P,Q,Seen) :-
pfcChild(X,Q),
(\+ member(X,Seen)),
(P=X ; pfcDescendant1(P,X,[X|Seen])).
pfcDescendants(P,L) :-
bagof(Q,pfcDescendant1(P,Q,[]),L).