(cd /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol ; timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "['fol_calc_01.pfc.pl']")
%~ init_phase(after_load)
%~ init_phase(restore_state)
%
%~ init_why(after_boot,program)
%~ after_boot.
%~ Dont forget to ?- logicmoo_i_cyc_xform.
running('/var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl'),
%~ /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/logicmoo_test_header.pl:93
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))
:- set_prolog_flag(gc,false).
% =================================================================================
% Set our engine up
% =================================================================================
/*~
~*/
% =================================================================================
% Set our engine up
% =================================================================================
:- expects_dialect(clif).
% deduce instances from usages in args having the effect of deducing human,dwelling,beverage_class are classes
/*~
~*/
% deduce instances from usages in args having the effect of deducing human,dwelling,beverage_class are classes
==> feature_setting(make_wff,true).
/*~
~*/
==> feature_setting(add_admitted_arguments,true).
% set truth maintainance system to remove previous assertions that new assertions disagree with
/*~
~*/
% set truth maintainance system to remove previous assertions that new assertions disagree with
==> feature_setting(tms_mode,remove_conflicting).
/*~
~*/
:- set_prolog_flag(runtime_debug,3). % mention it when we remove previous assertions
/*~
~*/
% mention it when we remove previous assertions
:- set_prolog_flag_until_eof(do_renames,mpred_expansion).
/*~
~*/
:- kif_compile.
% =================================================================================
% Begin program
% =================================================================================
% Create out 14 keys
/*~
~*/
% =================================================================================
% Begin program
% =================================================================================
% Create out 14 keys
exists(Key,glythed(Key,"1")).
/*~
%~ kifi = exists(_3133382,glythed(_3133382,"1")).
%~ kifm = exists(Glythed,nesc(glythed(Glythed,"1"))).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:41
%~ kifm = exists(Nesc_Glythed3,nesc(glythed(Nesc_Glythed3,"1"))).
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"1")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_3015790,glythed(_3015790,"1"))))))
% xgrun compiled into parser_chat80 0.00 sec, 0 clauses
% xgproc compiled into parser_chat80 0.02 sec, 0 clauses
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/clone.xg: 1469 words .. **
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: 488 words .. **
% chatops compiled into parser_chat80 0.00 sec, 0 clauses
% chatops compiled into parser_chat80 0.00 sec, 0 clauses
% :- share_mfa_pt2(parser_chat80,test_chat80,1).
% :- share_mfa_pt2(parser_chat80,hi80,0).
% :- share_mfa_pt2(parser_chat80,hi80,1).
% :- share_mfa_pt2(parser_chat80,control80,1).
% :- share_mfa_pt2(parser_chat80,trace_chat80,1).
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/load compiled into parser_chat80 2.67 sec, 3 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.15 sec, -16 clauses
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"1"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"1")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "1" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"1")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"1")))==>nesc(glythed(Glythed,"1")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"1"))
%~ It's Proof that:
%~ " ?Glythed glythed "1" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"1")))==>nesc(glythed(Glythed,"1")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"1")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"1"))
%~ It's Proof that:
%~ " ?Key glythed "1" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"1")))==>nesc(glythed(Key,"1")).
~*/
exists(Key,glythed(Key,"2")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"2")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_12292784,glythed(_12292784,"2"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"2"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"2")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "2" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"2")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"2")))==>nesc(glythed(Glythed,"2")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"2"))
%~ It's Proof that:
%~ " ?Glythed glythed "2" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"2")))==>nesc(glythed(Glythed,"2")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"2")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"2"))
%~ It's Proof that:
%~ " ?Key glythed "2" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"2")))==>nesc(glythed(Key,"2")).
~*/
exists(Key,glythed(Key,"3")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"3")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_13141350,glythed(_13141350,"3"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"3"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"3")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "3" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"3")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"3")))==>nesc(glythed(Glythed,"3")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"3"))
%~ It's Proof that:
%~ " ?Glythed glythed "3" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"3")))==>nesc(glythed(Glythed,"3")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"3")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"3"))
%~ It's Proof that:
%~ " ?Key glythed "3" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"3")))==>nesc(glythed(Key,"3")).
~*/
exists(Key,glythed(Key,"4")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"4")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_13989924,glythed(_13989924,"4"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"4"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"4")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "4" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"4")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"4")))==>nesc(glythed(Glythed,"4")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"4"))
%~ It's Proof that:
%~ " ?Glythed glythed "4" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"4")))==>nesc(glythed(Glythed,"4")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"4")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"4"))
%~ It's Proof that:
%~ " ?Key glythed "4" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"4")))==>nesc(glythed(Key,"4")).
~*/
exists(Key,glythed(Key,"5")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"5")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_14838506,glythed(_14838506,"5"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"5"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"5")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "5" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"5")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"5")))==>nesc(glythed(Glythed,"5")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"5"))
%~ It's Proof that:
%~ " ?Glythed glythed "5" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"5")))==>nesc(glythed(Glythed,"5")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"5")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"5"))
%~ It's Proof that:
%~ " ?Key glythed "5" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"5")))==>nesc(glythed(Key,"5")).
~*/
exists(Key,glythed(Key,"6")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"6")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_15687096,glythed(_15687096,"6"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"6"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"6")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "6" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"6")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"6")))==>nesc(glythed(Glythed,"6")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"6"))
%~ It's Proof that:
%~ " ?Glythed glythed "6" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"6")))==>nesc(glythed(Glythed,"6")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"6")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"6"))
%~ It's Proof that:
%~ " ?Key glythed "6" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"6")))==>nesc(glythed(Key,"6")).
~*/
exists(Key,glythed(Key,"7")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"7")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_16535694,glythed(_16535694,"7"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"7"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"7")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "7" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"7")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"7")))==>nesc(glythed(Glythed,"7")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"7"))
%~ It's Proof that:
%~ " ?Glythed glythed "7" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"7")))==>nesc(glythed(Glythed,"7")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"7")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"7"))
%~ It's Proof that:
%~ " ?Key glythed "7" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"7")))==>nesc(glythed(Key,"7")).
~*/
exists(Key,glythed(Key,"8")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"8")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_17384300,glythed(_17384300,"8"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"8"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"8")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "8" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"8")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"8")))==>nesc(glythed(Glythed,"8")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"8"))
%~ It's Proof that:
%~ " ?Glythed glythed "8" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"8")))==>nesc(glythed(Glythed,"8")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"8")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"8"))
%~ It's Proof that:
%~ " ?Key glythed "8" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"8")))==>nesc(glythed(Key,"8")).
~*/
exists(Key,glythed(Key,"9")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"9")))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:45
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_18232914,glythed(_18232914,"9"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"9"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"9")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "9" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"9")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"9")))==>nesc(glythed(Glythed,"9")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"9"))
%~ It's Proof that:
%~ " ?Glythed glythed "9" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"9")))==>nesc(glythed(Glythed,"9")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"9")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"9"))
%~ It's Proof that:
%~ " ?Key glythed "9" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"9")))==>nesc(glythed(Key,"9")).
~*/
exists(Key,glythed(Key,"0")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Glythed3'),necessary(glythed('$VAR'('Nesc_Glythed3'),"0")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_19081898,glythed(_19081898,"0"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"0"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"0")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "0" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"0")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"0")))==>nesc(glythed(Glythed,"0")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"0"))
%~ It's Proof that:
%~ " ?Glythed glythed "0" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"0")))==>nesc(glythed(Glythed,"0")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"0")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"0"))
%~ It's Proof that:
%~ " ?Key glythed "0" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"0")))==>nesc(glythed(Key,"0")).
~*/
exists(Key,glythed(Key,"+")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc'),necessary(glythed('$VAR'('Nesc'),"+")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_19930856,glythed(_19930856,"+"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"+"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"+")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "+" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"+")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"+")))==>nesc(glythed(Glythed,"+")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"+"))
%~ It's Proof that:
%~ " ?Glythed glythed "+" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"+")))==>nesc(glythed(Glythed,"+")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"+")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"+"))
%~ It's Proof that:
%~ " ?Key glythed "+" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"+")))==>nesc(glythed(Key,"+")).
~*/
exists(Key,glythed(Key,"-")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc'),necessary(glythed('$VAR'('Nesc'),"-")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_20780556,glythed(_20780556,"-"))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"-"))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"-")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "-" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"-")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"-")))==>nesc(glythed(Glythed,"-")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"-"))
%~ It's Proof that:
%~ " ?Glythed glythed "-" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"-")))==>nesc(glythed(Glythed,"-")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"-")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"-"))
%~ It's Proof that:
%~ " ?Key glythed "-" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"-")))==>nesc(glythed(Key,"-")).
~*/
exists(Key,glythed(Key,"=")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc'),necessary(glythed('$VAR'('Nesc'),"=")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_21629904,glythed(_21629904,"="))))))
=======================================================
exists('$VAR'('Glythed'),glythed('$VAR'('Glythed'),"="))
============================================
?- kif_to_boxlog( exists(Glythed,glythed(Glythed,"=")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed
%~ " ?Glythed glythed "=" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed'),necessary(glythed('$VAR'('Glythed'),"=")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed,1,nesc(glythed(Glythed,"=")))==>nesc(glythed(Glythed,"=")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed nesc(glythed(Glythed,"="))
%~ It's Proof that:
%~ " ?Glythed glythed "=" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Glythed,1,nesc(glythed(Glythed,"=")))==>nesc(glythed(Glythed,"=")).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"=")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"="))
%~ It's Proof that:
%~ " ?Key glythed "=" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"=")))==>nesc(glythed(Key,"=")).
~*/
exists(Key,glythed(Key,"CLR")).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_CLR4'),necessary(glythed('$VAR'('Nesc_CLR4'),"CLR")))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_22479620,glythed(_22479620,"CLR"))))))
=======================================================
exists('$VAR'('Glythed_CLR'),glythed('$VAR'('Glythed_CLR'),"CLR"))
============================================
?- kif_to_boxlog( exists(Glythed_CLR,glythed(Glythed_CLR,"CLR")) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Glythed_CLR
%~ " ?Glythed_CLR glythed "CLR" "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Glythed_CLR'),necessary(glythed('$VAR'('Glythed_CLR'),"CLR")))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Glythed_CLR,1,nesc(glythed(Glythed_CLR,"CLR")))==>nesc(glythed(Glythed_CLR,"CLR")).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Glythed_CLR nesc(glythed(Glythed_CLR,"CLR"))
%~ It's Proof that:
%~ " ?Glythed_CLR glythed "CLR" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(Glythed_CLR,1,nesc(glythed(Glythed_CLR,"CLR"))) ==>
nesc( glythed(Glythed_CLR,"CLR"))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Key'),necessary(glythed('$VAR'('Key'),"CLR")))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Key nesc(glythed(Key,"CLR"))
%~ It's Proof that:
%~ " ?Key glythed "CLR" " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(Key,1,nesc(glythed(Key,"CLR")))==>nesc(glythed(Key,"CLR")).
~*/
:- kif_compile.
/*~
~*/
:- listing(glythed).
% Let same/2 be our unification identify
/*~
%~ skipped( listing(glythed))
~*/
% Let same/2 be our unification identify
all(X,same(X,X)).
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Nesc_Same3'),necessary(same('$VAR'('Nesc_Same3'),'$VAR'('Nesc_Same3'))))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(all(_23358818,same(_23358818,_23358818))))))
=======================================================
all('$VAR'('Same'),same('$VAR'('Same'),'$VAR'('Same')))
============================================
?- kif_to_boxlog( all(Same,same(Same,Same)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Same
%~ " ?Same same ?Same "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Same'),necessary(same('$VAR'('Same'),'$VAR'('Same'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(same(Same,Same)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that ?Same same ?Same
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( same(Same,Same)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),necessary(same('$VAR'('X'),'$VAR'('X'))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that ?X same ?X
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( same(X,X)).
~*/
:- listing(same/2).
% Make each key unique depending on its label
/*~
%~ skipped( listing( same/2))
~*/
% Make each key unique depending on its label
all([Key1,Key2,Label1,Label2],
glythed(Key1,Label1) & glythed(Key2,Label2) & different(Label1,Label2) => different(Key1,Key2)).
% same/2 implies not differnt
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('All_Glythed15'),forall('$VAR'('Different_All_Glythed16'),forall('$VAR'('Glythed_All_Different17'),forall('$VAR'('Different_Glythed_Nesc'),necessary(=>(and(and(glythed('$VAR'('All_Glythed15'),'$VAR'('Glythed_All_Different17')),glythed('$VAR'('Different_All_Glythed16'),'$VAR'('Different_Glythed_Nesc'))),different('$VAR'('Glythed_All_Different17'),'$VAR'('Different_Glythed_Nesc'))),different('$VAR'('All_Glythed15'),'$VAR'('Different_All_Glythed16'))))))))
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( all( [Key1,Key2,Label1,Label2],
%~ ( ( glythed(Key1,Label1) &
%~ glythed(Key2,Label2) &
%~ different(Label1,Label2)) =>
%~ different(Key1,Key2)))))))
=======================================================
all('[|]'('$VAR'('Glythed'),'[|]'('$VAR'('Different_Glythed5'),'[|]'('$VAR'('Glythed_Different'),'[|]'('$VAR'('Different_Glythed8'),[])))),=>(&(&(glythed('$VAR'('Glythed'),'$VAR'('Glythed_Different')),glythed('$VAR'('Different_Glythed5'),'$VAR'('Different_Glythed8'))),different('$VAR'('Glythed_Different'),'$VAR'('Different_Glythed8'))),different('$VAR'('Glythed'),'$VAR'('Different_Glythed5'))))
============================================
?- kif_to_boxlog( all([Glythed,Different_Glythed5,Glythed_Different,Different_Glythed8],((glythed(Glythed,Glythed_Different)&glythed(Different_Glythed5,Different_Glythed8))&different(Glythed_Different,Different_Glythed8))=>different(Glythed,Different_Glythed5)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Glythed ?Different_Glythed5 ?Glythed_Different ?Different_Glythed8
%~ (If:
%~ (" ?Glythed glythed ?Glythed_Different " and
%~ " ?Different_Glythed5 glythed ?Different_Glythed8 " ) and
%~ " ?Glythed_Different different ?Different_Glythed8 " then it is
%~ Implied that:
%~ ?Glythed different ?Different_Glythed5 )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Glythed'),forall('$VAR'('Different_Glythed5'),forall('$VAR'('Glythed_Different'),forall('$VAR'('Different_Glythed8'),necessary(=>(and(and(glythed('$VAR'('Glythed'),'$VAR'('Glythed_Different')),glythed('$VAR'('Different_Glythed5'),'$VAR'('Different_Glythed8'))),different('$VAR'('Glythed_Different'),'$VAR'('Different_Glythed8'))),different('$VAR'('Glythed'),'$VAR'('Different_Glythed5'))))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s):
(nesc(glythed(Different_Glythed5,Different_Glythed8))&nesc(different(Glythed_Different,Different_Glythed8)))&poss(~different(Glythed,Different_Glythed5))==>poss(~glythed(Glythed,Glythed_Different)).
(nesc(glythed(Glythed,Glythed_Different))&nesc(different(Glythed_Different,Different_Glythed8)))&poss(~different(Glythed,Different_Glythed5))==>poss(~glythed(Different_Glythed5,Different_Glythed8)).
(nesc(glythed(Glythed,Glythed_Different))&nesc(glythed(Different_Glythed5,Different_Glythed8)))&nesc(different(Glythed_Different,Different_Glythed8))==>nesc(different(Glythed,Different_Glythed5)).
(nesc(glythed(Glythed,Glythed_Different))&nesc(glythed(Different_Glythed5,Different_Glythed8)))&poss(~different(Glythed,Different_Glythed5))==>poss(~different(Glythed_Different,Different_Glythed8)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Different_Glythed5 glythed ?Different_Glythed8 " is necessarily true and
%~ " ?Glythed_Different different ?Different_Glythed8 " is necessarily true ) and
%~ " ?Glythed different ?Different_Glythed5 " is possibly false
%~ It's Proof that:
%~ " ?Glythed glythed ?Glythed_Different " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Different_Glythed5,Different_Glythed8)) &
nesc( different(Glythed_Different,Different_Glythed8)) &
poss( ~( different(Glythed,Different_Glythed5)))) ==>
poss( ~( glythed(Glythed,Glythed_Different)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Glythed glythed ?Glythed_Different " is necessarily true and
%~ " ?Glythed_Different different ?Different_Glythed8 " is necessarily true ) and
%~ " ?Glythed different ?Different_Glythed5 " is possibly false
%~ It's Proof that:
%~ " ?Different_Glythed5 glythed ?Different_Glythed8 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Glythed,Glythed_Different)) &
nesc( different(Glythed_Different,Different_Glythed8)) &
poss( ~( different(Glythed,Different_Glythed5)))) ==>
poss( ~( glythed(Different_Glythed5,Different_Glythed8)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Glythed glythed ?Glythed_Different " is necessarily true and
%~ " ?Different_Glythed5 glythed ?Different_Glythed8 " is necessarily true ) and
%~ " ?Glythed_Different different ?Different_Glythed8 " is necessarily true
%~ It's Proof that:
%~ " ?Glythed different ?Different_Glythed5 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Glythed,Glythed_Different)) &
nesc( glythed(Different_Glythed5,Different_Glythed8)) &
nesc( different(Glythed_Different,Different_Glythed8))) ==>
nesc( different(Glythed,Different_Glythed5))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Glythed glythed ?Glythed_Different " is necessarily true and
%~ " ?Different_Glythed5 glythed ?Different_Glythed8 " is necessarily true ) and
%~ " ?Glythed different ?Different_Glythed5 " is possibly false
%~ It's Proof that:
%~ " ?Glythed_Different different ?Different_Glythed8 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Glythed,Glythed_Different)) &
nesc( glythed(Different_Glythed5,Different_Glythed8)) &
poss( ~( different(Glythed,Different_Glythed5)))) ==>
poss( ~( different(Glythed_Different,Different_Glythed8)))).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Key1'),forall('$VAR'('Key2'),forall('$VAR'('Label1'),forall('$VAR'('Label2'),necessary(=>(and(and(glythed('$VAR'('Key1'),'$VAR'('Label1')),glythed('$VAR'('Key2'),'$VAR'('Label2'))),different('$VAR'('Label1'),'$VAR'('Label2'))),different('$VAR'('Key1'),'$VAR'('Key2'))))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Key1 glythed ?Label1 " is necessarily true and
%~ " ?Key2 glythed ?Label2 " is necessarily true ) and
%~ " ?Label1 different ?Label2 " is necessarily true
%~ It's Proof that:
%~ " ?Key1 different ?Key2 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Key1,Label1)) &
nesc( glythed(Key2,Label2)) &
nesc( different(Label1,Label2))) ==>
nesc( different(Key1,Key2))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Key1 glythed ?Label1 " is necessarily true and
%~ " ?Key2 glythed ?Label2 " is necessarily true ) and
%~ " ?Key1 different ?Key2 " is possibly false
%~ It's Proof that:
%~ " ?Label1 different ?Label2 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Key1,Label1)) &
nesc( glythed(Key2,Label2)) &
poss( ~( different(Key1,Key2)))) ==>
poss( ~( different(Label1,Label2)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Key2 glythed ?Label2 " is necessarily true and
%~ " ?Label1 different ?Label2 " is necessarily true ) and
%~ " ?Key1 different ?Key2 " is possibly false
%~ It's Proof that:
%~ " ?Key1 glythed ?Label1 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Key2,Label2)) &
nesc( different(Label1,Label2)) &
poss( ~( different(Key1,Key2)))) ==>
poss( ~( glythed(Key1,Label1)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Key1 glythed ?Label1 " is necessarily true and
%~ " ?Label1 different ?Label2 " is necessarily true ) and
%~ " ?Key1 different ?Key2 " is possibly false
%~ It's Proof that:
%~ " ?Key2 glythed ?Label2 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( glythed(Key1,Label1)) &
nesc( different(Label1,Label2)) &
poss( ~( different(Key1,Key2)))) ==>
poss( ~( glythed(Key2,Label2)))).
~*/
% same/2 implies not differnt
all([X,Y], same(X,Y) => ~ different(X,Y)).
% Note all unquantified vars will be universal from here on out
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('All_Same7'),forall('$VAR'('Different_Same_Nesc'),necessary(=>(same('$VAR'('All_Same7'),'$VAR'('Different_Same_Nesc')),not(different('$VAR'('All_Same7'),'$VAR'('Different_Same_Nesc')))))))
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( all([X,Y],same(X,Y)=>(~different(X,Y)))))))
=======================================================
all('[|]'('$VAR'('Same'),'[|]'('$VAR'('Different_Same3'),[])),=>(same('$VAR'('Same'),'$VAR'('Different_Same3')),~(different('$VAR'('Same'),'$VAR'('Different_Same3')))))
============================================
?- kif_to_boxlog( all([Same,Different_Same3],same(Same,Different_Same3)=>(~different(Same,Different_Same3))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Same ?Different_Same3
%~ (If:
%~ ?Same same ?Different_Same3 then it is
%~ Implied that:
%~ " ?Same different ?Different_Same3 " is false)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Same'),forall('$VAR'('Different_Same3'),necessary(=>(same('$VAR'('Same'),'$VAR'('Different_Same3')),not(different('$VAR'('Same'),'$VAR'('Different_Same3')))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s):
nesc(same(Same,Different_Same3))==>nesc(~different(Same,Different_Same3)).
poss(different(Same,Different_Same3))==>poss(~same(Same,Different_Same3)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Same same ?Different_Same3 " is necessarily true
%~ It's Proof that:
%~ " ?Same different ?Different_Same3 " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(same(Same,Different_Same3))==>nesc(~different(Same,Different_Same3)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Same different ?Different_Same3 " is possible
%~ It's Proof that:
%~ " ?Same same ?Different_Same3 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(different(Same,Different_Same3))==>poss(~same(Same,Different_Same3)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),forall('$VAR'('Y'),necessary(=>(same('$VAR'('X'),'$VAR'('Y')),not(different('$VAR'('X'),'$VAR'('Y')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X different ?Y " is possible
%~ It's Proof that:
%~ " ?X same ?Y " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(different(X,Y))==>poss(~same(X,Y)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X same ?Y " is necessarily true
%~ It's Proof that:
%~ " ?X different ?Y " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(same(X,Y))==>nesc(~different(X,Y)).
~*/
% Note all unquantified vars will be universal from here on out
subclass(S,C) & inst(I,S) => inst(I,C).
% an accumulator is a numeric buffer
/*~
%~ kif_to_boxlog_attvars2 = necessary(=>(and(genls('$VAR'('Inst_Genls'),'$VAR'('Inst_Genls13')),inst('$VAR'('Inst12'),'$VAR'('Inst_Genls'))),inst('$VAR'('Inst12'),'$VAR'('Inst_Genls13'))))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:66
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( (subclass(S,C)&inst(I,S))=>inst(I,C)))))
=======================================================
=>(&(subclass('$VAR'('Inst_Subclass'),'$VAR'('Inst_Subclass5')),inst('$VAR'('Inst'),'$VAR'('Inst_Subclass'))),inst('$VAR'('Inst'),'$VAR'('Inst_Subclass5')))
============================================
?- kif_to_boxlog( (subclass(Inst_Subclass,Inst_Subclass5)&inst(Inst,Inst_Subclass))=>inst(Inst,Inst_Subclass5) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ If:
%~ " ?Inst_Subclass subclass ?Inst_Subclass5 " and
%~ " ?Inst inst ?Inst_Subclass " then it is
%~ Implied that:
%~ ?Inst inst ?Inst_Subclass5
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(=>(and(genls('$VAR'('Inst_Subclass'),'$VAR'('Inst_Subclass5')),inst('$VAR'('Inst'),'$VAR'('Inst_Subclass'))),inst('$VAR'('Inst'),'$VAR'('Inst_Subclass5'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 3 entailment(s):
nesc(genls(Inst_Subclass,Inst_Subclass5))&nesc(inst(Inst,Inst_Subclass))==>nesc(inst(Inst,Inst_Subclass5)).
poss(~inst(Inst,Inst_Subclass5))&nesc(genls(Inst_Subclass,Inst_Subclass5))==>poss(~inst(Inst,Inst_Subclass)).
poss(~inst(Inst,Inst_Subclass5))&nesc(inst(Inst,Inst_Subclass))==>poss(~genls(Inst_Subclass,Inst_Subclass5)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Inst_Subclass genls ?Inst_Subclass5 " is necessarily true and
%~ " ?Inst inst ?Inst_Subclass " is necessarily true
%~ It's Proof that:
%~ " ?Inst inst ?Inst_Subclass5 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(genls(Inst_Subclass,Inst_Subclass5))&nesc(inst(Inst,Inst_Subclass)) ==>
nesc( inst(Inst,Inst_Subclass5))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Inst inst ?Inst_Subclass5 " is possibly false and
%~ " ?Inst_Subclass genls ?Inst_Subclass5 " is necessarily true
%~ It's Proof that:
%~ " ?Inst inst ?Inst_Subclass " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( poss( ~( inst(Inst,Inst_Subclass5))) &
nesc( genls(Inst_Subclass,Inst_Subclass5))) ==>
poss( ~( inst(Inst,Inst_Subclass)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Inst inst ?Inst_Subclass5 " is possibly false and
%~ " ?Inst inst ?Inst_Subclass " is necessarily true
%~ It's Proof that:
%~ " ?Inst_Subclass genls ?Inst_Subclass5 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(~inst(Inst,Inst_Subclass5))&nesc(inst(Inst,Inst_Subclass)) ==>
poss( ~( genls(Inst_Subclass,Inst_Subclass5)))).
============================================
%~ kif_to_boxlog_attvars2 = necessary(=>(and(genls('$VAR'('S'),'$VAR'('C')),inst('$VAR'('I'),'$VAR'('S'))),inst('$VAR'('I'),'$VAR'('C'))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?S genls ?C " is necessarily true and
%~ " ?I inst ?S " is necessarily true
%~ It's Proof that:
%~ " ?I inst ?C " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(genls(S,C))&nesc(inst(I,S))==>nesc(inst(I,C)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?I inst ?C " is possibly false and
%~ " ?I inst ?S " is necessarily true
%~ It's Proof that:
%~ " ?S genls ?C " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(~inst(I,C))&nesc(inst(I,S)) ==>
poss( ~( genls(S,C)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?I inst ?C " is possibly false and
%~ " ?S genls ?C " is necessarily true
%~ It's Proof that:
%~ " ?I inst ?S " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( poss(~inst(I,C))&nesc(genls(S,C)) ==>
poss( ~( inst(I,S)))).
~*/
% an accumulator is a numeric buffer
subclass(accumulator,numbuffer).
% a display is a numeric buffer
/*~
%~ kif_to_boxlog_attvars2 = necessary(genls(accumulator,numbuffer))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(subclass(accumulator,numbuffer)))))
=======================================================
subclass(accumulator,numbuffer)
============================================
?- kif_to_boxlog( subclass(accumulator,numbuffer) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ accumulator subclass numbuffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(genls(accumulator,numbuffer))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(genls(accumulator,numbuffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that accumulator genls numbuffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( genls(accumulator,numbuffer)).
============================================
~*/
% a display is a numeric buffer
subclass(display,numbuffer).
% numeric buffer and operation buffer are buffers
/*~
%~ kif_to_boxlog_attvars2 = necessary(genls(display,numbuffer))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:72
%~ warn( really_remake_as_dynamic(
%~ edinburgh : display(Display),
%~ for(baseKB,decl_kb_type(kb_shared,baseKB:display/1))))
%~ warn( really_remake_as_dynamic2(edinburgh:display(Display),bc(decl_kb_type(kb_shared,baseKB:display/1))))
_42251488
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(subclass(display,numbuffer)))))
=======================================================
subclass(display,numbuffer)
============================================
?- kif_to_boxlog( subclass(display,numbuffer) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ display subclass numbuffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(genls(display,numbuffer))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(genls(display,numbuffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that display genls numbuffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( genls(display,numbuffer)).
============================================
~*/
% numeric buffer and operation buffer are buffers
subclass(numbuffer,buffer).
/*~
%~ kif_to_boxlog_attvars2 = necessary(genls(numbuffer,buffer))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(subclass(numbuffer,buffer)))))
=======================================================
subclass(numbuffer,buffer)
============================================
?- kif_to_boxlog( subclass(numbuffer,buffer) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ numbuffer subclass buffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(genls(numbuffer,buffer))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(genls(numbuffer,buffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that numbuffer genls buffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( genls(numbuffer,buffer)).
============================================
~*/
subclass(opbuffer,buffer).
% Create some buffers
/*~
%~ kif_to_boxlog_attvars2 = necessary(genls(opbuffer,buffer))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(subclass(opbuffer,buffer)))))
=======================================================
subclass(opbuffer,buffer)
============================================
?- kif_to_boxlog( subclass(opbuffer,buffer) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ opbuffer subclass buffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(genls(opbuffer,buffer))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
nesc(genls(opbuffer,buffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ it is necessarily true that opbuffer genls buffer
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc( genls(opbuffer,buffer)).
============================================
~*/
% Create some buffers
exists(X,inst(X,accumulator)).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Accumulator4'),necessary(inst('$VAR'('Nesc_Accumulator4'),accumulator)))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_43258076,inst(_43258076,accumulator))))))
=======================================================
exists('$VAR'('Inst_Accumulator'),inst('$VAR'('Inst_Accumulator'),accumulator))
============================================
?- kif_to_boxlog( exists(Inst_Accumulator,inst(Inst_Accumulator,accumulator)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Inst_Accumulator
%~ " ?Inst_Accumulator inst accumulator "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Inst_Accumulator'),necessary(inst('$VAR'('Inst_Accumulator'),accumulator)))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Inst_Accumulator,1,nesc(inst(Inst_Accumulator,accumulator)))==>nesc(inst(Inst_Accumulator,accumulator)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Inst_Accumulator nesc(inst(Inst_Accumulator,accumulator))
%~ It's Proof that:
%~ " ?Inst_Accumulator inst accumulator " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(Inst_Accumulator,1,nesc(inst(Inst_Accumulator,accumulator))) ==>
nesc( inst(Inst_Accumulator,accumulator))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(inst('$VAR'('X'),accumulator)))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?X nesc(inst(X,accumulator))
%~ It's Proof that:
%~ " ?X inst accumulator " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(X,1,nesc(inst(X,accumulator)))==>nesc(inst(X,accumulator)).
~*/
exists(X,inst(X,display)).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Display4'),necessary(inst('$VAR'('Nesc_Display4'),display)))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_44113978,inst(_44113978,display))))))
=======================================================
exists('$VAR'('Inst_Display'),inst('$VAR'('Inst_Display'),display))
============================================
?- kif_to_boxlog( exists(Inst_Display,inst(Inst_Display,display)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Inst_Display
%~ " ?Inst_Display inst display "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Inst_Display'),necessary(inst('$VAR'('Inst_Display'),display)))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Inst_Display,1,nesc(inst(Inst_Display,display)))==>nesc(inst(Inst_Display,display)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Inst_Display nesc(inst(Inst_Display,display))
%~ It's Proof that:
%~ " ?Inst_Display inst display " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(Inst_Display,1,nesc(inst(Inst_Display,display))) ==>
nesc( inst(Inst_Display,display))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(inst('$VAR'('X'),display)))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?X nesc(inst(X,display))
%~ It's Proof that:
%~ " ?X inst display " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(X,1,nesc(inst(X,display)))==>nesc(inst(X,display)).
~*/
exists(X,inst(X,opbuffer)).
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Nesc_Opbuffer4'),necessary(inst('$VAR'('Nesc_Opbuffer4'),opbuffer)))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:80
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_44965772,inst(_44965772,opbuffer))))))
=======================================================
exists('$VAR'('Inst_Opbuffer'),inst('$VAR'('Inst_Opbuffer'),opbuffer))
============================================
?- kif_to_boxlog( exists(Inst_Opbuffer,inst(Inst_Opbuffer,opbuffer)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Inst_Opbuffer
%~ " ?Inst_Opbuffer inst opbuffer "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Inst_Opbuffer'),necessary(inst('$VAR'('Inst_Opbuffer'),opbuffer)))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Inst_Opbuffer,1,nesc(inst(Inst_Opbuffer,opbuffer)))==>nesc(inst(Inst_Opbuffer,opbuffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Inst_Opbuffer nesc(inst(Inst_Opbuffer,opbuffer))
%~ It's Proof that:
%~ " ?Inst_Opbuffer inst opbuffer " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(Inst_Opbuffer,1,nesc(inst(Inst_Opbuffer,opbuffer))) ==>
nesc( inst(Inst_Opbuffer,opbuffer))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('X'),necessary(inst('$VAR'('X'),opbuffer)))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?X nesc(inst(X,opbuffer))
%~ It's Proof that:
%~ " ?X inst opbuffer " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(X,1,nesc(inst(X,opbuffer)))==>nesc(inst(X,opbuffer)).
~*/
/*
Extra TODO ?
define how a buffer is shown in screen locations
exactly(10,X, inst(X,screenLocation)).
*/
% All number buffers have a, inital value of 0
(all(X,inst(X,numbuffer) => initalValue(X,0))).
% exists an initial world
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Nesc_Numbuffer3'),necessary(=>(inst('$VAR'('Nesc_Numbuffer3'),numbuffer),initalValue('$VAR'('Nesc_Numbuffer3'),0))))
%~ debugm( baseKB,
%~ show_success(baseKB,baseKB:ain(clif(all(X,inst(X,numbuffer)=>initalValue(X,0))))))
=======================================================
all('$VAR'('Numbuffer'),=>(inst('$VAR'('Numbuffer'),numbuffer),initalValue('$VAR'('Numbuffer'),0)))
============================================
?- kif_to_boxlog( all(Numbuffer,inst(Numbuffer,numbuffer)=>initalValue(Numbuffer,0)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Numbuffer
%~ (If:
%~ ?Numbuffer inst numbuffer then it is
%~ Implied that:
%~ ?Numbuffer initalValue 0 )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Numbuffer'),necessary(=>(inst('$VAR'('Numbuffer'),numbuffer),initalValue('$VAR'('Numbuffer'),0))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s):
nesc(inst(Numbuffer,numbuffer))==>nesc(initalValue(Numbuffer,0)).
poss(~initalValue(Numbuffer,0))==>poss(~inst(Numbuffer,numbuffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Numbuffer inst numbuffer " is necessarily true
%~ It's Proof that:
%~ " ?Numbuffer initalValue 0 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(inst(Numbuffer,numbuffer))==>nesc(initalValue(Numbuffer,0)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Numbuffer initalValue 0 " is possibly false
%~ It's Proof that:
%~ " ?Numbuffer inst numbuffer " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(~initalValue(Numbuffer,0))==>poss(~inst(Numbuffer,numbuffer)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),necessary(=>(inst('$VAR'('X'),numbuffer),initalValue('$VAR'('X'),0))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X initalValue 0 " is possibly false
%~ It's Proof that:
%~ " ?X inst numbuffer " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(~initalValue(X,0))==>poss(~inst(X,numbuffer)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X inst numbuffer " is necessarily true
%~ It's Proof that:
%~ " ?X initalValue 0 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(inst(X,numbuffer))==>nesc(initalValue(X,0)).
~*/
% exists an initial world
exists(C,initialWorld(C)).
% initial world is populated by inital values
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('InitialWorld_Nesc'),necessary(initialWorld('$VAR'('InitialWorld_Nesc'))))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:94
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_47593036,initialWorld(_47593036))))))
=======================================================
exists('$VAR'('InitialWorld'),initialWorld('$VAR'('InitialWorld')))
============================================
?- kif_to_boxlog( exists(InitialWorld,initialWorld(InitialWorld)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?InitialWorld
%~ " ?InitialWorld isa initialWorld "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('InitialWorld'),necessary(initialWorld('$VAR'('InitialWorld'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(InitialWorld,1,nesc(initialWorld(InitialWorld)))==>nesc(initialWorld(InitialWorld)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?InitialWorld nesc(initialWorld(InitialWorld))
%~ It's Proof that:
%~ " ?InitialWorld isa initialWorld " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(InitialWorld,1,nesc(initialWorld(InitialWorld))) ==>
nesc( initialWorld(InitialWorld))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('C'),necessary(initialWorld('$VAR'('C'))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?C nesc(initialWorld(C))
%~ It's Proof that:
%~ " ?C isa initialWorld " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(C,1,nesc(initialWorld(C)))==>nesc(initialWorld(C)).
~*/
% initial world is populated by inital values
initalValue(N,V) & initialWorld(W) => currentValue(W,N,V).
% All numeric buffers have a value
/*~
%~ kif_to_boxlog_attvars2 = necessary(=>(and(initalValue('$VAR'('InitalValue11'),'$VAR'('CurrentValue_InitalValue13')),initialWorld('$VAR'('InitialWorld_CurrentValue12'))),currentValue('$VAR'('InitialWorld_CurrentValue12'),'$VAR'('InitalValue11'),'$VAR'('CurrentValue_InitalValue13'))))
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( (initalValue(N,V)&initialWorld(W))=>currentValue(W,N,V)))))
=======================================================
=>(&(initalValue('$VAR'('InitalValue'),'$VAR'('CurrentValue_InitalValue5')),initialWorld('$VAR'('InitialWorld_CurrentValue'))),currentValue('$VAR'('InitialWorld_CurrentValue'),'$VAR'('InitalValue'),'$VAR'('CurrentValue_InitalValue5')))
============================================
?- kif_to_boxlog( (initalValue(InitalValue,CurrentValue_InitalValue5)&initialWorld(InitialWorld_CurrentValue))=>currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ If:
%~ " ?InitalValue initalValue ?CurrentValue_InitalValue5 " and
%~ " ?InitialWorld_CurrentValue isa initialWorld " then it is
%~ Implied that:
%~ currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(=>(and(initalValue('$VAR'('InitalValue'),'$VAR'('CurrentValue_InitalValue5')),initialWorld('$VAR'('InitialWorld_CurrentValue'))),currentValue('$VAR'('InitialWorld_CurrentValue'),'$VAR'('InitalValue'),'$VAR'('CurrentValue_InitalValue5'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 3 entailment(s):
nesc(initialWorld(InitialWorld_CurrentValue))&poss(~currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5))==>poss(~initalValue(InitalValue,CurrentValue_InitalValue5)).
nesc(initalValue(InitalValue,CurrentValue_InitalValue5))&nesc(initialWorld(InitialWorld_CurrentValue))==>nesc(currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5)).
nesc(initalValue(InitalValue,CurrentValue_InitalValue5))&poss(~currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5))==>poss(~initialWorld(InitialWorld_CurrentValue)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?InitialWorld_CurrentValue isa initialWorld " is necessarily true and
%~ " currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5) " is possibly false
%~ It's Proof that:
%~ " ?InitalValue initalValue ?CurrentValue_InitalValue5 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( initialWorld(InitialWorld_CurrentValue)) &
poss( ~( currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5)))) ==>
poss( ~( initalValue(InitalValue,CurrentValue_InitalValue5)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?InitalValue initalValue ?CurrentValue_InitalValue5 " is necessarily true and
%~ " ?InitialWorld_CurrentValue isa initialWorld " is necessarily true
%~ It's Proof that:
%~ " currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5) " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( initalValue(InitalValue,CurrentValue_InitalValue5)) &
nesc( initialWorld(InitialWorld_CurrentValue))) ==>
nesc( currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?InitalValue initalValue ?CurrentValue_InitalValue5 " is necessarily true and
%~ " currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5) " is possibly false
%~ It's Proof that:
%~ " ?InitialWorld_CurrentValue isa initialWorld " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( initalValue(InitalValue,CurrentValue_InitalValue5)) &
poss( ~( currentValue(InitialWorld_CurrentValue,InitalValue,CurrentValue_InitalValue5)))) ==>
poss( ~( initialWorld(InitialWorld_CurrentValue)))).
============================================
%~ kif_to_boxlog_attvars2 = necessary(=>(and(initalValue('$VAR'('N'),'$VAR'(v)),initialWorld('$VAR'('W'))),currentValue('$VAR'('W'),'$VAR'('N'),'$VAR'(v))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((?N initalValue ?v )is necessarily true ) and
%~ " ?W isa initialWorld " is necessarily true
%~ It's Proof that:
%~ (currentValue(W,N,'$VAR'(v)) )is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(initalValue(N,'$VAR'(v)))&nesc(initialWorld(W)) ==>
nesc( currentValue(W,N,'$VAR'(v)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?W isa initialWorld " is necessarily true and
%~ ((currentValue(W,N,'$VAR'(v)) )is possibly false )
%~ It's Proof that:
%~ (?N initalValue ?v )is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(initialWorld(W))&poss(~currentValue(W,N,'$VAR'(v))) ==>
poss( ~( initalValue(N,'$VAR'(v))))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ ((?N initalValue ?v )is necessarily true ) and
%~ ((currentValue(W,N,'$VAR'(v)) )is possibly false )
%~ It's Proof that:
%~ " ?W isa initialWorld " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(initalValue(N,'$VAR'(v)))&poss(~currentValue(W,N,'$VAR'(v))) ==>
poss( ~( initialWorld(W)))).
~*/
% All numeric buffers have a value
all(W,all(N,exists(V,inst(N,numbuffer) & world(W) => currentValue(W,N,V)))).
% Op buffer is intialized to null
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('World_All_CurrentValue13'),forall('$VAR'('Exists_Numbuffer12'),exists('$VAR'('CurrentValue_Nesc'),necessary(=>(and(inst('$VAR'('Exists_Numbuffer12'),numbuffer),world('$VAR'('World_All_CurrentValue13'))),currentValue('$VAR'('World_All_CurrentValue13'),'$VAR'('Exists_Numbuffer12'),'$VAR'('CurrentValue_Nesc')))))))
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( all( W,
%~ all( N,
%~ exists( V,
%~ (inst(N,numbuffer)&world(W))=>currentValue(W,N,V))))))))
=======================================================
all('$VAR'('World_All_CurrentValue'),all('$VAR'('Exists_Numbuffer'),exists('$VAR'('CurrentValue8'),=>(&(inst('$VAR'('Exists_Numbuffer'),numbuffer),world('$VAR'('World_All_CurrentValue'))),currentValue('$VAR'('World_All_CurrentValue'),'$VAR'('Exists_Numbuffer'),'$VAR'('CurrentValue8'))))))
============================================
?- kif_to_boxlog( all(World_All_CurrentValue,all(Exists_Numbuffer,exists(CurrentValue8,(inst(Exists_Numbuffer,numbuffer)&world(World_All_CurrentValue))=>currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8)))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?World_All_CurrentValue
%~ (
%~ For all ?Exists_Numbuffer
%~ (
%~ There exists ?CurrentValue8
%~ (If:
%~ " ?Exists_Numbuffer inst numbuffer " and
%~ " ?World_All_CurrentValue isa world " then it is
%~ Implied that:
%~ currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8) )))
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('World_All_CurrentValue'),forall('$VAR'('Exists_Numbuffer'),exists('$VAR'('CurrentValue8'),necessary(=>(and(inst('$VAR'('Exists_Numbuffer'),numbuffer),world('$VAR'('World_All_CurrentValue'))),currentValue('$VAR'('World_All_CurrentValue'),'$VAR'('Exists_Numbuffer'),'$VAR'('CurrentValue8')))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 3 entailment(s):
nesc(world(World_All_CurrentValue))&poss(~currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8))==>poss(~inst(Exists_Numbuffer,numbuffer)).
nesc(inst(Exists_Numbuffer,numbuffer))&poss(~currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8))==>poss(~world(World_All_CurrentValue)).
(nesc(inst(Exists_Numbuffer,numbuffer))&nesc(world(World_All_CurrentValue)))&'$existential'(CurrentValue8,1,(nesc(inst(Exists_Numbuffer,numbuffer))&nesc(world(World_All_CurrentValue)))=>nesc(currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8)))==>nesc(currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?World_All_CurrentValue isa world " is necessarily true and
%~ " currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8) " is possibly false
%~ It's Proof that:
%~ " ?Exists_Numbuffer inst numbuffer " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( world(World_All_CurrentValue)) &
poss( ~( currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8)))) ==>
poss( ~( inst(Exists_Numbuffer,numbuffer)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Exists_Numbuffer inst numbuffer " is necessarily true and
%~ " currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8) " is possibly false
%~ It's Proof that:
%~ " ?World_All_CurrentValue isa world " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( inst(Exists_Numbuffer,numbuffer)) &
poss( ~( currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8)))) ==>
poss( ~( world(World_All_CurrentValue)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?Exists_Numbuffer inst numbuffer " is necessarily true and
%~ " ?World_All_CurrentValue isa world " is necessarily true ) and
%~ by default ?CurrentValue8 (nesc(inst(Exists_Numbuffer,numbuffer))&nesc(world(World_All_CurrentValue)))=>nesc(currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8))
%~ It's Proof that:
%~ " currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8) " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( inst(Exists_Numbuffer,numbuffer)) &
nesc( world(World_All_CurrentValue)) &
'$existential'( CurrentValue8,
1,
( nesc(inst(Exists_Numbuffer,numbuffer))&nesc(world(World_All_CurrentValue)) =>
nesc( currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8))))) ==>
nesc( currentValue(World_All_CurrentValue,Exists_Numbuffer,CurrentValue8))).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('W'),forall('$VAR'('N'),exists('$VAR'(v),necessary(=>(and(inst('$VAR'('N'),numbuffer),world('$VAR'('W'))),currentValue('$VAR'('W'),'$VAR'('N'),'$VAR'(v)))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ (" ?N inst numbuffer " is necessarily true and
%~ " ?W isa world " is necessarily true ) and
%~ by default ?v (nesc(inst(N,numbuffer))&nesc(world(W)))=>nesc(currentValue(W,N,'$VAR'(v)))
%~ It's Proof that:
%~ (currentValue(W,N,'$VAR'(v)) )is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( ( nesc( inst(N,numbuffer)) &
nesc( world(W)) &
'$existential'( '$VAR'(v),
1,
( nesc(inst(N,numbuffer))&nesc(world(W)) =>
nesc( currentValue(W,N,'$VAR'(v)))))) ==>
nesc( currentValue(W,N,'$VAR'(v)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?W isa world " is necessarily true and
%~ ((currentValue(W,N,'$VAR'(v)) )is possibly false )
%~ It's Proof that:
%~ " ?N inst numbuffer " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(world(W))&poss(~currentValue(W,N,'$VAR'(v))) ==>
poss( ~( inst(N,numbuffer)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?N inst numbuffer " is necessarily true and
%~ ((currentValue(W,N,'$VAR'(v)) )is possibly false )
%~ It's Proof that:
%~ " ?W isa world " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(inst(N,numbuffer))&poss(~currentValue(W,N,'$VAR'(v))) ==>
poss( ~( world(W)))).
~*/
% Op buffer is intialized to null
all(X,inst(X,opbuffer) => initalValue(X,null)).
% exists a current world (Fluent 1)
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Nesc_Null_Opbuffer4'),necessary(=>(inst('$VAR'('Nesc_Null_Opbuffer4'),opbuffer),initalValue('$VAR'('Nesc_Null_Opbuffer4'),null))))
%~ debugm( baseKB,
%~ show_success(baseKB,baseKB:ain(clif(all(X,inst(X,opbuffer)=>initalValue(X,null))))))
=======================================================
all('$VAR'('Null_Opbuffer'),=>(inst('$VAR'('Null_Opbuffer'),opbuffer),initalValue('$VAR'('Null_Opbuffer'),null)))
============================================
?- kif_to_boxlog( all(Null_Opbuffer,inst(Null_Opbuffer,opbuffer)=>initalValue(Null_Opbuffer,null)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Null_Opbuffer
%~ (If:
%~ ?Null_Opbuffer inst opbuffer then it is
%~ Implied that:
%~ ?Null_Opbuffer initalValue null )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Null_Opbuffer'),necessary(=>(inst('$VAR'('Null_Opbuffer'),opbuffer),initalValue('$VAR'('Null_Opbuffer'),null))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s):
nesc(inst(Null_Opbuffer,opbuffer))==>nesc(initalValue(Null_Opbuffer,null)).
poss(~initalValue(Null_Opbuffer,null))==>poss(~inst(Null_Opbuffer,opbuffer)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Null_Opbuffer inst opbuffer " is necessarily true
%~ It's Proof that:
%~ " ?Null_Opbuffer initalValue null " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(inst(Null_Opbuffer,opbuffer))==>nesc(initalValue(Null_Opbuffer,null)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Null_Opbuffer initalValue null " is possibly false
%~ It's Proof that:
%~ " ?Null_Opbuffer inst opbuffer " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(~initalValue(Null_Opbuffer,null))==>poss(~inst(Null_Opbuffer,opbuffer)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),necessary(=>(inst('$VAR'('X'),opbuffer),initalValue('$VAR'('X'),null))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X initalValue null " is possibly false
%~ It's Proof that:
%~ " ?X inst opbuffer " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(~initalValue(X,null))==>poss(~inst(X,opbuffer)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?X inst opbuffer " is necessarily true
%~ It's Proof that:
%~ " ?X initalValue null " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(inst(X,opbuffer))==>nesc(initalValue(X,null)).
~*/
% exists a current world (Fluent 1)
exists(C,currentWorld(C)).
%:- rtrace.
/*~
%~ kif_to_boxlog_attvars2 = exists('$VAR'('CurrentWorld_Nesc'),necessary(currentWorld('$VAR'('CurrentWorld_Nesc'))))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_61559882,currentWorld(_61559882))))))
=======================================================
exists('$VAR'('CurrentWorld'),currentWorld('$VAR'('CurrentWorld')))
============================================
?- kif_to_boxlog( exists(CurrentWorld,currentWorld(CurrentWorld)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?CurrentWorld
%~ " ?CurrentWorld isa currentWorld "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('CurrentWorld'),necessary(currentWorld('$VAR'('CurrentWorld'))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(CurrentWorld,1,nesc(currentWorld(CurrentWorld)))==>nesc(currentWorld(CurrentWorld)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?CurrentWorld nesc(currentWorld(CurrentWorld))
%~ It's Proof that:
%~ " ?CurrentWorld isa currentWorld " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(CurrentWorld,1,nesc(currentWorld(CurrentWorld))) ==>
nesc( currentWorld(CurrentWorld))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('C'),necessary(currentWorld('$VAR'('C'))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?C nesc(currentWorld(C))
%~ It's Proof that:
%~ " ?C isa currentWorld " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(C,1,nesc(currentWorld(C)))==>nesc(currentWorld(C)).
~*/
%:- rtrace.
nextWorld(C,N) => inst(C,world) & inst(N,world).
/*~
%~ kif_to_boxlog_attvars2 = necessary(=>(nextWorld('$VAR'('NextWorld6'),'$VAR'('NextWorld_World7')),and(inst('$VAR'('NextWorld6'),world),inst('$VAR'('NextWorld_World7'),world))))
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/fol_calc_01.pfc.pl:109
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( nextWorld(C,N)=>(inst(C,world)&inst(N,world))))))
=======================================================
=>(nextWorld('$VAR'('NextWorld'),'$VAR'('World')),&(inst('$VAR'('NextWorld'),world),inst('$VAR'('World'),world)))
============================================
?- kif_to_boxlog( nextWorld(NextWorld,World)=>(inst(NextWorld,world)&inst(World,world)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ If:
%~ ?NextWorld nextWorld ?World then it is
%~ Implied that:
%~ " ?NextWorld inst world " and
%~ " ?World inst world "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(=>(nextWorld('$VAR'('NextWorld'),'$VAR'('World')),and(inst('$VAR'('NextWorld'),world),inst('$VAR'('World'),world))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 6 entailment(s):
nesc(inst(NextWorld,world))&poss(~inst(World,world))==>poss(~nextWorld(NextWorld,World)).
nesc(inst(World,world))&poss(~inst(NextWorld,world))==>poss(~nextWorld(NextWorld,World)).
nesc(nextWorld(NextWorld,World))&nesc(inst(NextWorld,world))==>nesc(inst(World,world)).
nesc(nextWorld(NextWorld,World))&nesc(inst(World,world))==>nesc(inst(NextWorld,world)).
nesc(nextWorld(NextWorld,World))&poss(~inst(NextWorld,world))==>poss(~inst(World,world)).
nesc(nextWorld(NextWorld,World))&poss(~inst(World,world))==>poss(~inst(NextWorld,world)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?NextWorld inst world " is necessarily true and
%~ " ?World inst world " is possibly false
%~ It's Proof that:
%~ " ?NextWorld nextWorld ?World " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(inst(NextWorld,world))&poss(~inst(World,world)) ==>
poss( ~( nextWorld(NextWorld,World)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?World inst world " is necessarily true and
%~ " ?NextWorld inst world " is possibly false
%~ It's Proof that:
%~ " ?NextWorld nextWorld ?World " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(inst(World,world))&poss(~inst(NextWorld,world)) ==>
poss( ~( nextWorld(NextWorld,World)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?NextWorld nextWorld ?World " is necessarily true and
%~ " ?NextWorld inst world " is necessarily true
%~ It's Proof that:
%~ " ?World inst world " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(nextWorld(NextWorld,World))&nesc(inst(NextWorld,world)) ==>
nesc( inst(World,world))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?NextWorld nextWorld ?World " is necessarily true and
%~ " ?World inst world " is necessarily true
%~ It's Proof that:
%~ " ?NextWorld inst world " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(nextWorld(NextWorld,World))&nesc(inst(World,world)) ==>
nesc( inst(NextWorld,world))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?NextWorld nextWorld ?World " is necessarily true and
%~ " ?NextWorld inst world " is possibly false
%~ It's Proof that:
%~ " ?World inst world " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(nextWorld(NextWorld,World))&poss(~inst(NextWorld,world)) ==>
poss( ~( inst(World,world)))).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?NextWorld nextWorld ?World " is necessarily true and
%~ " ?World inst world " is possibly false
%~ It's Proof that:
%~ " ?NextWorld inst world " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( nesc(nextWorld(NextWorld,World))&poss(~inst(World,world)) ==>
poss( ~( inst(NextWorld,world)))).
============================================
%~ kif_to_boxlog_attvars2 = necessary(=>(nextWorld('$VAR'('C'),'$VAR'('N')),and(inst('$VAR'('C'),world),inst('$VAR'('N'),world))))
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k fol_calc_01.pfc.pl (returned 137) Add_LABELS='Errors,Overtime' Rem_LABELS='Skipped,Skipped,Warnings,Skipped'
![dependabot[bot] avatar](https://avatars.githubusercontent.com/in/29110?v=4 "dependabot[bot]")
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent