/* Version: 1.00 - Date: 16/11/03 - File: belief.pl Written for "Eclipse 5.4 #27". Purpose: The belief revision component of FLUX kernel Author: Jin Yi Usage: In this version of implementation, we only handle propositional formulas. From now onwards, we refer a formula to a propositional formula. Belief base is represented as a finite consistent list: [F1@E1,...,Fn@En], where Fi is a non-tautology formula, and Ei is a real number within (0,1]. Ei is called the belief degree(which can be considered as degree of evidence) of formula Fi. Let B a belief base, the belief degree E of any formula F (which may not occur in B), can be quired by "?- rankRedundant(F,0,E,B)". If B is nonredundant, we also can use the more efficient version "?- rank(F,0,E,B)". A tautology will always be assigned a degree of 2. The contraction of nonredundant belief base B with any formula F can be computed by "?- contract(B,F,B1)", where B1 is the resultant belief base. The revision of nonredundant belief base with any consistent formula F (which can be considered as additional evidence if F is already believed in B) with new belief degree E, can be computed by "?- revise(B,F@E,B1)", where B1 is the resultant belief base. A nonredundant belief base B1 can be obtained from a redundant base B via "?- removeRedundant(B,B1)". Any nonredundant belief base is contracted or revised by some formula will result in a nonredundant belief base. A belief base B's consistency can be checked by "?- consistent(B)" */ :- lib(lists). %% Declare '@' as an infix binary function, which is used to annotate a %% formula F with its belief degree E. :- op(1150,xfx,@). %% Load the non-clausal decision procedure for propositional logic, %% which is available at http://www.intellektik.informatik.tu-darmstadt.de/~jeotten/ncDP/ :-[ncDP]. %% Logic connectives :- op(1000, xfy, [&]). /* Conjunction */ :- op(1050, xfy, [v]). /* Disjunction */ :- op(500,fy,[-]). /* Negation */ %% Those are already defined in ncDP %:- op(1110, xfy, [=>]). /* Implication */ %:- op(1130,xfy, [<=>]). /* Equivalence */ %% Transfer a formula to the syntax required by ncDP. transform(F1 & F2, (F1P)','(F2P)) :- transform(F1,F1P),transform(F2,F2P),!. transform(F1 v F2, (F1P)';'(F2P)) :- transform(F1,F1P),transform(F2,F2P),!. transform(F1 => F2,(F1P)=>(F2P)) :- transform(F1,F1P),transform(F2,F2P),!. transform(F1 <=> F2, (F1P)<=>(F2P)) :- transform(F1,F1P),transform(F2,F2P),!. transform(-F, ~(FP) ) :- transform(F,FP),!. transform(F,F). myprove(F) :- transform(F,F1),prove(F1). %% atLeastDegree(B,E,FL), FL contains all formulas in B with belief degree %% at lest E. atLeastDegree([],_,[]). atLeastDegree([F1@E1|B],E,FL) :- atLeastDegree(B,E,FL1), ( E1>=E -> FL = [F1|FL1]; FL = FL1 ). %% degreeList(B,EL), EL contains all belief degrees which occur in B degreeList([],[]). degreeList([_@E|B],EL) :- degreeList(B,EL1), ( member(E,EL1) -> EL=EL1; EL=[E|EL1] ). %% conjunction(FL,C), C is the conjunction of all formulas in FL conjunction([],a v -(a)). conjunction([F|FL],C) :- conjunction(FL,C1),C=(F&(C1)). %% Yes if FL |- F, no otherwise deduce(FL,F) :- conjunction(FL,FLC), myprove(((FLC)=>F)). %% rankRedundant(F,E1,E,B), if formula F is at least degree E1, then E is its belief degree, otherwise E=0. %% Note, a tautology gets degree 2. rankRedundant(F,E1,E,B) :- myprove((F)) -> E=2; degreeList(B,EL1), sort(EL1,EL2), reverse(EL2,EL), ( member(E,EL),E>=E1,atLeastDegree(B,E,FL),deduce(FL,F) -> true; E=0 ). %% rank(F,E1,E,B), if formula F is at least degree E1, then E is its belief degree, otherwise E=0. %% Note, B here should be redundant free. rank(F,_,E,B) :- member(F@E,B),!. rank(F,E1,E,B) :- rankRedundant(F,E1,E,B). %% Check the consistency of the belief base. consistent(B) :- atLeastDegree(B,0,FL), \+ deduce(FL,a&(-(a))). %% Remove all redundant elements of the belief base, in the sense, %% a formula F with belief degree E is redundant, if a higher or %% equal degree of F can be induced from the rest of base. removeRedundant(B,B1) :- nonredundant(B,B,B1). nonredundant([],B,B). nonredundant([F@E|B],BRest,B1) :- delete(F@E,BRest,BRest1), ( rankRedundant(F,E,E1,BRest1), E1>=E -> nonredundant(B,BRest1,B1); nonredundant(B,BRest,B1) ). %% mydelete(B,F,B1), remove formula F from belief base B mydelete([],_,[]). mydelete([FE|B],F,B1) :- FE=..[@,F,_] -> mydelete(B,F,B1); mydelete(B,F,B2), B1=[FE|B2]. %% make the belief degree of formula F to be E update(B,F@E,B1) :- mydelete(B,F,B2),B1=[F@E|B2]. %% expand(B,F@E,B1), expands B with formula F and degree E. expand(B,F@E,B1) :- ( rank((-(F)),0,E1,B),E1>0; rank(F,E,E1,B),E1>=E ) ->B1=B; rank(F,0,E1,B), update(B,F@E,B2), expandFilter(B2,B2,E1,E,B1). %% expandFilter(B,B,E1,E2,B1), filter out redundant formula with degree %% between E1 and E2. expandFilter([],B,_,_,B). expandFilter([F@E|B],BRest,E1,E2,B1) :- delete(F@E,BRest,BRest1), ( ( E>E2; E expandFilter(B,BRest,E1,E2,B1); expandFilter(B,BRest1,E1,E2,B1) ). %% contract(B,F,B1), contract formula F from belief base. contract(B,F,B1) :- (myprove((F)); rank(F,0,E,B),E=0) -> B1=B; rank(F,0,E,B), contractFilter(B,B,F,E,B1). %% contractFilter(B,B,F,E,B1), filter out all redundant formula with %% belief degree =< E, and add F=>E if necessary. contractFilter([],B,_,_,B). contractFilter([F1@E1|B],BRest,F,E,B1) :- delete(F1@E1,BRest,BRest1), ( ( E1>E; rank( (F1) v (F) ,E,E2,BRest1), E2>E ) -> contractFilter(B,BRest,F,E,B1); ( E1 (F1),E1,E3,BRest1), E3 contractFilter(B,[((F) => (F1))@E1|BRest1],F,E,B1); contractFilter(B,BRest1,F,E,B1) ). %% Revision is defined via Levi Identity. revise(B,F@E,B1) :- contract(B,(-(F)),B2), expand(B2,F@E,B1). /* Examples Example Revision Z=[a=>b@0.3], revise(Z,-b@0.2,Z1), revise(Z1,a@0.1,Z2). Example Expansion Z=[], expand(Z,a v b@0.4,Z1), expand(Z1,a@0.2,Z2), expand(Z2,a v c@0.1,Z3),expand(Z3,a&b@0.3,Z4),expand(Z4,-b@0.2,Z5). Example Contraction Z=[a&b=>c@0.3,a@0.2,b@0.1],contract(Z,a,Z1), contract(Z,c,Z2). Z=[a@0.3,b@0.2,a&b=>c@0.1], contract(Z,c,Z1). Z=[a@0.1,b@0.1],contract(Z,a,Z1). Z=[a@0.1,b@0.2], contract(Z,a,Z1). Z=[a@0.1,b@0.2,a v b@0.3], contract(Z,a,Z1). removeRedundant([a@0.1,b@0.2,a@0.3,a v b@0.25],Z). intList(1000,L),test(L,[a v c@0.8, b v c@0.7, a v d@0.4, b v d@0.5, c@0.1, d@0.3, e@0.8, f@0.9, h@0.9],B). intList(1,L),testBase(50,B1),test(L,B1,B). */ %% test facilities test([],B,B). test([H|T],B,B1):- test(T,B,B2), writeln(B2), X is H mod 3, random(N1), N2 is N1 mod 10, N is N2/10, ( X=1 -> revise(B2,a@N,B1); X=2 -> revise(B2,a=>b@N,B1); revise(B2,-b@N,B1) ). intList(0,[]):-!. intList(N,[N|L1]):- N1 is N-1, intList(N1,L1). testBase(0,[]):-!. testBase(N,[N@E|B1]):- random(E1), E2 is E1 mod 10, E is E2/10, N1 is N-1, testBase(N1,B1). %rankRedundant(-(a)<=>l,0,E,[(-(a) v l)@0.3, (a v l)@0.9, (-(a) v -(l))@0.9]) %revise([-(a)@0.2, l@0.2], -(l)@0.5,B). %rankRedundant(a,0,E,[(a v -(l))@0.8, (a v l)@0.9, (-(a) v -(l))@0.9])