/* ------ Start the Program: dr(Listofsentences,Resultlist) dorevision(Listofsentences,Result) some simple examples: dr([a,imp(a,b)],X) dr([a,bar(a)],X) dr([a,bar(a),bar(bar(a))],X) dr([dis([a,b]),dis([a,bar(b)])],X) depending on the prolog system used, these queries have to be adapted by putting a '.' or '?' at the end... ------*/ /*connectives allowed in the language: nott(_), bar(_), imp(_,_), con([_]), dis([_]); valid(sentence) tests for validity of the sentence*/ valid(A):-atom(A). valid(nott(A)):-valid(A). valid(imp(A,B)):-valid(A),valid(B). valid(con(X)):-length(X,Y), Y>1, validlist(X). valid(dis(X)):-length(X,Y), Y>1, validlist(X). valid(bar(A)):-valid(A). /*valid([sentence]) tests for validity of a list of sentences*/ validlist([]). validlist([X|R]):-valid(X),validlist(R). /*abbreviations for starting the revision dr([Sentence], [[Sentence,Valuerestriction]]) right now the Result is a List of sentences with their evaluation in the 8-valued logic dorevision has the same type it checks validity of the inputsentences, brings them into a semi-normal form and triggers the calculation if you don't need the result of the revision, you can omit the second argument in dr */ dr(X):-dorevision(X,R). dr(X,R):-dorevision(X,R). dorevision(X,R):-validlist(X),nfl(X,Y), calculate(Y,[],R), sort(R,Z),writeln(Z). /*calculate ([Sentence], [[Sentence,Valuerestriction]], [[Sen.,Valuerestr.]]) 2nd argument is the intermediate Result calculated so far 3rd the final Result manages the belief revision procedure*/ /*if nothing is to be added, the intermediate result is the final one*/ calculate([], Intermediate, Intermediate). /*if something is to be added, calculate the result of the rest of the list, and then update that result with the head As the sentence is supposed to be true, its evaluation to 3 is passed on to update(_,_,_). if this update does not give an error, take the result of the update*/ calculate([H|Rest], Intermediate,Y):- calculate(Rest, Intermediate, Finalresult), update(Finalresult, [H, 3], Resultlist), (member([X,0],Resultlist)-> write('\n Integration of '), write(H), writeln(' leads to inconsistency.'), Y=Finalresult;Y=Resultlist), writeln(Y). /*update([[S.,V.]], [S.,V.], [[S.,V.]],Error) expands the sentence by which the intermediate result is to be extended, infers restrictions on its subsentences and then updates the intermediate result by this list the Error-flag received by updatebl is passed on to calculate(_,_,_)*/ update(Intermediate, [H,X], Result):- expand([H,X], List), infer1(List, List2), updatebl(Intermediate, List2, Result). /*updatebl([[S.,V.]], [[S.,V.]], [[S.,V.]], Error) appends the intermediate result and the list by which it is to be updated and runs an inference procedure on the list obtained.*/ updatebl(List1, List2, Result):-append(List1,List2,Inter), infer1(Inter,Result). /*nf(Sentence,SentenceInSemiNormalForm) transfers sentences into a semi-normal form which is supposed to simplify equivalence checks between sentences negations are brought as far into the sentence as possible double negations are eliminated*/ nf(A,A):-atom(A). nf(nott(A),nott(A)):-atom(A). nf(con(X),con(E)):-nfl(X,Z), contransform(Z,W), throwoutdup2(W,Y), contransform(Y,E). nf(dis(X),dis(E)):-nfl(X,Z), distransform(Z,W), throwoutdup2(W,Y), distransform(Y,E). nf(imp(A,B),imp(C,D)):-nf(A,C),nf(B,D). nf(bar(A),bar(B)):-nf(A,B). nf(nott(nott(A)),B):-nf(A,B). nf(nott(con(X)),E):-nottransform(X,W), nf(dis(W),E). nf(nott(dis(X)),E):-nottransform(X,W), nf(con(W),E). nf(nott(bar(A)),nott(bar(B))):-nf(A,B). nf(nott(imp(A,B)),nott(imp(C,D))):-nf(A,C),nf(B,D). /*nfl([Sentence],[SentenceInSemiNormalForm])*/ nfl([],[]). nfl([A|X],[B|Y]):-nf(A,B),nfl(X,Y). /*nottransform([sentence],[sentence]) negates all sentences in a given list*/ nottransform([],[]). nottransform([X|R],[nott(X)|Y]):-nottransform(R,Y). /*distransform([sentence],[sentence]) flattens disjunctions if there are further disjunctions within another, the lists are appended, as disjunction is commutative and associative, all other connectives stay untouched*/ distransform([],[]). distransform([dis(X)|R],Y):-distransform(R,Z), append(X,Z,Y). distransform([con(X)|R],Y):-distransform(R,Z), append([con(X)],Z,Y). distransform([bar(X)|R],Y):-distransform(R,Z), append([bar(X)],Z,Y). distransform([imp(A,B)|R],Y):-distransform(R,Z), append([imp(A,B)],Z,Y). distransform([nott(X)|R],Y):-distransform(R,Z), append([nott(X)],Z,Y). distransform([X|R],Y):-atom(X),distransform(R,Z), append([X],Z,Y). /*the same with conjunction*/ contransform([],[]). contransform([con(X)|R],Y):-contransform(R,Z), append(X,Z,Y). contransform([dis(X)|R],Y):-contransform(R,Z), append([dis(X)],Z,Y). contransform([bar(X)|R],Y):-contransform(R,Z), append([bar(X)],Z,Y). contransform([imp(A,B)|R],Y):-contransform(R,Z), append([imp(A,B)],Z,Y). contransform([nott(X)|R],Y):-contransform(R,Z), append([nott(X)],Z,Y). contransform([X|R],Y):-atom(X),contransform(R,Z), append([X],Z,Y). /*throwoutdup2(Sentence,[Sentence]) eliminates duplicates*/ throwoutdup2([],[]). /*if there is a duplicate of the head of the list in the tail of the list, the result is the rest of the list with eliminated duplicates, if there is no duplicate of the head in the tail, append the head to the rest of the list which has been cleared of duplicates*/ throwoutdup2([X|Rest],Z):- chkdup2(X,Rest,1) -> throwoutdup2(Rest,Z); (throwoutdup2(Rest, Inter), append([X],Inter,Z)). /*chkdup2(Sentence,[Sentence], Flag) checks whether element or equivalent appear*/ chkdup2(X, [], 0). chkdup2(X, [Y|Rest],Flag):- eq(X,Y) -> Flag = 1,!; chkdup2(X,Rest,Flag). /*eq(Sentence, EquivalentSentence) checks two sentences for equivalence this predicate is one of the essential ones still to be extended because much of the inference depends on recognising eqivalence !!!!!!!!!!!!!!!!!!!to be worked on!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*/ eq(A,A). eq(nott(nott(A)),B):-eq(A,B). eq(A,nott(nott(B))):-eq(A,B). %eq(A,B):-eq(B,A),!. eq(bar(A),bar(B)):-eq(A,B). eq(nott(A),nott(B)):-eq(A,B). eq(con(X),con(Y)):-eqsen(X,Y). eq(dis(X),dis(Y)):-eqsen(X,Y). eq(nott(con(A,B)),dis(nott(A),nott(B))). eq(nott(dis(A,B)),con(nott(A),nott(B))). /*eqsen([sentence],[sentence]) checks whether two lists contain the same (eqivalent) sentences by testing mutual inclusion*/ eqsen(X,Y):-exin(X,Y),exin(Y,X). /*exin([sentence],[sentence]) tests inclusion of the first list in the second*/ exin([],X). exin([X|R1],[Y|R2]):-eq(X,Y),exin(R1,[Y|R2]). exin([X|R1],[Y|R2]):-exin([X],R2),exin(R1,[Y|R2]). /*move X to the back of a list, needed for the inference procedure, as several formulas might have the same structure, but update is run only on the first one found in order to stop backtracking, formulas have to be moved to the back, so that the other ones will be found in the next update run */ mtb(X,[],[X]). mtb(X,[E|Rest],Y):-(X=E -> mtb(X,Rest,Y); mtb(X,Rest,Bla), append([E],Bla,Y)). /*imported*/ powerset([],[[]]). powerset([H|T],PowerSet):- powerset(T,PowerSetOfT), extend_pset(H,PowerSetOfT,PowerSet). extend_pset(_,[],[]). extend_pset(H,[List|MoreLists],[List,[H|List]|More]):- extend_pset(H,MoreLists,More). kopf([X|R],X). /*end imported*/ /*expandsub([S.],V.,[[S.,V.]]) expands all subsentences in a list of sentences and adds evaluation restrictions*/ expandsub([],Val,[]). expandsub([X|Rest],Val,Erg):-expand([X,Val],Inter), expandsub(Rest,Val,Inter2), append(Inter,Inter2,Erg). /*expandlist(Type,[S.],V.,[[S.,V.]]) Type is c for conjunction and d for disjunction creates all subconjunctions and subdisjunctions by creating the powerset of the elements and then calling puttogether which brings them into the right form, and then triggers the expansion of their subsentences*/ expandlist(E,X,Val,Y):-length(X,Lx), powerset(X,Z), puttogether(E,Lx,Z,Val,Y1), expandsub(X,Val,Y2), append(Y1,Y2,Y). /*puttogether(Type, Length, [S.], V.,[[S.,V.]]) Type is c for conjunction, d for disjunction Length is the length of the original list: as the original conjunction/ disjunction may have a different evaluation, it is excluded from this procedure puttogether gets a powerset and brings each element in the correct form of a con/disjunction */ puttogether(A,B,[],Val,[]). puttogether(A,Lx,[S|Rest],Val,Y):-length(S,Lx) -> puttogether(A,Lx,Rest,Val,Y). puttogether(A,Lx,[S|Rest],Val,Y):-length(S,0) -> puttogether(A,Lx,Rest,Val,Y). puttogether(A,Lx,[S|Rest],Val,Y):-length(S,1) -> puttogether(A,Lx,Rest,Val,Z), kopf(S,S1),append([[S1,Val]],Z,Y). puttogether(c,Lx,[S|Rest],Val,Y):-length(S,X), X>1, X puttogether(c,Lx,Rest,Val,Z), append([[con(S),Val]],Z,Y). puttogether(d,Lx,[S|Rest],Val,Y):-length(S,X), X>1, X puttogether(d,Lx,Rest,Val,Z), append([[dis(S),Val]],Z,Y). /*expand([S.,V.],[[S.,V.]]) expands a sentence to all its subsentences and propagates evaluation restrictions to them*/ expand([con(X),1],List):-expandlist(c,X,7,L1), append([[con(X),1]], L1, List). expand([con(X),2],List):-expandlist(c,X,6,L1), append([[con(X),2]], L1, List). expand([con(X),3],List):-expandlist(c,X,3,L1), append([[con(X),3]], L1, List). expand([con(X),4],List):-expandlist(c,X,7,L1), append([[con(X),4]], L1, List). expand([con(X),5],List):-expandlist(c,X,7,L1), append([[con(X),5]], L1, List). expand([con(X),6],List):-expandlist(c,X,6,L1), append([[con(X),6]], L1, List). expand([con(X),7],List):-expandlist(c,X,7,L1), append([[con(X),7]], L1, List). expand([dis(X),1],List):-expandlist(d,X,1,L1), append([[dis(X),1]], L1, List). expand([dis(X),2],List):-expandlist(d,X,4,L1), append([[dis(X),2]], L1, List). expand([dis(X),3],List):-expandlist(d,X,7,L1), append([[dis(X),3]], L1, List). expand([dis(X),4],List):-expandlist(d,X,4,L1), append([[dis(X),4]], L1, List). expand([dis(X),5],List):-expandlist(d,X,7,L1), append([[dis(X),5]], L1, List). expand([dis(X),6],List):-expandlist(d,X,7,L1), append([[dis(X),6]], L1, List). expand([dis(X),7],List):-expandlist(d,X,7,L1), append([[dis(X),7]], L1, List). expand([imp(A,B),1],List):-expand([A,3],L1), expand([B,1],L2), append([[imp(A,B),1]], L1, List1), append(List1,L2,List). expand([imp(A,B),2],List):-expand([A,4],L1), expand([B,6],L2), append([[imp(A,B),2]], L1, List1), append(List1,L2,List). expand([imp(A,B),3],List):-expand([A,7],L1), expand([B,7],L2), append([[imp(A,B),3]], L1, List1), append(List1,L2,List). expand([imp(A,B),4],List):-expand([A,7],L1), expand([B,7],L2), append([[imp(A,B),4]], L1, List1), append(List1,L2,List). expand([imp(A,B),5],List):-expand([A,5],L1), expand([B,5],L2), append([[imp(A,B),5]], L1, List1), append(List1,L2,List). expand([imp(A,B),6],List):-expand([A,7],L1), expand([B,7],L2), append([[imp(A,B),6]], L1, List1), append(List1,L2,List). expand([imp(A,B),7],List):-expand([A,7],L1), expand([B,7],L2), append([[imp(A,B),7]], L1, List1), append(List1,L2,List). expand([nott(A),1],List):-expand([A,3],L1),append([[nott(A),1]], L1,List). expand([nott(A),2],List):-expand([A,2],L1),append([[nott(A),2]], L1,List). expand([nott(A),3],List):-expand([A,1],L1),append([[nott(A),3]], L1,List). expand([nott(A),4],List):-expand([A,6],L1),append([[nott(A),4]], L1,List). expand([nott(A),5],List):-expand([A,5],L1),append([[nott(A),5]], L1,List). expand([nott(A),6],List):-expand([A,4],L1),append([[nott(A),6]], L1,List). expand([nott(A),7],List):-expand([A,7],L1),append([[nott(A),7]], L1,List). expand([bar(A),1],List):-expand([A,6],L1), append([[bar(A),1]], L1,List). expand([bar(A),2],List):-expand([A,7],L1), append([[bar(A),2]], L1,List). expand([bar(A),3],List):-expand([A,4],L1), append([[bar(A),3]], L1,List). expand([bar(A),4],List):-expand([A,7],L1), append([[bar(A),4]], L1,List). expand([bar(A),5],List):-expand([A,7],L1), append([[bar(A),5]], L1,List). expand([bar(A),6],List):-expand([A,7],L1), append([[bar(A),6]], L1,List). expand([bar(A),7],List):-expand([A,7],L1), append([[bar(A),7]], L1,List). expand([A,X],[[A,X]]):-atom(A). expand([],[]). /*prepare1([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]]) brings sentences into semi normal form similar to nfl, but deals with the value restrictions as well*/ prepare1([],[]). prepare1([[X,V]|R1],[[Y,V]|R2]):-nf(X,Y), prepare1(R1,R2). /*prepare2([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]]) updates all duplicate sentences to a single value restrictionthrows and then throws out the duplicates*/ prepare2(X,Y):-dupupl(X,X,Z), throwoutdup(Z,Y). /*throwoutdup([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]]) eliminates duplicates*/ throwoutdup([],[]). /*if there is a duplicate of the head of the list in the tail of the list, the result is the rest of the list with eliminated duplicates, if there is no duplicate of the head in the tail, append the head to the rest of the list which has been cleared of duplicates*/ throwoutdup([X|Rest],Z):- chkdup(X,Rest,1) -> throwoutdup(Rest,Z); (throwoutdup(Rest, Inter), append([X],Inter,Z)). /*chkdup([Sentence,Valuerestriction],[[Sentence,Valuerestriction]], Flag) checks whether element or equivalent appear*/ chkdup([X,V], [], 0). chkdup([X,V], [[Y,V2]|Rest],Flag):- eq(X,Y) -> Flag = 1,!; chkdup([X,V],Rest,Flag). /*dupup([[S.,V.]],[[S.,V.]],[[S.,V.]]) 1st List is the one by which the update is done 2nd is the one to be updated 3rd is the result updates the value restriction in list by the list of sentences*/ dupupl([],X,X). dupupl([X|Rest],List1,List2):-dupup(X,List1,Inter),dupupl(Rest,Inter,List2). /*dupup([S.,V.],[[S.,V.]],[[S.,V.]]) 1st arg is sentence by which the update is done 2nd is the one to be updated 3rd is the result updates value restriction in List, that are directly affected by the sentene given*/ dupup([X,Val1],[],[]). dupup([X,Val1],[[Y,Val2]|Rest],[[Z,Val3]|Rest2]):- /*if sentences are equivalent, calculate the new valuerestr.*/ (eq(X,Y) -> Z=X, newvalue(Val1,Val2,Val3); /*if sentence eq to the negation of the other, calculate new value restriction but consider negation*/ (eq(X,nott(Y)) -> Z=Y, notval(Val1,Nval1),newvalue(Nval1,Val2,Val3); /*otherwise nothing changes*/ Z=Y,Val3=Val2)) /*and then update the rest of the list*/ ,dupup([X,Val1],Rest,Rest2),!. /*definition of the negation of a value restriction*/ notval(A,B):- (A=1,B=3,!);(A=2,B=2,!);(A=3,B=1,!);(A=4,B=6,!); (A=5,B=5,!);(A=6,B=4,!);(A=7,B=7,!);(A=0,B=0,!). /*newvalue(old1, old2, new) definition of the new value restr. of a sentence given two old ones*/ newvalue(A,B,0):-(A=1,(B=2;B=3;B=6));(A=2,(B=1;B=3;B=5)); (A=3,(B=1;B=2;B=4));(A=4,B=3);(A=5,B=2);(A=6,B=1);A=0;B=0 . newvalue(A,B,1):-(A=1,(B=1;B=4;B=5;B=7));(A=4,(B=1;B=5)); (A=5,(B=1;B=4));(A=7,B=1). newvalue(A,B,2):-(A=2,(B=2;B=4;B=6;B=7));(A=4,(B=2;B=6)); (A=6,(B=2;B=4));(A=7,B=2). newvalue(A,B,3):-(A=3,(B=3;B=5;B=6;B=7));(A=5,(B=3;B=6)); (A=6,(B=3;B=5));(A=7,B=3). newvalue(A,B,4):-(A=4,(B=4;B=7));(A=7,B=4). newvalue(A,B,5):-(A=5,(B=5;B=7));(A=7,B=5). newvalue(A,B,6):-(A=6,(B=6;B=7));(A=7,B=6). newvalue(A,B,7):- A=7,B=7 . /*conval(A,B, A&B) encodes the truth table for conjunction*/ convalue(A,B,0):-A=0;B=0 . convalue(A,B,1):-A=1;B=1 . convalue(A,B,2):-(A=2,(B=2;B=3;B=6));(A=3,B=2);(A=6,B=2). convalue(A,B,3):-A=3,B=3 . convalue(A,B,4):-(A=4,not(B=1));(B=4,not(A=1));(B=2,(A=5;A=7));(A=2,(B=5;B=7)). convalue(A,B,5):-(A=5,(B=3;B=5));(A=3,B=5). convalue(A,B,6):-(A=6,(B=3;B=6));(A=3,B=6). convalue(A,B,7):-(A=7,(B=3;B=5;B=6;B=7));(A=6,(B=5;B=7)); (A=5,(B=6;B=7));(A=3,B=7). /*disval(A,B, AvB) encodes the truth table for disjunction*/ disvalue(A,B,0):-A=0;B=0 . disvalue(A,B,1):-A=1,B=1 . disvalue(A,B,2):-(A=2,(B=1;B=2));(A=1,B=2);(A=4,B=2);(A=2,B=4). disvalue(A,B,3):-A=3;B=3 . disvalue(A,B,4):-(A=4,(B=1;B=4));(A=1,B=4). disvalue(A,B,5):-(A=5,(B=1;B=5));(A=1,B=5). disvalue(A,B,6):-(A=6,not(B=3));(B=6,not(A=3));(A=2,(B=5;B=7));(B=2,(A=5;A=7)). disvalue(A,B,7):-(A=7,(B=1;B=4;B=5;B=7));(A=5,(B=4;B=7)); (A=4,(B=5;B=7));(A=1,B=7). /*impval(A,B, A->B) encodes the truth table for implication*/ impvalue(A,B,0):-A=0;B=0 . impvalue(A,B,1):-A=3,B=1 . impvalue(A,B,2):-(A=2,B=1);(A=3,B=2). impvalue(A,B,3):-A=1;B=3;(A=2,(B=2;B=6));(A=4,(B=2;B=6)). impvalue(A,B,4):-(A=3,B=4);(A=6,B=1). impvalue(A,B,5):-(A=3,B=5);(A=5,(B=1;B=5)). impvalue(A,B,6):-(A=2,(B=4;B=5;B=7));(A=3,B=6);(A=4,(B=1;B=4;B=5;B=7)); ((A=5;A=6;A=7),(B=2;B=6)). impvalue(A,B,7):-(A=7,(B=1;B=4;B=5;B=7));(A=6,(B=4;B=5;B=7)); (A=5,(B=4;B=7));(A=3,B=7). /*infer1([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]]) Preparation of inference: semi normal form, duplicate elimination, triggering of the inference procedure*/ infer1(Inputlist, Resultlist):- prepare1(Inputlist,X), prepare2(X, Resultlist1), infer(Resultlist1, Resultlist). /*infer([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]]) go on updating value restrictions until the lists don't change (fixpoint reached), infer triggers so many inference runs on the list as it is long, so every subsentence has the chance to get tested */ infer(List1,List2):-length(List1,X),Runs is (X//2),runs(List1,List2,Runs). /*runs([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]],Number) Number is the Number of runs to be done, it is set back to the length of the list, if something has changed if Number is 0 nothing has changed while every subsentence has been tested - done */ runs(List1,List2,Runs):-dosomething(List1,Inter), filterbeliefs(Inter,Out), % writeln(['one run done:', Runs, Inter]), % writeln(['one run done:', Runs]), (eqsen(List1,Inter) -> /*vorher eqlist*/ (Runs>0 -> Newruns is Runs-1, runs(Inter,List2,Newruns) ;List2 = List1) ;(length(Inter,Newruns),runs(Inter,List2,Newruns))). /*rest(List1, List2, Result) calculates List1\List2*/ rest(List,[],List). rest(X,[Y|Rest],Erg):-throwout(Y,X,Inter),rest(Inter, Rest, Erg). /*throwout(X,Y,Result) throws out Element X out of List Y*/ throwout(X,[],[]). throwout(X,[Y|Rest],Rest2):- eq(X,Y) -> throwout(X,Rest,Rest2); (throwout(X,Rest,Inter),append([Y],Inter,Rest2)). /*makelistof(Type,S.,[S.]) creates a list out of an element, different types are necessary since a disjunction within a conjunction is something different than within another disjunction...*/ makelistof(A,X,[X]):-atom(X). makelistof(A,nott(X),[nott(X)]). makelistof(A,bar(X),[bar(X)]). makelistof(A,imp(X),[imp(X)]). makelistof(d,dis(X),X). makelistof(c,con(X),X). makelistof(d,con(X),[con(X)]). makelistof(c,dis(X),[dis(X)]). /*getrest(Type,[S.],S.,Result) calculates the remaining Sentence, after removing parts of a conjunction/disjunction*/ getrest(c,Lg,Lk1,Erg):-makelistof(c,Lk1,Lk),rest(Lg,Lk,Inter), (length(Inter,1) -> kopf(Inter,Erg);Erg=con(Inter)). getrest(d,Lg,Lk1,Erg):-makelistof(d,Lk1,Lk),rest(Lg,Lk,Inter), (length(Inter,1) -> kopf(Inter,Erg);Erg=dis(Inter)). /*isrestof(S.,S.) checks whether a sentence is a part of a conjunction or disjunction*/ isrestof(X,Y):-nf(X,Z1),nf(Y,Z2),isrestof2(Z1,Z2). isrestof2(con(X),con(Y)):-exin(Y,X), not(exin(X,Y)). isrestof2(dis(X),dis(Y)):-exin(Y,X), not(exin(X,Y)). isrestof2(con(X),Y):-member(Y,X). isrestof2(dis(X),Y):-member(Y,X). /*dosomething([[Sentence,Valuerestriction]],[[Sentence,Valuerestriction]]) checks for patterns that allow update of a value restriction, generl pattern: if a pattern that allows update is found -> update and cut to stop backtracking and updating a similar pattern then the pattern is moved to the back of the list, so that in the next run, another pattern can be updated*/ dosomething(List1,List2):-dosomething1(List1,Inter), collectresults(Inter,Inter,List2). /*dosomething1 propagates value restrictions from a sentence to subsentences*/ dosomething1(List1, List2):- ((member([con(X0),1],List1), member([Y0,Val0],List1), isrestof(con(X0),Y0), (Val0=2;Val0=3;Val0=6)),! -> (getrest(c,X0,Y0,Z0), dupup([Z0,1],List1,M1), mtb([con(X0),1],M1,I2));List1=I2), ((member([con(X2),Val2],I2), (Val2=2;Val2=6)),! -> (expandlist(c,X2,6,Y2), dupupl(Y2, I2, M3), mtb([con(X2),Val2],M3,I3));I2=I3), ((member([con(X3),2],I3), member([Y3,3],I3), isrestof(con(X3),Y3)),! -> (getrest(c,X3,Y3,Z3), dupup([Z3,2],I3,M4), mtb([con(X3),2],M4,I9));I3=I9), (member([con(X9),3],I9),! -> (expandlist(c,X9,3,Y9), dupupl(Y9, I9, M10), mtb([con(X9),3],M10,I10));I9=I10), ((member([con(X10),4],I10), member([Y10,3],I10), isrestof(con(X10),Y10)),! -> (getrest(c,X10,Y10,Z10), dupup([Z10,4],I10,M11), mtb([con(X10),4],M11,I12));I10=I12), ((member([con(X12),5],I12), member([Y12,2],I12), isrestof(con(X12),Y12)),! -> (getrest(c,X12,Y12,Z12), dupup([Z12,1],I12,M13), mtb([con(X12),5],M13,I14));I12=I14), ((member([con(X14),5],I14), member([Y14,3],I14), isrestof(con(X14),Y14)),! -> (getrest(c,X14,Y14,Z14), dupup([Z14,5],I14,M15), mtb([con(X14),5],M15,I16));I14=I16), ((member([dis(X16),1],I16)),! -> (expandlist(d,X16,1,Y16), dupupl(Y16, I16, M17), mtb([dis(X16),1],M17,I17));I16=I17), ((member([dis(X17),2],I17)),! -> (expandlist(d,X17,4,Y17), dupupl(Y17, I17, M18), mtb([dis(X17),2],M18,I18));I17=I18), ((member([dis(X18),2],I18), member([Y18,1],I18), isrestof(dis(X18),Y18)),! -> (getrest(d,X18,Y18,Z18), dupup([Z18,2],I18,M19), mtb([dis(X18),2],M19,I20));I18=I20), ((member([dis(X20),3],I20), member([Y20,Val20],I20), isrestof(dis(X20),Y20), (Val20=1;Val20=2;Val20=4)),! -> (getrest(d,X20,Y20,Z20), dupup([Z20,3],I20,M21), mtb([dis(X20),3],M21,I22));I20=I22), ((member([dis(X22),4],I22)),! -> (expandlist(d,X22,4,Y22), dupupl(Y22, I22, M23), mtb([dis(X22),4],M23,I23));I22=I23), ((member([dis(X23),5],I23), member([Y23,2],I23), isrestof(dis(X23),Y23)),! -> (getrest(d,X23,Y23,Z23), dupup([Z23,3],I23,M24), mtb([dis(X23),5],M24,I25));I23=I25), ((member([dis(X25),6],I25), member([Y25,1],I25), isrestof(dis(X25),Y25)),! -> (getrest(d,X25,Y25,Z25), dupup([Z25,6],I25,M26), mtb([dis(X25),6],M26,I27));I25=I27), (member([imp(X27,Y27),1],I27),! -> (dupup([X27,3],I27,II27), dupup([Y27,1],II27,M28), mtb([imp(X27,Y27),1],M28,I28));I27=I28), (member([imp(X28,Y28),2],I28),! -> (dupup([X28,6],I28,II28), dupup([Y28,4],II28,M29), mtb([imp(X28,Y28),2],M29,I29));I28=I29), ((member([imp(X29,Y29),2],I29), member([X29,1],I29)),! -> (dupup([Y29,0],I29,M30), mtb([imp(X29,Y29),2],M30,I30));I29=I30), ((member([imp(X30,Y30),2],I30), member([X30,2],I30)),! -> (dupup([X30,1],I30,M31), mtb([imp(X30,Y30),2],M31,I31));I30=I31), ((member([imp(X31,Y31),2],I31), member([X31,3],I31)),! -> (dupup([X31,2],I31,M32), mtb([imp(X31,Y31),2],M32,I32));I31=I32), ((member([imp(X32,Y32),3],I32), member([X32,Val32],I32), (Val32=2;Val32=6)),! -> (dupup([Y32,6],I32,M33), mtb([imp(X32,Y32),3],M33,I33));I32=I33), ((member([imp(X33,Y33),3],I33), member([X33,3],I33)),! -> (dupup([Y33,3],I33,M34), mtb([imp(X33,Y33),3],M34,I34));I33=I34), (member([imp(X34,Y34),4],I34),! -> (dupup([X34,6],I34,II34), dupup([Y34,4],II34,M35), mtb([imp(X34,Y34),4],M35,I35));I34=I35), ((member([imp(X35,Y35),4],I35), member([X35,2],I35)),! -> (dupup([Y35,1],I35,M36), mtb([imp(X35,Y35),4],M36,I36));I35=I36), ((member([imp(X36,Y36),5],I36), member([X36,2],I36)),! -> (dupup([Y36,6],I36,M37), mtb([imp(X36,Y36),5],M37,I37));I36=I37), ((member([imp(X37,Y37),5],I37), member([X37,3],I37)),! -> (dupup([Y37,5],I37,M38), mtb([imp(X37,Y37),5],M38,I38));I37=I38), ((member([imp(X38,Y38),6],I38), member([X38,3],I38)),! -> (dupup([Y38,6],I38,M39), mtb([imp(X38,Y38),6],M39,I39));I38=I39), ((member([imp(X39,Y39),2],I39), member([Y39,1],I39)),! -> (dupup([X39,2],I39,M40), mtb([imp(X39,Y39),2],M40,I40));I39=I40), ((member([imp(X40,Y40),2],I40), member([Y40,2],I40)),! -> (dupup([X40,3],I40,M41), mtb([imp(X40,Y40),2],M41,I41));I40=I41), ((member([imp(X41,Y41),2],I41), member([Y41,3],I41)),! -> (dupup([X41,0],I41,M42), mtb([imp(X41,Y41),2],M42,I42));I41=I42), ((member([imp(X42,Y42),2],I42), member([Y42,4],I42)),! -> (dupup([X42,4],I42,M43), mtb([imp(X42,Y42),2],M43,I43));I42=I43), ((member([imp(X43,Y43),3],I43), member([Y43,1],I43)),! -> (dupup([X43,1],I43,M44), mtb([imp(X43,Y43),3],M44,I44));I43=I44), ((member([imp(X44,Y44),3],I44), member([Y44,2],I44)),! -> (dupup([X44,4],I44,M45), mtb([imp(X44,Y44),3],M45,I45));I44=I45), ((member([imp(X45,Y45),3],I45), member([Y45,4],I45)),! -> (dupup([X45,4],I45,M46), mtb([imp(X45,Y45),3],M46,I46));I45=I46), ((member([imp(X46,Y46),4],I46), member([Y46,2],I46)),! -> (dupup([X46,3],I46,M47), mtb([imp(X46,Y46),4],M47,I47));I46=I47), ((member([imp(X47,Y47),5],I47), member([Y47,1],I47)),! -> (dupup([X47,5],I47,M48), mtb([imp(X47,Y47),5],M48,I48));I47=I48), ((member([imp(X48,Y48),5],I48), member([Y48,2],I48)),! -> (dupup([X48,4],I48,M49), mtb([imp(X48,Y48),5],M49,I49));I48=I49), ((member([imp(X49,Y49),6],I49), member([Y49,1],I49)),! -> (dupup([X49,4],I49,M50), mtb([imp(X49,Y49),6],M50,I50));I49=I50), ((member([dis(X50),3],I50), member(XE50,X50), member([dis(Y50),3],I50), isrestof(dis(Y50),nott(XE50)), nf(nott(XE50),YE50), getrest(d,X50,XE50,RX50), getrest(d,Y50,YE50,RY50), eq(RX50,RY50)),! -> (dupup([RX50,3],I50,M51), mtb([dis(X50),3],M51,II51), mtb([dis(Y50),3],II51,I52));I50=I52), ((member([dis(X52),3],I52), member(bar(XE52),X52), member([dis(Y52),3],I52), isrestof(dis(Y52),XE52), getrest(d,X52,bar(XE52),RX52), getrest(d,Y52,XE52,RY52), eq(RX52,RY52)),! ->(dupup([RX52,3],I52,M53), mtb([dis(X52),3],M53,II53), mtb([dis(Y52),3],II53,I62));I52=I62), (member([bar(X62),3],I62),! -> (dupup([X62,4],I62,M63), mtb([bar(X62),3],M63,I63));I62=I63), (member([bar(X63),1],I63),! -> (dupup([X63,6],I63,M64), mtb([bar(X63),1],M64,I64));I63=I64), List2=I64. /*collectresults([[S.,V.]],[[S.,V.]],[[S.,V.]]) propagates value restrictions from subsentences to the outer sentence*/ collectresults([],List,List). collectresults([[X,Val]|Rest],List1,List2):-atom(X), collectresults(Rest,List1,List2). collectresults([[nott(X),Val1]|Rest],List1,List2):- member([X,Val2],List1), notval(Val1,NVal1), newvalue(Val2,NVal1,New2), notval(New2,NewNVal1), dupupl([[nott(X),NewNVal1],[X,New2]],List1,Inter), collectresults(Rest,Inter,List2). collectresults([[con(X),Val1]|Rest],List1,List2):- conval(X,List1,New), newvalue(Val1,New,Newval), dupup([con(X),Newval],List1,Inter), collectresults(Rest,Inter,List2). collectresults([[dis(X),Val1]|Rest],List1,List2):- disval(X,List1,New), newvalue(Val1,New,Newval), dupup([dis(X),Newval],List1,Inter), collectresults(Rest,Inter,List2). collectresults([[bar(X),Val1]|Rest],List1,List2):- barval([X],List1,New), newvalue(Val1,New,Newval), dupup([bar(X),Newval],List1,Inter), collectresults(Rest,Inter,List2). collectresults([[imp(X,Y),Val1]|Rest],List1,List2):- impval([X,Y],List1,New), newvalue(Val1,New,Newval), dupup([imp(X,Y),Newval],List1,Inter), collectresults(Rest,Inter,List2). /*???val gets the values of the subsentences and calculates the new value*/ conval(X,List,New):-getvalues(X,List,Erg), calccon(Erg,New). disval(X,List,New):-getvalues(X,List,Erg), calcdis(Erg,New). barval(X,List,New):-getvalues(X,List,Erg), calcbar(Erg,New). impval(X,List,New):-getvalues(X,List,Erg), calcimp(Erg,New). calccon(X,Y):-length(X,1),kopf(X,Y). calccon([X|Rest],Y):-length(Rest,L),L>0,calccon(Rest,Inter),convalue(X,Inter,Y). calcdis(X,Y):-length(X,1),kopf(X,Y). calcdis([X|Rest],Y):-length(Rest,L),L>0,calcdis(Rest,Inter),disvalue(X,Inter,Y). calcbar([X],Y):-(X=0,Y=0);(X=1,Y=6);(X=3,Y=4);((X=2;X=4;X=5;X=6;X=7),Y=7). calcimp([X,Y],Z):-impvalue(X,Y,Z). /*getvalues collects the values of the sentences in a list*/ getvalues([],List,[]). getvalues([X|Rest],List,Erg):-member([X,Val1],List), getvalues(Rest,List,Inter), append([Val1],Inter,Erg). filterbeliefs(X,Y):-filterbeliefs1(X,Z),sort(Z,Y). filterbeliefs1([],[]). filterbeliefs1([[X,3]|Rest],Y):-filterbeliefs1(Rest,Rest2),append([[X,3]],Rest2,Y). filterbeliefs1([[X,1]|Rest],Y):-filterbeliefs1(Rest,Rest2),append([[X,1]],Rest2,Y). filterbeliefs1([[X,Val]|Rest],Rest2):-(Val=0;Val=2;Val=4;Val=5;Val=6;Val=7),filterbeliefs1(Rest,Rest2).