logicmoo_workspace icon indicating copy to clipboard operation
logicmoo_workspace copied to clipboard

Published 20 hours ago • verified publisher icon logicmoo

logicmoo.base.examples.fol.POSS_FORALL_EXISTS_05 JUnit

Open TeamSPoon opened this issue 4 years ago • 4 comments
trafficstars

(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 "['poss_forall_exists_05.pfc.pl']")

% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/poss_forall_exists_05.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/POSS_FORALL_EXISTS_05/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3APOSS_FORALL_EXISTS_05 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/441

%~ 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/poss_forall_exists_05.pfc.pl'),
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))


% =================================================================================
% 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).
%:- set_prolog_flag_until_eof(runtime_speed,0). % but dont gripe about speed
/*~
~*/

%:- set_prolog_flag_until_eof(runtime_speed,0). % but dont gripe about speed
:- kif_compile.

% =================================================================================
% temp test
% =================================================================================

/*~
~*/


% =================================================================================
% temp test
% =================================================================================

ff1:- show_kif_to_boxlog(if(nesc(livesAt(X, green_house)),nesc(drinks(X, coffee)))).
/*~
~*/

ff2:- show_kif_to_boxlog(if((livesAt(X, green_house)),(drinks(X, coffee)))).

/*~
~*/


ff3:- show_kif_to_boxlog(nesc(drinks(_X, coffee))).
/*~
~*/

ff4:- show_kif_to_boxlog(~nesc(drinks(_X, coffee))).
/*~
~*/

ff5:- show_kif_to_boxlog(~poss(drinks(_X, coffee))).
/*~
~*/

ff6:- show_kif_to_boxlog(poss(drinks(_X, coffee))).


/*~
~*/



:- show_kif_to_boxlog(all(X, if(nesc(livesAt(X, green_house)),poss(livesAt(X, green_house))))).

/*~
%~ test_boxlog( all(X,if(nesc(livesAt(X,green_house)),poss(livesAt(X,green_house)))))
~*/


:- show_kif_to_boxlog(all(X, if(poss(livesAt(X, green_house)),nesc(livesAt(X, green_house))))).

/*~
%~ test_boxlog( all(X,if(poss(livesAt(X,green_house)),nesc(livesAt(X,green_house)))))
~*/


:- break.

% =================================================================================
% Note these two assertions are implicit to the system and have no side effect 
% (they are here to serve as a reminder)
% =================================================================================

% for any objects in the universe that live in the green house must obvously have that as a possibility
/*~
%~ skipped(blocks_on_input,break)
~*/


% =================================================================================
% Note these two assertions are implicit to the system and have no side effect 
% (they are here to serve as a reminder)
% =================================================================================

% for any objects in the universe that live in the green house must obvously have that as a possibility
all(X, if(livesAt(X, green_house),poss(livesAt(X, green_house)))).

