search

logicmoo / logicmoo_workspace

https://jenkins.logicmoo.org/job/logicmoo_workspace https://logicmoo.org/xwiki/
http://www.logicmoo.org/
Other
45 stars 8 forks source link

logicmoo.base.examples.fol.FORALL_QUANT_01 JUnit #613

Open TeamSPoon opened 3 years ago

TeamSPoon commented 3 years ago

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

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

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

:- set_prolog_flag(gc,true).

% =================================================================================
% Set our engine up
% =================================================================================

/*~
~*/

% =================================================================================
% Set our engine up
% =================================================================================

:- expects_dialect(pfc).

% =================================================================================
% Begin program
% =================================================================================

% Let same/2 be our unification identify 
/*~
~*/

% =================================================================================
% Begin program
% =================================================================================

% Let same/2 be our unification identify 
:- test_boxlog(forall(X,same(X,X))).

% same/2 implies not differnt
/*~
%~ ?-( mpred_test("Test_0001_Line_0000__same_2",baseKB:test_boxlog(forall(X,same(X,X))))).
%~ kifi = all(X,same(X,X)).
%~ kifm = all(X,nesc(same(X,X))).
%~ 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)).

%~ kifi = all(X,same(X,X)).
%~ kifm = all(X,nesc(same(X,X))).
passed=info(why_was_true(baseKB:test_boxlog(forall(_452,same(_452,_452)))))
no_proof_for(test_boxlog(forall(X,same(X,X)))).

%~ kifi=all(X,same(X,X))
%~ kifm=all(X,nesc(same(X,X)))
%~ 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)).

no_proof_for(test_boxlog(forall(X,same(X,X)))).

no_proof_for(test_boxlog(forall(X,same(X,X)))).

    name    =   'logicmoo.base.examples.fol.FORALL_QUANT_01-Test_0001_Line_0000__same_2'. 
    JUNIT_CLASSNAME =   'logicmoo.base.examples.fol.FORALL_QUANT_01'. 
    JUNIT_CMD   =   'timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'forall_quant_01.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_FORALL_QUANT_01_Test_0001_Line_0000_same_2-junit.xml
~*/

% same/2 implies not differnt
:- test_boxlog(all(X,all(Y,same(X,Y) => ~ different(X,Y)))).

/*~
%~ ?-( mpred_test( "Test_0002_Line_0000__same_2",
%~       baseKB : test_boxlog( all(X,all(Y,same(X,Y)=>(~different(X,Y))))))).
%~ kifi = all(X,all(Y,same(X,Y)=>(~different(X,Y)))).
%~ kifm = all(X,all(Y,nesc(same(X,Y)=>(~different(X,Y))))).
%~ 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)).

%~ kifi = all(X,all(Y,same(X,Y)=>(~different(X,Y)))).
%~ kifm = all(X,all(Y,nesc(same(X,Y)=>(~different(X,Y))))).
passed=info(why_was_true(baseKB:test_boxlog(all(_518,all(_520,same(_518,_520)=>(~different(_518,_520)))))))
no_proof_for(test_boxlog(all(X,all(Y,same(X,Y)=>(~different(X,Y)))))).

%~ kifi=all(X,all(Y,same(X,Y)=>(~different(X,Y))))
%~ kifm=all(X,all(Y,nesc(same(X,Y)=>(~different(X,Y)))))
%~ 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)).

no_proof_for(test_boxlog(all(X,all(Y,same(X,Y)=>(~different(X,Y)))))).

no_proof_for(test_boxlog(all(X,all(Y,same(X,Y)=>(~different(X,Y)))))).

    name    =   'logicmoo.base.examples.fol.FORALL_QUANT_01-Test_0002_Line_0000__same_2'. 
    JUNIT_CLASSNAME =   'logicmoo.base.examples.fol.FORALL_QUANT_01'. 
    JUNIT_CMD   =   'timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'forall_quant_01.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_FORALL_QUANT_01_Test_0002_Line_0000_same_2-junit.xml
~*/

:- test_boxlog(forall([X,Y], same(X,Y) => ~ different(X,Y))).

