% test dealing with instances of type counts with modality :- module(cute6,[]). :- include(test_header). :- user:use_module(library(editline)). :- use_module(library(occurs)). % sub_term/2 :- use_module(library(sort)). % predsort/3 :- use_module(library(backcomp)). % concat_atom/2 :- user:autoload. :- module_transparent(system: = /2). :- module_transparent('$attvar':'$wakeup'/1). :- module_transparent('$attvar':'call_all_attr_uhooks'/2). :- module_transparent('$attvar':'begin_call_all_attr_uhooks'/2). :- module_transparent('$attvar':'uhook'/3). :- '$current_source_module'(M),install_retry_undefined(M,error). :- install_retry_undefined(user,error). :- install_retry_undefined(kbii,error). :- install_retry_undefined(kbi,error). % :- set_prolog_flag(autoload,false). :- set_prolog_flag(retry_undefined, false). :- set_prolog_flag(access_level, system). % Option Examples: nesc($sentence), poss($sentence), poss($sentence)=>nesc($sentence). % ==> feature_setting(default_modality,nesc($sentence)). /* Feature Notes: P. % P happens to be the feature_setting default_modality poss(P). % possibly P nesc(P). % necessarily P ~nesc(P). % not necessarily P nesc(~P). % necessarily not P ~poss(P). % not possibly P poss(~P). % possibly not P poss(P)=>nesc(P). % P is true by default (allows other axioms to override) poss(P)&~nesc(P). % possibly, but not necessarily P ~naf(P). % P is default naf(~P). % possibly P naf(P). % possibly not P there are many Logically equivalent settings like ~poss(P) == nesc(~P) falsify(~P) == poss(P) v nesc(P). */ test_sanity(G):- add_boxlog_history(G), test_sanity0(G),!. test_sanity0(G):- mpred_test(G),!. test_sanity0((A,B)):- !, mpred_test(A),test_sanity0(B). :- kbi_define(cute/1). :- kbi_define(ugly/1). :- kb_shared(baseKB:cute/1). :- kb_local(ugly/1). :- kb_local(isa/2). :- kbi_define(poss/1). :- use_module(library(clpfd)). % :- debug(_). :- set_prolog_flag(gc,false). :- set_prolog_flag(toplevel_print_anon,false). :- set_prolog_flag(answer_write_options,[quoted(true), portray(false), max_depth(20)]). :- set_prolog_flag(write_attributes,ignore). :- set_prolog_flag(toplevel_print_factorized, true). %===== axioms ======= % there are exactly 5 puppies total :- test_boxlog([+assert],exactly(5, X, puppy(X))). % Ensure we can see them % :- test_sanity((findall(X,puppy(X),L),length(L,5))). % there are 2 (for sure) cute puppies :- test_boxlog([+assert],exactly(2, X, puppy(X) & cute(X))). % there are 3 (for sure) hungry puppies :- test_boxlog([+assert],exactly(3, X, puppy(X) & hungry(X))). end_of_file. % there are 2 (for sure) ugly puppies :- test_boxlog([+assert],exactly(2, X, puppy(X) & ugly(X))). % There is a puppy we call puppy2 :- test_boxlog([+assert,+existentialize_objs],puppy(puppy2)). % cute things cannot be ugly things and visa versa :- test_boxlog([+assert],forall( X, iff(cute(X),~ugly(X)))). % all puppies are cute or ugly :- test_boxlog([+assert],forall( X, if(puppy(X),(ugly(X) v cute(X))))). end_of_file. % There is a puppy we call puppy1 :- test_boxlog([+assert],puppy(puppy1)). % Ensure we still only see 5 :- test_sanity((findall(X,puppy(X),L),length(L,5))). % Ensure we can get 5x5 :- test_sanity((findall(G,(puppy(X),puppy(Y),G =( X=Y), writeln(G),ignore(G)),L),length(L,Len),Len==25)). % there are 4 possibly cute puppies :- test_boxlog([+assert],exactly(4, X, puppy(X) & poss(cute(X)))). % Ensure we can see them :- test_sanity((findall(X,poss(cute(X)),L),length(L,4))). % Ensure only 4 pairs are equal instances :- test_sanity((findall(G,(puppy(X),puppy(Y),G =( X=Y), writeln(G),G),L),length(L,Len),Len==4)). % Ensure when two are picked out via conjunction the system tries to serve out 2 different values :- test_sanity(( puppy(X),puppy(Y), !, X\=Y )). % Ensure when two are picked out consecutively they are different object instances :- test_sanity(( puppy(X),puppy(Y), !, dif_objs(X,Y) )). % Ensure 12 naive obj dif pairs :- test_sanity(( findall(X\=Y,(puppy(X),puppy(Y), dif_objs(X,Y)),L),length(L,Len),Len==12)). % Ensure only 6 total obj dif pairs :- test_sanity(( findall(X\=Y,(pred1_to_unique_pairs(puppy,X,Y), dif_objs(X,Y)),L),length(L,Len),Len==6)). % Ensure 20 naive obj dif pairs :- test_sanity(( findall(X\=Y,(puppy(X),puppy(Y), dif_objs(X,Y)),L),length(L,Len),Len==20)). % Ensure only 10 total obj dif pairs :- test_sanity(( findall(X\=Y,(pred1_to_unique_pairs(puppy,X,Y), dif_objs(X,Y)),L),length(L,Len),Len==10)). % there are 2 (for sure) cute puppies :- test_boxlog([+assert],exactly(2, X, puppy(X) & cute(X))). % there is at least one puppy :- test_boxlog([+assert],atleast(1, X, puppy(X))). % there is at least one puppy :- test_boxlog([+assert],exists(X, puppy(X))). end_of_file. %===== tests ======= :- if(kif_option_value(unit_tests,true)). % means total 5 puppies :- test_sanity( { findall(X,puppy(X),L),length(L,5) }). % 2 are for sure actually cute :- test_sanity( { findall(X,(puppy(X),cute(X)),L),length(L,2)}). % leaving 3 more as _only_ possibly cute :- test_sanity( { findall(X,(puppy(X),poss(cute(X)),naf(cute(X))),L),length(L,3)}). % the last puppy is not for sure known cute or or not cute so it may be ugly % :- test_sanity( { findall(X,(puppy(X),poss(ugly(X))),L),length(L,1)}). :- endif. :- if(kif_option_value(extras(test_fwc),true)). puppy(X) ==> known(puppy(X)). cute(X) ==> known(cute(X)). ugly(X) ==> known(ugly(X)). ~ugly(X) ==> known(~ugly(X)). poss(cute(X)) ==> known(poss(cute(X))). :- endif. end_of_file. %===== debugging notes ======= :- test_sanity((nesc(puppy(Puppy1)),nesc(puppy(Puppy2)),Puppy1=Puppy2)). /* Puppy1 = Puppy2, add_cond(Puppy2, [puppy, poss(cute(Puppy2)), skF(skF(skIsCuteIsPuppyX_0FnSk, vv), 4)]) ; Puppy1 = Puppy2, add_cond(Puppy2, [puppy, poss(cute(Puppy2)), skF(skF(skIsCuteIsPuppyX_0FnSk, vv), 2)]) ; Puppy1 = Puppy2, add_cond(Puppy2, [puppy, poss(cute(Puppy2)), skF(skF(skIsCuteIsPuppyX_0FnSk, vv), 3)]) ; Puppy1 = Puppy2, add_cond(Puppy2, [puppy, poss(cute(Puppy2)), skF(skF(skIsCuteIsPuppyX_0FnSk, vv), 1)]). */ go_test:- forall(no_repeats(proven_neg(G)),writeln(proven_neg(G))). ?- nesc(puppy(Puppy1)),nesc(puppy(Puppy2)),nesc(puppy(Puppy3)),nesc(puppy(Puppy4),nesc(puppy(Puppy5)), comingle_vars([Puppy1,Puppy2,Puppy3,Puppy4],NewP). cute6: ?- nl,puppy(Puppy),get_typeinfos(Puppy,TYPEINFO),writeln(Puppy=TYPEINFO),fail. _488=[poss(cute(_488)),puppy(_488)] _488=[poss(cute(_488)),puppy(_488)] _488=[poss(cute(_488)),puppy(_488)] _488=[poss(cute(_488)),puppy(_488)] _3360=[cute(_3360),puppy(_3360)] _3360=[cute(_3360),puppy(_3360)] _4836=[puppy(_4836)] _4836=[puppy(_4836)] _4836=[puppy(_4836)] _4836=[puppy(_4836)] _4836=[puppy(_4836)] % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:11 % :- test_boxlog(exactly(4, X_VAR, puppy(X_VAR)&poss(cute(X_VAR)))). % autoloading common_logic_snark:gensym/2 from /home/prologmud_server/lib/swipl-7.5.15/library/gensym % autoloading dmsg:maplist/2 from /home/prologmud_server/lib/swipl-7.5.15/library/apply % autoloading attvar_serializer:maplist/3 from /home/prologmud_server/lib/swipl-7.5.15/library/apply % kif :- % exactly(4, X, puppy(X)&poss(cute(X))). % autoloading cute6:sub_term/2 from /home/prologmud_server/lib/swipl-7.5.15/library/occurs % autoloading cute6:concat_atom/2 from /home/prologmud_server/lib/swipl-7.5.15/library/backcomp % autoloading common_logic_compiler:sub_term/2 from /home/prologmud_server/lib/swipl-7.5.15/library/occurs % nnf :- % ~puppy(X)v nesc(~cute(X))v skolem(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), _38009592)&(puppy(X)&poss(cute(X))v~skolem(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), _38009592))&(~puppy(_38033330)v nesc(~cute(_38033330))v~different(_38006508, _38033330)v(~puppy(_38037090)v nesc(~cute(_38037090))v~different(_38006508, _38037090)v(~puppy(_38006508)v nesc(~cute(_38006508))v(~puppy(_38044610)v nesc(~cute(_38044610)))v~different(_38006508, _38044610)v(~puppy(_38040850)v nesc(~cute(_38040850))v~different(_38006508, _38040850))))). % to_tnot :- % ( ( ( neg(puppy(X)) % ; nesc(nesc(~cute(X))) % ) % ; nesc(skolem(X, % count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), % _38009592)) % ), % ( nesc(puppy(X)), % nesc(poss(cute(X))) % ; neg(skolem(X, % count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), % _38009592)) % ) % ), % ( ( ( neg(puppy(_38033330)) % ; nesc(nesc(~cute(_38033330))) % ) % ; neg(different(_38006508, _38033330)) % ) % ; ( ( neg(puppy(_38037090)) % ; nesc(nesc(~cute(_38037090))) % ) % ; neg(different(_38006508, _38037090)) % ) % ; ( ( ( neg(puppy(_38006508)) % ; nesc(nesc(~cute(_38006508))) % ) % ; neg(puppy(_38044610)) % ; nesc(nesc(~cute(_38044610))) % ) % ; neg(different(_38006508, _38044610)) % ) % ; ( neg(puppy(_38040850)) % ; nesc(nesc(~cute(_38040850))) % ) % ; neg(different(_38006508, _38040850)) % ). % tlog_nnf :- % ( ( ( n(neg(puppy(X))), % n(nesc(nesc(~cute(X)))) % ), % n(nesc(skolem(X, % count(4, % inf, % skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), % _38009592))) % ; ( n(nesc(puppy(X))) % ; n(nesc(poss(cute(X)))) % ), % n(neg(skolem(X, % count(4, % inf, % skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), % _38009592))) % ) % ; ( ( n(neg(puppy(_38033330))), % n(nesc(nesc(~cute(_38033330)))) % ), % n(neg(different(_38006508, _38033330))) % ), % ( ( n(neg(puppy(_38037090))), % n(nesc(nesc(~cute(_38037090)))) % ), % n(neg(different(_38006508, _38037090))) % ), % ( ( ( n(neg(puppy(_38006508))), % n(nesc(nesc(~cute(_38006508)))) % ), % n(neg(puppy(_38044610))), % n(nesc(nesc(~cute(_38044610)))) % ), % n(neg(different(_38006508, _38044610))) % ), % ( n(neg(puppy(_38040850))), % n(nesc(nesc(~cute(_38040850)))) % ), % n(neg(different(_38006508, _38040850))) % ). % tlog_nnf_out_negated :- % n(~puppy(X))&n(nesc(nesc(~cute(X))))&n(nesc(skolem(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), _38009592)))v(n(nesc(puppy(X)))v n(nesc(poss(cute(X))))&n(~skolem(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), _38009592)))v(n(~puppy(_38033330))&n(nesc(nesc(~cute(_38033330))))&n(~different(_38006508, _38033330))&(n(~puppy(_38037090))&n(nesc(nesc(~cute(_38037090))))&n(~different(_38006508, _38037090))&(n(~puppy(_38006508))&n(nesc(nesc(~cute(_38006508))))&(n(~puppy(_38044610))&n(nesc(nesc(~cute(_38044610)))))&n(~different(_38006508, _38044610))&(n(~puppy(_38040850))&n(nesc(nesc(~cute(_38040850))))&n(~different(_38006508, _38040850)))))). % autoloading common_logic_modalization:sub_term/2 from /home/prologmud_server/lib/swipl-7.5.15/library/occurs % autoloading cute6:predsort/3 from /home/prologmud_server/lib/swipl-7.5.15/library/sort proven_neg(puppy(Puppy1)) :- falsify(~cute(Puppy1)), nesc(puppy(Puppy2)), falsify(~cute(Puppy2)), dif_objs(Puppy1, Puppy2), nesc(puppy(Puppy3)), falsify(~cute(Puppy3)), dif_objs(Puppy1, Puppy3), nesc(puppy(Puppy4)), falsify(~cute(Puppy4)), dif_objs(Puppy1, Puppy4), nesc(puppy(Puppy5)), dif_objs(Puppy1, Puppy5), falsify(~cute(Puppy5)). proven_neg(different(Puppy1, Puppy5)) :- nesc(puppy(Puppy5)), falsify(~cute(Puppy5)), nesc(puppy(Puppy4)), falsify(~cute(Puppy4)), dif_objs(Puppy1, Puppy4), nesc(puppy(Puppy1)), falsify(~cute(Puppy1)), nesc(puppy(Puppy2)), falsify(~cute(Puppy2)), dif_objs(Puppy1, Puppy2), nesc(puppy(Puppy3)), dif_objs(Puppy1, Puppy3), falsify(~cute(Puppy3)). proven_tru(poss(cute(X))) :- skolem(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), KB). proven_tru(puppy(X)) :- skolem(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), KB). proven_tru(~cute(Puppy1)) :- nesc(puppy(Puppy1)), nesc(puppy(Puppy2)), falsify(~cute(Puppy2)), dif_objs(Puppy1, Puppy2), nesc(puppy(Puppy3)), falsify(~cute(Puppy3)), dif_objs(Puppy1, Puppy3), nesc(puppy(Puppy4)), falsify(~cute(Puppy4)), dif_objs(Puppy1, Puppy4), nesc(puppy(Puppy5)), dif_objs(Puppy1, Puppy5), falsify(~cute(Puppy5)). make_existential(X, count(4, inf, skF(skIsCuteIsPuppyX_0FnSk, vv(KB, X, KB))), KB) :- ensure_cond(X, puppy(X)), never_cond(X, ~cute(X)). % kbi_define(cute6:puppy/1). % kbi_define(cute6:different/2). % kbi_define(cute6:poss/1). % kbi_define(cute6:(~)/1). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:14 % :- test_boxlog(exactly(2, X_VAR, puppy(X_VAR)&cute(X_VAR))). % kif :- % exactly(2, X, puppy(X)&cute(X)). % nnf :- % ~puppy(X)v~cute(X)v skolem(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), _39514024)&(puppy(X)&cute(X)v~skolem(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), _39514024))&(~puppy(_39511688)v~cute(_39511688)v(~puppy(_39538616)v~cute(_39538616))v~different(_39511688, _39538616)v(~puppy(_39535680)v~cute(_39535680)v~different(_39511688, _39535680))). % to_tnot :- % ( ( ( neg(puppy(X)) % ; neg(cute(X)) % ) % ; nesc(skolem(X, % count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), % _39514024)) % ), % ( nesc(puppy(X)), % nesc(cute(X)) % ; neg(skolem(X, % count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), % _39514024)) % ) % ), % ( ( ( ( neg(puppy(_39511688)) % ; neg(cute(_39511688)) % ) % ; neg(puppy(_39538616)) % ; neg(cute(_39538616)) % ) % ; neg(different(_39511688, _39538616)) % ) % ; ( neg(puppy(_39535680)) % ; neg(cute(_39535680)) % ) % ; neg(different(_39511688, _39535680)) % ). % tlog_nnf :- % ( ( ( n(neg(puppy(X))), % n(neg(cute(X))) % ), % n(nesc(skolem(X, % count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), % _39514024))) % ; ( n(nesc(puppy(X))) % ; n(nesc(cute(X))) % ), % n(neg(skolem(X, % count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), % _39514024))) % ) % ; ( ( ( n(neg(puppy(_39511688))), % n(neg(cute(_39511688))) % ), % n(neg(puppy(_39538616))), % n(neg(cute(_39538616))) % ), % n(neg(different(_39511688, _39538616))) % ), % ( n(neg(puppy(_39535680))), % n(neg(cute(_39535680))) % ), % n(neg(different(_39511688, _39535680))) % ). % tlog_nnf_out_negated :- % n(~puppy(X))&n(~cute(X))&n(nesc(skolem(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), _39514024)))v(n(nesc(puppy(X)))v n(nesc(cute(X)))&n(~skolem(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), _39514024)))v(n(~puppy(_39511688))&n(~cute(_39511688))&(n(~puppy(_39538616))&n(~cute(_39538616)))&n(~different(_39511688, _39538616))&(n(~puppy(_39535680))&n(~cute(_39535680))&n(~different(_39511688, _39535680)))). proven_neg(cute(Cute1)) :- nesc(puppy(Cute1)), nesc(puppy(Puppy2)), nesc(cute(Puppy2)), dif_objs(Cute1, Puppy2), nesc(puppy(Puppy3)), dif_objs(Cute1, Puppy3), nesc(cute(Puppy3)). proven_neg(puppy(Cute1)) :- nesc(cute(Cute1)), nesc(puppy(Puppy2)), nesc(cute(Puppy2)), dif_objs(Cute1, Puppy2), nesc(puppy(Puppy3)), dif_objs(Cute1, Puppy3), nesc(cute(Puppy3)). proven_neg(different(Cute1, Puppy3)) :- nesc(puppy(Puppy3)), nesc(cute(Puppy3)), nesc(puppy(Cute1)), nesc(cute(Cute1)), nesc(puppy(Puppy2)), dif_objs(Cute1, Puppy2), nesc(cute(Puppy2)). proven_tru(cute(X)) :- skolem(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), KB). proven_tru(puppy(X)) :- skolem(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), KB). make_existential(X, count(2, inf, skF(skIsCuteIsX_0FnSk, vv(KB, X))), KB) :- ensure_cond(X, puppy(X)), ensure_cond(X, cute(X)). % kbi_define(cute6:cute/1). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:17 % :- test_boxlog(exactly(5, X_VAR, puppy(X_VAR))). % kif :- % exactly(5, X, puppy(X)). % nnf :- % ~puppy(X)v skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), _40260990)&(puppy(X)v~skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), _40260990))&(~puppy(_40274182)v~different(_40259278, _40274182)v(~puppy(_40276474)v~different(_40259278, _40276474)v(~puppy(_40278766)v~different(_40259278, _40278766)v(~puppy(_40259278)v~puppy(_40283350)v~different(_40259278, _40283350)v(~puppy(_40281058)v~different(_40259278, _40281058)))))). % to_tnot :- % ( ( neg(puppy(X)) % ; nesc(skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), _40260990)) % ), % ( nesc(puppy(X)) % ; neg(skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), _40260990)) % ) % ), % ( ( neg(puppy(_40274182)) % ; neg(different(_40259278, _40274182)) % ) % ; ( neg(puppy(_40276474)) % ; neg(different(_40259278, _40276474)) % ) % ; ( neg(puppy(_40278766)) % ; neg(different(_40259278, _40278766)) % ) % ; ( ( neg(puppy(_40259278)) % ; neg(puppy(_40283350)) % ) % ; neg(different(_40259278, _40283350)) % ) % ; neg(puppy(_40281058)) % ; neg(different(_40259278, _40281058)) % ). % tlog_nnf :- % ( ( n(neg(puppy(X))), % n(nesc(skolem(X, % count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), % _40260990))) % ; n(nesc(puppy(X))), % n(neg(skolem(X, % count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), % _40260990))) % ) % ; ( n(neg(puppy(_40274182))), % n(neg(different(_40259278, _40274182))) % ), % ( n(neg(puppy(_40276474))), % n(neg(different(_40259278, _40276474))) % ), % ( n(neg(puppy(_40278766))), % n(neg(different(_40259278, _40278766))) % ), % ( ( n(neg(puppy(_40259278))), % n(neg(puppy(_40283350))) % ), % n(neg(different(_40259278, _40283350))) % ), % n(neg(puppy(_40281058))), % n(neg(different(_40259278, _40281058))) % ). % tlog_nnf_out_negated :- % n(~puppy(X))&n(nesc(skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), _40260990)))v(n(nesc(puppy(X)))&n(~skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), _40260990)))v(n(~puppy(_40274182))&n(~different(_40259278, _40274182))&(n(~puppy(_40276474))&n(~different(_40259278, _40276474))&(n(~puppy(_40278766))&n(~different(_40259278, _40278766))&(n(~puppy(_40259278))&n(~puppy(_40283350))&n(~different(_40259278, _40283350))&(n(~puppy(_40281058))&n(~different(_40259278, _40281058))))))). proven_neg(puppy(Puppy1)) :- nesc(puppy(Puppy2)), dif_objs(Puppy1, Puppy2), nesc(puppy(Puppy3)), dif_objs(Puppy1, Puppy3), nesc(puppy(Puppy4)), dif_objs(Puppy1, Puppy4), nesc(puppy(Puppy5)), dif_objs(Puppy1, Puppy5), dif_objs(Puppy1, Puppy6), nesc(puppy(Puppy6)). proven_neg(different(Puppy1, Puppy6)) :- nesc(puppy(Puppy6)), nesc(puppy(Puppy5)), dif_objs(Puppy1, Puppy5), nesc(puppy(Puppy4)), dif_objs(Puppy1, Puppy4), nesc(puppy(Puppy1)), nesc(puppy(Puppy2)), dif_objs(Puppy1, Puppy2), dif_objs(Puppy1, Puppy3), nesc(puppy(Puppy3)). proven_tru(puppy(X)) :- skolem(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), KB). make_existential(X, count(5, inf, skF(skIsX_0FnSk, vv(KB, X))), KB) :- ensure_cond(X, puppy(X)). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:20 % :- test_boxlog(forall(X_VAR, iff(cute(X_VAR), not(ugly(X_VAR))))). % kif :- % all(X, (cute(X)<=> ~ugly(X))). % nnf :- % ~cute(X)v~ugly(X)&(ugly(X)v cute(X)). % to_tnot :- % ( neg(cute(X)) % ; neg(ugly(X)) % ), % ( nesc(ugly(X)) % ; nesc(cute(X)) % ). % tlog_nnf :- % ( n(neg(cute(X))), % n(neg(ugly(X))) % ; n(nesc(ugly(X))), % n(nesc(cute(X))) % ). % tlog_nnf_out_negated :- % n(~cute(X))&n(~ugly(X))v(n(nesc(ugly(X)))&n(nesc(cute(X)))). proven_neg(cute(X)) :- nesc(ugly(X)). proven_neg(ugly(X)) :- nesc(cute(X)). proven_tru(cute(X)) :- falsify(ugly(X)). proven_tru(ugly(X)) :- falsify(cute(X)). % kbi_define(cute6:ugly/1). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:23 % :- test_boxlog(forall(X_VAR, if(puppy(X_VAR), ugly(X_VAR)v cute(X_VAR)))). % kif :- % all(X, (puppy(X)=>ugly(X)v cute(X))). % nnf :- % ~puppy(X)v(ugly(X)v cute(X)). % to_tnot :- % ( neg(puppy(X)) % ; nesc(ugly(X)) % ; nesc(cute(X)) % ). % tlog_nnf :- % n(neg(puppy(X))), % n(nesc(ugly(X))), % n(nesc(cute(X))). % tlog_nnf_out_negated :- % n(~puppy(X))&(n(nesc(ugly(X)))&n(nesc(cute(X)))). proven_neg(puppy(X)) :- falsify(ugly(X)), falsify(cute(X)). proven_tru(cute(X)) :- falsify(ugly(X)), nesc(puppy(X)). proven_tru(ugly(X)) :- falsify(cute(X)), nesc(puppy(X)). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:28 % :- test_boxlog({findall(X_VAR, puppy(X_VAR), L_VAR), length(L_VAR, 5)}). % kif :- % { findall(X, puppy(X), L), % length(L, 5) % }. % ensure_quantifiers :- % all(L, all(X, {findall(X, puppy(X), L), length(L, 5)})). % nnf :- % {findall(X, puppy(X), L)}&{length(L, 5)}. % to_tnot :- % nesc({findall(X, puppy(X), L)}), % nesc({length(L, 5)}). % tlog_nnf :- % ( n(nesc({findall(X, puppy(X), L)})) % ; n(nesc({length(L, 5)})) % ). % tlog_nnf_out_negated :- % n(nesc({findall(X, puppy(X), L)}))v n(nesc({length(L, 5)})). nesc({length(L, 5)}). nesc({findall(X, puppy(X), L)}). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:31 % :- test_boxlog({ findall(X_VAR, % ( puppy(X_VAR), % cute(X_VAR) % ), % L_VAR), % length(L_VAR, 2) % }). % kif :- % { findall(X, % ( puppy(X), % cute(X) % ), % L), % length(L, 2) % }. % ensure_quantifiers :- % all(L, all(X, {findall(X, (puppy(X), cute(X)), L), length(L, 2)})). % nnf :- % {findall(X, puppy(X)&cute(X), L)}&{length(L, 2)}. % to_tnot :- % nesc({findall(X, (puppy(X), cute(X)), L)}), % nesc({length(L, 2)}). % tlog_nnf :- % ( n(nesc({findall(X, (puppy(X), cute(X)), L)})) % ; n(nesc({length(L, 2)})) % ). % tlog_nnf_out_negated :- % n(nesc({findall(X, puppy(X)&cute(X), L)}))v n(nesc({length(L, 2)})). nesc({length(L, 2)}). nesc({findall(X, (puppy(X), cute(X)), L)}). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:34 % :- test_boxlog({ findall(X_VAR, % ( puppy(X_VAR), % poss(cute(X_VAR)) % ), % L_VAR), % length(L_VAR, 3) % }). % kif :- % { findall(X, % ( puppy(X), % poss(cute(X)) % ), % L), % length(L, 3) % }. % ensure_quantifiers :- % all(L, all(X, {findall(X, (puppy(X), poss(cute(X))), L), length(L, 3)})). % nnf :- % { findall(X, puppy(X)&poss(cute(X)), L)&length(L, 3) % }. % to_tnot :- % nesc({findall(X, (puppy(X), poss(cute(X))), L), length(L, 3)}). % tlog_nnf :- % n(nesc({findall(X, (puppy(X), poss(cute(X))), L), length(L, 3)})). % tlog_nnf_out_negated :- % n(nesc({findall(X, puppy(X)&poss(cute(X)), L)&length(L, 3)})). nesc({findall(X, (puppy(X), poss(cute(X))), L), length(L, 3)}). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:37 % :- test_boxlog({ findall(X_VAR, % ( puppy(X_VAR), % poss(ugly(X_VAR)) % ), % L_VAR), % length(L_VAR, 1) % }). % kif :- % { findall(X, % ( puppy(X), % poss(ugly(X)) % ), % L), % length(L, 1) % }. % ensure_quantifiers :- % all(L, all(X, {findall(X, (puppy(X), poss(ugly(X))), L), length(L, 1)})). % nnf :- % { findall(X, puppy(X)&poss(ugly(X)), L)&length(L, 1) % }. % to_tnot :- % nesc({findall(X, (puppy(X), poss(ugly(X))), L), length(L, 1)}). % tlog_nnf :- % n(nesc({findall(X, (puppy(X), poss(ugly(X))), L), length(L, 1)})). % tlog_nnf_out_negated :- % n(nesc({findall(X, puppy(X)&poss(ugly(X)), L)&length(L, 1)})). nesc({findall(X, (puppy(X), poss(ugly(X))), L), length(L, 1)}). % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/exactly_poss_cute_06.pfc.pl:39 % kbi_define(cute6:option_setting/2). % init_why(program). % start_x_ide % after_boot % autoloading editline:use_foreign_library/1 from /home/prologmud_server/lib/swipl-7.5.15/library/shlib cute6: ?-