% all objects in the universe that do drink coffee, may drink coffee
/*~
%~ kifi = all(_24304,if(livesAt(_24304,green_house),poss(livesAt(_24304,green_house)))).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/poss_forall_exists_05.pfc.pl:43 
%~ kifm = all( If_Green_house,
%~          livesAt(If_Green_house,green_house)=>poss(livesAt(If_Green_house,green_house))).
%~ kifm = all( Green_house4,
%~          livesAt(Green_house4,green_house)=>poss(livesAt(Green_house4,green_house))).
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Green_house4'),=>(livesAt('$VAR'('Green_house4'),green_house),possible(livesAt('$VAR'('Green_house4'),green_house))))
%~ debugm( baseKB,
%~   show_success( baseKB,
%~     baseKB : ain( clif( all(X,if(livesAt(X,green_house),poss(livesAt(X,green_house))))))))
%   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: 211 words .. **



** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/lex.xg: -221 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.63 sec, 3 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.14 sec, -16 clauses




=======================================================
all('$VAR'('If_Green_house'),if(livesAt('$VAR'('If_Green_house'),green_house),poss(livesAt('$VAR'('If_Green_house'),green_house))))
============================================


?- kif_to_boxlog( all(If_Green_house,if(livesAt(If_Green_house,green_house),poss(livesAt(If_Green_house,green_house)))) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ 
%~  For all ?If_Green_house
%~    ?If_Green_house livesAt green_house if " ?If_Green_house livesAt green_house " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('If_Green_house'),=>(livesAt('$VAR'('If_Green_house'),green_house),possible(livesAt('$VAR'('If_Green_house'),green_house))))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s): 
nesc(~livesAt(If_Green_house,green_house))==>nesc(~livesAt(If_Green_house,green_house)).
nesc(livesAt(If_Green_house,green_house))==>poss(livesAt(If_Green_house,green_house)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?If_Green_house livesAt green_house " is necessarily false
%~  It's Proof that:
%~    " ?If_Green_house livesAt green_house " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~livesAt(If_Green_house,green_house))==>nesc(~livesAt(If_Green_house,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?If_Green_house livesAt green_house " is necessarily true
%~  It's Proof that:
%~    " ?If_Green_house livesAt green_house " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(livesAt(If_Green_house,green_house))==>poss(livesAt(If_Green_house,green_house)).

============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),=>(livesAt('$VAR'('X'),green_house),possible(livesAt('$VAR'('X'),green_house))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X livesAt green_house " is necessarily false
%~  It's Proof that:
%~    " ?X livesAt green_house " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~livesAt(X,green_house))==>nesc(~livesAt(X,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X livesAt green_house " is necessarily true
%~  It's Proof that:
%~    " ?X livesAt green_house " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(livesAt(X,green_house))==>poss(livesAt(X,green_house)).

~*/


% all objects in the universe that do drink coffee, may drink coffee
if(nesc(drinks(X, coffee)),poss(drinks(X, coffee))).


% =================================================================================
% Define a couple predicates
% =================================================================================

% maximum cardinality of livesAt/2 is 1
/*~
%~ kif_to_boxlog_attvars2 = =>(necessary(drinks('$VAR'('Coffee3'),coffee)),possible(drinks('$VAR'('Coffee3'),coffee)))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(if(nesc(drinks(_484,coffee)),poss(drinks(_484,coffee)))))))




=======================================================
if(nesc(drinks('$VAR'('Coffee'),coffee)),poss(drinks('$VAR'('Coffee'),coffee)))
============================================


?- kif_to_boxlog( if(nesc(drinks(Coffee,coffee)),poss(drinks(Coffee,coffee))) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  " ?Coffee drinks coffee " is necessarily true if " ?Coffee drinks coffee " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = =>(necessary(drinks('$VAR'('Coffee'),coffee)),possible(drinks('$VAR'('Coffee'),coffee)))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s): 
nesc(~drinks(Coffee,coffee))==>poss(~drinks(Coffee,coffee)).
nesc(drinks(Coffee,coffee))==>poss(drinks(Coffee,coffee)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Coffee drinks coffee " is necessarily false
%~  It's Proof that:
%~    " ?Coffee drinks coffee " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~drinks(Coffee,coffee))==>poss(~drinks(Coffee,coffee)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Coffee drinks coffee " is necessarily true
%~  It's Proof that:
%~    " ?Coffee drinks coffee " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(drinks(Coffee,coffee))==>poss(drinks(Coffee,coffee)).

============================================
%~ kif_to_boxlog_attvars2 = =>(necessary(drinks('$VAR'('X'),coffee)),possible(drinks('$VAR'('X'),coffee)))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X drinks coffee " is necessarily false
%~  It's Proof that:
%~    " ?X drinks coffee " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~drinks(X,coffee))==>poss(~drinks(X,coffee)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X drinks coffee " is necessarily true
%~  It's Proof that:
%~    " ?X drinks coffee " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(drinks(X,coffee))==>poss(drinks(X,coffee)).

~*/



% =================================================================================
% Define a couple predicates
% =================================================================================

