Menu
▾
▴
[Xsb-commits] CVS: XSB/packages/altCDF/mknf/tests/ex_disj cdf_extensional.P, 1.1, 1.2 rules.P, 1.1, 1.2
|
From: Terrance S. <ts...@us...> - 2009-05-17 17:14:21
|
Update of /cvsroot/xsb/XSB/packages/altCDF/mknf/tests/ex_disj In directory fdv4jf1.ch3.sourceforge.com:/tmp/cvs-serv3142/tests/ex_disj Modified Files: cdf_extensional.P rules.P Log Message: 1) Refactored mknf code so that it is again properly calling check_worlds. 2) MKNF code isno longer (improperly) propagating conditional answers to allModelsEntails --- this gets rid of get_conditional_dependencies and last_dlnot. Index: cdf_extensional.P =================================================================== RCS file: /cvsroot/xsb/XSB/packages/altCDF/mknf/tests/ex_disj/cdf_extensional.P,v retrieving revision 1.1 retrieving revision 1.2 diff -u -r1.1 -r1.2 --- cdf_extensional.P 12 May 2009 16:44:48 -0000 1.1 +++ cdf_extensional.P 17 May 2009 17:14:06 -0000 1.2 @@ -1,15 +1,39 @@ -/* -nessesCond_ext(oid(p_or_q,mknf),vid(';'(cid(p,mknf),cid(q,mknf)))). -isa_ext(oid(p_or_q,mknf),cid(r,mknf)). -*/ +%----------- +% Ex 1 isa_ext(cid(first,mknf),cid(second,mknf)). isa_ext(cid(third,mknf),cid(fourth,mknf)). +%----------- +% Ex 2 + necessCond_ext(cid(win1,mknf),vid(not(cid(win2,mknf)))). necessCond_ext(cid(win3,mknf),vid(not(cid(win4,mknf)))). +%----------- +% Ex 3 + necessCond_ext(cid(loop2,mknf),vid(not(cid(loop1,mknf)))). -%isa_ext(oid(tok,mknf),cid(win1,mknf)). +%----------- +% Ex 4 + +necessCond_ext(oid(a4,mknf),vid(not(cid(two4,mknf)))). + +%----------- +% Ex 5 + +nessesCond_ext(cid(p_or_q5,mknf),vid(';'(cid(p5,mknf),cid(q5,mknf)))). +nectssCond_ext(cid(r5,mknf),vid(not(';'(cid(p5,mknf),cid(q5,mknf))))). + +%----------- +% Ex 6 + +% NaturalDeath â Pay +isa_ext(cid(naturalDeath,mknf),cid(pay,mknf)). + +% Suicide â ¬Pay (cheating here) +isa_ext(cid(suicide,mknf),cid(notpay),mknf). + +isa_ext(oid(j1,mknf),cid(notNaturalDeath,mknf)). Index: rules.P =================================================================== RCS file: /cvsroot/xsb/XSB/packages/altCDF/mknf/tests/ex_disj/rules.P,v retrieving revision 1.1 retrieving revision 1.2 diff -u -r1.1 -r1.2 --- rules.P 12 May 2009 16:44:48 -0000 1.1 +++ rules.P 17 May 2009 17:14:06 -0000 1.2 @@ -1,5 +1,6 @@ +:- import member/2 from basics. -/**** +/* p_or_q \subseteq (p or q) p_or_q \subseteq r @@ -7,32 +8,100 @@ ****/ -l1(ab):- dlnot(l2(ab)). -l2(ab):- dlnot(l1(ab)). +%----------- +% Ex 1 first(callback). third(X):- known(second(X)). fifth(X):- known(fourth(X)). -win1(tok). -win3(tok):- dlnot(win2(tok)). -win5(tok):- dlnot(win4(tok)). - definedClass(first(Obj),first,Obj):- Obj = callback. definedClass(second(Obj),second,Obj):- Obj = callback. definedClass(third(Obj),third,Obj):- Obj = callback. definedClass(fourth(Obj),fourth,Obj):- Obj = callback. definedClass(fifth(Obj),fifth,Obj):- Obj = callback. +%----------- +% Ex 2 +% win1 \subset not(win2) +% win3 \subset not(win4) + +win1(tok). +win3(tok):- dlnot(win2(tok)). +win5(tok):- dlnot(win4(tok)). + definedClass(win1(Obj),win1,Obj):- Obj = tok. definedClass(win2(Obj),win2,Obj):- Obj = tok. definedClass(win3(Obj),win3,Obj):- Obj = tok. definedClass(win4(Obj),win4,Obj):- Obj = tok. definedClass(win5(Obj),win5,Obj):- Obj = tok. +%----------- +% Ex 3 + +l1(ab):- dlnot(l2(ab)). +l2(ab):- dlnot(l1(ab)). + definedClass(l1(Obj),l1,Obj):- Obj = ab. definedClass(l2(Obj),l2,Obj):- Obj = ab. +%----------- +% Ex 4 +% p \in not(two4). + +one4(X):- known(p4(a4)),dlnot(two4(X)). +two4(X):- known(p4(a4)),dlnot(one4(X)). + +p4(a4). + +definedClass(p4(X),p4,X):- X = a4. +definedClass(two4(X),two4,X):- X = a4. +definedClass(one4(X),one4,X):- X = a4. + +%----------- +% Ex 5 (not yet working) +% p_or_q \subset (p \cup q) +% r \subset not (p \cup q) + +p5(a5). + +definedClass(p5(X),p5,X):- X = a5. +definedClass(q5(X),q5,X):- X = a5. +definedClass(p_or_q5(X),p_or_q5,X):- X = a5. +definedClass(r5(X),r5,X):- X = a5. + +%----------- +% Ex 6 + +% NaturalDeath â Pay +% Suicide â ¬Pay (cheating here) +/* +pay(X):- known(murdered(X)),known(benefits(X,Y)),dlnot(responsible(Y,X)). +suicide(X):- dlnot(naturalDeath(X)),dlnot(murdered(X)). +murdered(X):- dlnot(naturalDeath(X)),dlnot(suicide(X)). + +murdered(j2). +responsible(max,j2). +benefits(j2,thomas). + +murdered(j3). +responsible(max,j3). +benefits(j3,max). + +definedClass(pay(X),pay,X):- member(X,[j1,j2,j3,max,thomas]). +definedClass(suicide(X),suicide,X):- member(X,[j1,j2,j3,max,thomas]). +definedClass(murdered(X),murdered,X):- member(X,[j1,j2,j3,max,thomas]). +definedClass(benefits(X),benefits,X):- member(X,[j1,j2,j3,max,thomas]). +definedClass(responsible(X),responsible,X):- member(X,[j1,j2,j3,max,thomas]). +*/ + +%----------- +% example w. multiple objects. + +first1(cb1). +first2(cb2):- known(first1(cb1)). +first3(cb1):- known(first2(cb2)). + /* definedClass(loop1(Obj),loop1,Obj):- Obj = abd. definedClass(loop2(Obj),loop2,Obj):- Obj = abd. @@ -41,35 +110,49 @@ test:- test_call(k(fifth(callback)),get_object_model(oid(callback,mknf), - [entry(known(fifth(callback),6),[[]]), - entry(known(first(callback),6),[[]]), - entry(known(fourth(callback),6),[[]]), - entry(known(second(callback),6),[[]]), - entry(known(third(callback),6),[[]])], + [entry(known(fifth(callback)),[[]]), + entry(known(first(callback)),[[]]), + entry(known(fourth(callback)),[[]]), + entry(known(second(callback)),[[]]), + entry(known(third(callback)),[[]])], [], - [entry(allModelsEntails(oid(callback,mknf),cid(fifth,mknf),6),[[]]), - entry(allModelsEntails(oid(callback,mknf),cid(first,mknf),6),[[]]), - entry(allModelsEntails(oid(callback,mknf),cid(fourth,mknf),6),[[]]), - entry(allModelsEntails(oid(callback,mknf),cid(second,mknf),6),[[]]), - entry(allModelsEntails(oid(callback,mknf),cid(third,mknf),6),[[]])])), + [entry(allModelsEntails(oid(callback,mknf),cid(fifth,mknf)),[[]]), + entry(allModelsEntails(oid(callback,mknf),cid(first,mknf)),[[]]), + entry(allModelsEntails(oid(callback,mknf),cid(fourth,mknf)),[[]]), + entry(allModelsEntails(oid(callback,mknf),cid(second,mknf)),[[]]), + entry(allModelsEntails(oid(callback,mknf),cid(third,mknf)),[[]])])), test_call(k(win5(tok)),get_object_model(oid(tok,mknf), - [entry(known(win1(tok),2),[[]]),entry(known(win3(tok),2),[[]]), - entry(known(win5(tok),2),[[]])], - [entry(dlnot(win2(tok),2),[[]]),entry(dlnot(win4(tok),2),[[]])], - [entry(allModelsEntails(oid(tok,mknf),not cid(win2,mknf),2),[[]]), - entry(allModelsEntails(oid(tok,mknf),not cid(win4,mknf),2),[[]]), - entry(allModelsEntails(oid(tok,mknf),cid(win1,mknf),2),[[]]), - entry(allModelsEntails(oid(tok,mknf),cid(win3,mknf),2),[[]]), - entry(allModelsEntails(oid(tok,mknf),cid(win5,mknf),2),[[]])])), + [entry(known(win1(tok)),[[]]),entry(known(win3(tok)),[[]]), + entry(known(win5(tok)),[[]])], + [entry(dlnot(win2(tok)),[[]]),entry(dlnot(win4(tok)),[[]])], + [entry(allModelsEntails(oid(tok,mknf),not cid(win2,mknf)),[[]]), + entry(allModelsEntails(oid(tok,mknf),not cid(win4,mknf)),[[]]), + entry(allModelsEntails(oid(tok,mknf),cid(win1,mknf)),[[]]), + entry(allModelsEntails(oid(tok,mknf),cid(win3,mknf)),[[]]), + entry(allModelsEntails(oid(tok,mknf),cid(win5,mknf)),[[]])])), + +% test_call(k(l1(ab)),get_object_model(oid(ab,mknf), +% [entry(known(l1(ab),3),[[dlnot(l2(ab),3)],[allModelsEntails(oid(ab,mknf),cid(l1,mknf),2)]]), +% entry(known(l2(ab),3),[[dlnot(l1(ab),3)],[allModelsEntails(oid(ab,mknf),cid(l2,mknf),2)]])], +% [entry(dlnot(l1(ab),3),[[tnot(known(l1(ab),3))]]), +% entry(dlnot(l2(ab),3),[[tnot(known(l2(ab),3))]])], +% [entry(allModelsEntails(oid(ab,mknf),cid(l1,mknf),3),[[known(l1(ab),2),known(l2(ab),2)]]), +% entry(allModelsEntails(oid(ab,mknf),cid(l2,mknf),3),[[known(l1(ab),2),known(l2(ab),2)]])])). test_call(k(l1(ab)),get_object_model(oid(ab,mknf), - [entry(known(l1(ab),3),[[dlnot(l2(ab),3)],[allModelsEntails(oid(ab,mknf),cid(l1,mknf),2)]]), - entry(known(l2(ab),3),[[dlnot(l1(ab),3)],[allModelsEntails(oid(ab,mknf),cid(l2,mknf),2)]])], - [entry(dlnot(l1(ab),3),[[tnot(known(l1(ab),3))]]), - entry(dlnot(l2(ab),3),[[tnot(known(l2(ab),3))]])], - [entry(allModelsEntails(oid(ab,mknf),cid(l1,mknf),3),[[known(l1(ab),2),known(l2(ab),2)]]), - entry(allModelsEntails(oid(ab,mknf),cid(l2,mknf),3),[[known(l1(ab),2),known(l2(ab),2)]])])). + [entry(known(l1(ab)),[[dlnot(l2(ab))]]), + entry(known(l2(ab)),[[dlnot(l1(ab))]])], + [entry(dlnot(l1(ab)),[[tnot(known(l1(ab)))]]), + entry(dlnot(l2(ab)),[[tnot(known(l2(ab)))]])], + [])), + + test_call(k(one4(a4)),get_object_model(oid(a4,mknf), + [entry(known(one4(a4)),[[]]),entry(known(p4(a4)),[[]])], + [entry(dlnot(two4(a4)),[[]])], + [entry(allModelsEntails(oid(a4,mknf),not cid(two4,mknf)),[[]]), + entry(allModelsEntails(oid(a4,mknf),cid(one4,mknf)),[[]]), + entry(allModelsEntails(oid(a4,mknf),cid(p4,mknf)),[[]])])). end_of_file. |