/*~
%~ ?-( mpred_test( Kw,
%~       baseKB : test_boxlog( forall( [X,Y],
%~                               same(X,Y)=>(~different(X,Y)))))).
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/forall_quant_01.pfc.pl:28 
%~ correct_special_quantifiers :- all( X,
%~                                  all(Y,same(X,Y)=>(~different(X,Y)))).
%~ %~ correct_special_quantifiers:-all(X,all(Y,same(X,Y)=>(~different(X,Y))))
%~ kifi = all( [X,Y],
%~          same(X,Y)=>(~different(X,Y))).
%~ kifm = all(X,all(Y,nesc(same(X,Y)=>(~different(X,Y))))).
%~ 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)).

%~ correct_special_quantifiers :- all( Same,
%~                                  all( Different_Same6,
%~                                    same(Same,Different_Same6)=>(~different(Same,Different_Same6)))).
%~ kifi = all( [Same,Different_Same6],
%~          same(Same,Different_Same6)=>(~different(Same,Different_Same6))).
%~ kifm = all( Same,
%~          all( Different_Same6,
%~            nesc( same(Same,Different_Same6)=>(~different(Same,Different_Same6))))).
passed=info(why_was_true(baseKB:test_boxlog(forall([_504,_506],same(_504,_506)=>(~different(_504,_506))))))
no_proof_for(test_boxlog(forall([Same,Different_Same6],same(Same,Different_Same6)=>(~different(Same,Different_Same6))))).

%~ %~ correct_special_quantifiers:-all(Same,all(Different_Same6,same(Same,Different_Same6)=>(~different(Same,Different_Same6))))
%~ kifi=all([Same,Different_Same6],same(Same,Different_Same6)=>(~different(Same,Different_Same6)))
%~ kifm=all(Same,all(Different_Same6,nesc(same(Same,Different_Same6)=>(~different(Same,Different_Same6)))))
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Same'),forall('$VAR'('Different_Same6'),necessary(=>(same('$VAR'('Same'),'$VAR'('Different_Same6')),not(different('$VAR'('Same'),'$VAR'('Different_Same6')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Same different ?Different_Same6 " is possible
%~  It's Proof that:
%~    " ?Same same ?Different_Same6 " is possibly false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

poss(different(Same,Different_Same6))==>poss(~same(Same,Different_Same6)).

%  AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~  Whenever:
%~    " ?Same same ?Different_Same6 " is necessarily true
%~  It's Proof that:
%~    " ?Same different ?Different_Same6 " is necessarily false
%~ 
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nesc(same(Same,Different_Same6))==>nesc(~different(Same,Different_Same6)).

no_proof_for(test_boxlog(forall([Same10,Different_Same11],same(Same10,Different_Same11)=>(~different(Same10,Different_Same11))))).

no_proof_for(test_boxlog(forall([Same10,Different_Same11],same(Same10,Different_Same11)=>(~different(Same10,Different_Same11))))).

    name    =   'logicmoo.base.examples.fol.FORALL_QUANT_01-Test_0001_Line_0000__same_2'. 
    JUNIT_CLASSNAME =   'logicmoo.base.examples.fol.FORALL_QUANT_01'. 
    JUNIT_CMD   =   'timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'forall_quant_01.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_FORALL_QUANT_01_Test_0001_Line_0000_same_2_0-junit.xml
~*/
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/forall_quant_01.pfc.pl:30 
%~ unused(no_junit_results)
Test_0001_Line_0000__same_2 result  =   passed. 
Test_0002_Line_0000__same_2 result  =   passed. 

%~ test_completed_exit(64)

totalTime=1.000

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

TeamSPoon commented 3 years ago

Fixed in https://github.com/logicmoo/logicmoo_workspace/commit/005b698b856a92b51f18328ba02a312f4328960d https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/commit/005b698b856a92b51f18328ba02a312f4328960d

TeamSPoon commented 3 years ago

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

TeamSPoon commented 3 years ago

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

TeamSPoon commented 3 years ago

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

TeamSPoon commented 3 years ago

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