% maximum cardinality of livesAt/2 is 1
instance(livesAt,'FunctionalBinaryPredicate').
% thus implies
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/poss_forall_exists_05.pfc.pl:54 
%~ azzert_rename('FunctionalBinaryPredicate',rtFunctionalBinaryPredicate)
%~ kif_to_boxlog_attvars2 = necessary(rtFunctionalBinaryPredicate(livesAt))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(instance(livesAt,rtFunctionalBinaryPredicate)))))




=======================================================
instance(livesAt,rtFunctionalBinaryPredicate)
============================================


?- kif_to_boxlog( instance(livesAt,rtFunctionalBinaryPredicate) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  livesAt instance rtFunctionalBinaryPredicate
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(rtFunctionalBinaryPredicate(livesAt))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s): 
nesc(rtFunctionalBinaryPredicate(livesAt)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  it is necessarily true that livesAt isa rtFunctionalBinaryPredicate
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc( rtFunctionalBinaryPredicate(livesAt)).

============================================
~*/

% thus implies
==> arity(livesAt,2).
/*~
~*/

==> domain(livesAt,1,human).
/*~
~*/

==> domain(livesAt,2,dwelling).

% define drinks/2
/*~
~*/


% define drinks/2
==> arity(drinks,2).
/*~
~*/

domain(drinks,1,human).
/*~
%~ kif_to_boxlog_attvars2 = necessary(argIsa(drinks,1,human))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(domain(drinks,1,human)))))




=======================================================
domain(drinks,1,human)
============================================


?- kif_to_boxlog( domain(drinks,1,human) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  domain(drinks,1,human)
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(drinks,1,human))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s): 
nesc(argIsa(drinks,1,human)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  it is necessarily true that argIsa(drinks,1,human)
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc( argIsa(drinks,1,human)).

============================================
~*/

domain(drinks,2,beverage_class).

% =================================================================================
% Note these two assertions are implicit to the system and have no side effect 
% (they are here to serve as a reminder)
% =================================================================================

% all objects in the universe that do drink coffee, may drink coffee
/*~
%~ kif_to_boxlog_attvars2 = necessary(argIsa(drinks,2,beverage_class))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(domain(drinks,2,beverage_class)))))




=======================================================
domain(drinks,2,beverage_class)
============================================


?- kif_to_boxlog( domain(drinks,2,beverage_class) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  domain(drinks,2,beverage_class)
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = necessary(argIsa(drinks,2,beverage_class))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s): 
nesc(argIsa(drinks,2,beverage_class)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  it is necessarily true that argIsa(drinks,2,beverage_class)
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc( argIsa(drinks,2,beverage_class)).

============================================
~*/


% =================================================================================
% Note these two assertions are implicit to the system and have no side effect 
% (they are here to serve as a reminder)
% =================================================================================

% all objects in the universe that do drink coffee, may drink coffee
all(X, if(drinks(X, coffee),possible(drinks(X, coffee)))).

% for any objects in the universe that live in the green house must obvously have that as a possibility
/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Coffee4'),=>(drinks('$VAR'('Coffee4'),coffee),possible(drinks('$VAR'('Coffee4'),coffee))))
%~ debugm( baseKB,
%~   show_success( baseKB,
%~     baseKB : ain( clif( all(X,if(drinks(X,coffee),possible(drinks(X,coffee))))))))




=======================================================
all('$VAR'('If_Coffee'),if(drinks('$VAR'('If_Coffee'),coffee),possible(drinks('$VAR'('If_Coffee'),coffee))))
============================================


?- kif_to_boxlog( all(If_Coffee,if(drinks(If_Coffee,coffee),possible(drinks(If_Coffee,coffee)))) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ 
%~  For all ?If_Coffee
%~    " ?If_Coffee drinks coffee if ?If_Coffee drinks coffee isa possible "
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('If_Coffee'),=>(drinks('$VAR'('If_Coffee'),coffee),possible(drinks('$VAR'('If_Coffee'),coffee))))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s): 
nesc(~drinks(If_Coffee,coffee))==>nesc(~drinks(If_Coffee,coffee)).
nesc(drinks(If_Coffee,coffee))==>poss(drinks(If_Coffee,coffee)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?If_Coffee drinks coffee " is necessarily false
%~  It's Proof that:
%~    " ?If_Coffee drinks coffee " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~drinks(If_Coffee,coffee))==>nesc(~drinks(If_Coffee,coffee)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?If_Coffee drinks coffee " is necessarily true
%~  It's Proof that:
%~    " ?If_Coffee drinks coffee " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(drinks(If_Coffee,coffee))==>poss(drinks(If_Coffee,coffee)).

============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),=>(drinks('$VAR'('X'),coffee),possible(drinks('$VAR'('X'),coffee))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X drinks coffee " is necessarily false
%~  It's Proof that:
%~    " ?X drinks coffee " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~drinks(X,coffee))==>nesc(~drinks(X,coffee)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X drinks coffee " is necessarily true
%~  It's Proof that:
%~    " ?X drinks coffee " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(drinks(X,coffee))==>poss(drinks(X,coffee)).

~*/


% for any objects in the universe that live in the green house must obvously have that as a possibility
all(X, if(livesAt(X, green_house),possible(livesAt(X, green_house)))).

% =================================================================================
% But given the above: 
%
%   Only things that possibly can drink coffee live in the green house?
%
% =================================================================================
/*~
%~ debugm( baseKB,
%~   show_success( baseKB,
%~     baseKB : ain( clif( all(X,if(livesAt(X,green_house),possible(livesAt(X,green_house))))))))




=======================================================
all('$VAR'('If_Green_house'),if(livesAt('$VAR'('If_Green_house'),green_house),possible(livesAt('$VAR'('If_Green_house'),green_house))))
============================================


?- kif_to_boxlog( all(If_Green_house,if(livesAt(If_Green_house,green_house),possible(livesAt(If_Green_house,green_house)))) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ 
%~  For all ?If_Green_house
%~    " ?If_Green_house livesAt green_house if ?If_Green_house livesAt green_house isa possible "
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('If_Green_house'),=>(livesAt('$VAR'('If_Green_house'),green_house),possible(livesAt('$VAR'('If_Green_house'),green_house))))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s): 
nesc(~livesAt(If_Green_house,green_house))==>nesc(~livesAt(If_Green_house,green_house)).
nesc(livesAt(If_Green_house,green_house))==>poss(livesAt(If_Green_house,green_house)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?If_Green_house livesAt green_house " is necessarily false
%~  It's Proof that:
%~    " ?If_Green_house livesAt green_house " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~livesAt(If_Green_house,green_house))==>nesc(~livesAt(If_Green_house,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?If_Green_house livesAt green_house " is necessarily true
%~  It's Proof that:
%~    " ?If_Green_house livesAt green_house " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(livesAt(If_Green_house,green_house))==>poss(livesAt(If_Green_house,green_house)).

============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),=>(livesAt('$VAR'('X'),green_house),possible(livesAt('$VAR'('X'),green_house))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X livesAt green_house " is necessarily false
%~  It's Proof that:
%~    " ?X livesAt green_house " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(~livesAt(X,green_house))==>nesc(~livesAt(X,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X livesAt green_house " is necessarily true
%~  It's Proof that:
%~    " ?X livesAt green_house " is possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(livesAt(X,green_house))==>poss(livesAt(X,green_house)).

~*/


% =================================================================================
% But given the above: 
%
%   Only things that possibly can drink coffee live in the green house?
%
% =================================================================================
all(X, livesAt(X, green_house) & drinks(X, coffee)).

/*~
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Nesc_Coffee_Green_house4'),necessary(and(livesAt('$VAR'('Nesc_Coffee_Green_house4'),green_house),drinks('$VAR'('Nesc_Coffee_Green_house4'),coffee))))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(all(_480,livesAt(_480,green_house)&drinks(_480,coffee))))))




=======================================================
all('$VAR'('Coffee_Green_house'),&(livesAt('$VAR'('Coffee_Green_house'),green_house),drinks('$VAR'('Coffee_Green_house'),coffee)))
============================================


?- kif_to_boxlog( all(Coffee_Green_house,livesAt(Coffee_Green_house,green_house)&drinks(Coffee_Green_house,coffee)) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ 
%~  For all ?Coffee_Green_house
%~    (" ?Coffee_Green_house livesAt green_house "  and
%~    " ?Coffee_Green_house drinks coffee " )
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Coffee_Green_house'),necessary(and(livesAt('$VAR'('Coffee_Green_house'),green_house),drinks('$VAR'('Coffee_Green_house'),coffee))))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 4 entailment(s): 
nesc(drinks(Coffee_Green_house,coffee))==>nesc(livesAt(Coffee_Green_house,green_house)).
nesc(livesAt(Coffee_Green_house,green_house))==>nesc(drinks(Coffee_Green_house,coffee)).
poss(~drinks(Coffee_Green_house,coffee))==>poss(~livesAt(Coffee_Green_house,green_house)).
poss(~livesAt(Coffee_Green_house,green_house))==>poss(~drinks(Coffee_Green_house,coffee)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Coffee_Green_house drinks coffee " is necessarily true
%~  It's Proof that:
%~    " ?Coffee_Green_house livesAt green_house " is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(drinks(Coffee_Green_house,coffee))==>nesc(livesAt(Coffee_Green_house,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Coffee_Green_house livesAt green_house " is necessarily true
%~  It's Proof that:
%~    " ?Coffee_Green_house drinks coffee " is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(livesAt(Coffee_Green_house,green_house))==>nesc(drinks(Coffee_Green_house,coffee)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Coffee_Green_house drinks coffee " is possibly false
%~  It's Proof that:
%~    " ?Coffee_Green_house livesAt green_house " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(~drinks(Coffee_Green_house,coffee))==>poss(~livesAt(Coffee_Green_house,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Coffee_Green_house livesAt green_house " is possibly false
%~  It's Proof that:
%~    " ?Coffee_Green_house drinks coffee " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(~livesAt(Coffee_Green_house,green_house))==>poss(~drinks(Coffee_Green_house,coffee)).

============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('X'),necessary(and(livesAt('$VAR'('X'),green_house),drinks('$VAR'('X'),coffee))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X livesAt green_house " is possibly false
%~  It's Proof that:
%~    " ?X drinks coffee " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(~livesAt(X,green_house))==>poss(~drinks(X,coffee)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X drinks coffee " is necessarily true
%~  It's Proof that:
%~    " ?X livesAt green_house " is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(drinks(X,coffee))==>nesc(livesAt(X,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X drinks coffee " is possibly false
%~  It's Proof that:
%~    " ?X livesAt green_house " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(~drinks(X,coffee))==>poss(~livesAt(X,green_house)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?X livesAt green_house " is necessarily true
%~  It's Proof that:
%~    " ?X drinks coffee " is necessarily true
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(livesAt(X,green_house))==>nesc(drinks(X,coffee)).

~*/


~poss(livesAt(fred,green_house)).

% Does fred drink coffee? (should be unknown)
/*~
~*/


% Does fred drink coffee? (should be unknown)
:- \+ drinks(fred,coffee).

/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/poss_forall_exists_05.pfc.pl:87 
%~ ?-( mpred_test("Test_0001_Line_0000__naf_Fred",baseKB:(\+drinks(fred,coffee)))).
%~ make_dynamic_here(baseKB,drinks(fred,coffee))
passed=info(why_was_true(baseKB:(\+drinks(fred,coffee))))
no_proof_for(\+drinks(fred,coffee)).

no_proof_for(\+drinks(fred,coffee)).

no_proof_for(\+drinks(fred,coffee)).

	name	=	'logicmoo.base.examples.fol.POSS_FORALL_EXISTS_05-Test_0001_Line_0000__naf_Fred'. 
	JUNIT_CLASSNAME	=	'logicmoo.base.examples.fol.POSS_FORALL_EXISTS_05'. 
	JUNIT_CMD	=	'timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'poss_forall_exists_05.pfc.pl\']"'. 
% saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace@2/test_results/jenkins/Report-logicmoo-base-examples-fol-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_examples_fol_POSS_FORALL_EXISTS_05_Test_0001_Line_0000_naf_Fred-junit.xml
~*/


possible(livesAt(joe,green_house)).
/*~
%~ kif_to_boxlog_attvars2 = possible(livesAt(joe,green_house))
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(possible(livesAt(joe,green_house))))))




=======================================================
possible(livesAt(joe,green_house))
============================================


?- kif_to_boxlog( possible(livesAt(joe,green_house)) ).



% In English: 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  joe livesAt green_house isa possible
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = possible(livesAt(joe,green_house))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s): 
poss(livesAt(joe,green_house)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  it is possible that joe livesAt green_house
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss( livesAt(joe,green_house)).

============================================
~*/

:- drinks(joe,coffee).


% =================================================================================
% These two assertions are a bit weird but are for fun
% =================================================================================

% all objects in the universe that may drink coffee do drink coffee
%all(X, if(possible(drinks(X, coffee)),drinks(X, coffee))).

% all objects in the universe that may live in the green house do live in the green house
%all(X, if(possible(livesAt(X, green_house)),lives(X, green_house) )).



% ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/441 
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/poss_forall_exists_05.pfc.pl 
% JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/POSS_FORALL_EXISTS_05/ 
% ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3APOSS_FORALL_EXISTS_05 

/*~
%~ message_hook_type(warning)
%~ message_hook(
%~    goal_failed(directive,baseKB:drinks(joe,coffee)),
%~    warning,
%~    [ 'Goal (~w) failed: ~p' - [ directive,
%~                                 baseKB : drinks(joe,coffee)]])
Goal (directive) failed: baseKB:drinks(joe,coffee)
Warning: Goal (directive) failed: baseKB:drinks(joe,coffee)
~*/
%~ unused(no_junit_results)
Test_0001_Line_0000__naf_Fred	result	=	passed. 
logicmoo.base.examples.fol.POSS_FORALL_EXISTS_05 JUnit	warning	=	Goal (directive) failed: baseKB:drinks(joe,coffee) 

%~ test_completed_exit(80)

totalTime=6.000

SUCCESS: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k poss_forall_exists_05.pfc.pl (returned 80) Add_LABELS='Warnings' Rem_LABELS='Skipped,Skipped,Errors,Overtime,Skipped,Skipped'

TeamSPoon avatar Sep 18 '21 22:09 TeamSPoon

Broken in https://github.com/logicmoo/logicmoo_workspace/commit/47cfb56e12234430e980d22dbcca206411201b38 https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/commit/47cfb56e12234430e980d22dbcca206411201b38

TeamSPoon avatar Sep 20 '21 20:09 TeamSPoon

Fixed in https://github.com/logicmoo/logicmoo_workspace/commit/51a38b8a8cc92a39cbea53faf8883a32e6dc3b61 https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/commit/51a38b8a8cc92a39cbea53faf8883a32e6dc3b61

TeamSPoon avatar Sep 21 '21 00:09 TeamSPoon

Broken in https://github.com/logicmoo/logicmoo_workspace/commit/157f663e9aafee41e1bef5aa3e17fd16962ab8c7 https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/commit/157f663e9aafee41e1bef5aa3e17fd16962ab8c7

TeamSPoon avatar Sep 21 '21 19:09 TeamSPoon

Fixed in https://github.com/logicmoo/logicmoo_workspace/commit/90f5d1e5fc22fb1b2f7fdc46074babc473034f36 https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/commit/90f5d1e5fc22fb1b2f7fdc46074babc473034f36

TeamSPoon avatar Sep 23 '21 19:09 TeamSPoon