house(H1) & house(H2). /*~ %~ debugm(user,show_success(user,user:ain(clif((leftof(_829876,_829898)=>house(_829876)&house(_829898)))))) ======================================================= =>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof3')),&(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof3')))) ============================================ ?- kif_to_boxlog( leftof(House_Leftof,House_Leftof3)=>house(House_Leftof)&house(House_Leftof3) ). % In English: %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ If: %~ ?House_Leftof leftof ?House_Leftof3 then it is %~ Implied that: %~ " ?House_Leftof isa house " and %~ " ?House_Leftof3 isa house " %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ kifm = ( leftof(House_Leftof,House_Leftof3) => %~ house(House_Leftof)&house(House_Leftof3)). %~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof3')),and(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof3')))) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results in the following 6 entailment(s): nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof))==>nesc(~house(House_Leftof3)). nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof3))==>nesc(~house(House_Leftof)). nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof))==>nesc(house(House_Leftof3)). nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof3))==>nesc(house(House_Leftof)). poss(house(House_Leftof))&nesc(~house(House_Leftof3))==>nesc(~leftof(House_Leftof,House_Leftof3)). poss(house(House_Leftof3))&nesc(~house(House_Leftof))==>nesc(~leftof(House_Leftof,House_Leftof3)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and %~ " ?House_Leftof isa house " is necessarily false %~ It's Proof that: %~ " ?House_Leftof3 isa house " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof)) ==> nesc( ~( house(House_Leftof3)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and %~ " ?House_Leftof3 isa house " is necessarily false %~ It's Proof that: %~ " ?House_Leftof isa house " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( nesc(leftof(House_Leftof,House_Leftof3))&nesc(~house(House_Leftof3)) ==> nesc( ~( house(House_Leftof)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and %~ " ?House_Leftof isa house " is possible %~ It's Proof that: %~ " ?House_Leftof3 isa house " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof)) ==> nesc( house(House_Leftof3))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily true and %~ " ?House_Leftof3 isa house " is possible %~ It's Proof that: %~ " ?House_Leftof isa house " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( nesc(leftof(House_Leftof,House_Leftof3))&poss(house(House_Leftof3)) ==> nesc( house(House_Leftof))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?House_Leftof isa house " is possible and %~ " ?House_Leftof3 isa house " is necessarily false %~ It's Proof that: %~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( poss(house(House_Leftof))&nesc(~house(House_Leftof3)) ==> nesc( ~( leftof(House_Leftof,House_Leftof3)))). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?House_Leftof3 isa house " is possible and %~ " ?House_Leftof isa house " is necessarily false %~ It's Proof that: %~ " ?House_Leftof leftof ?House_Leftof3 " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ( poss(house(House_Leftof3))&nesc(~house(House_Leftof)) ==> nesc( ~( leftof(House_Leftof,House_Leftof3)))). ============================================ %~ kifm = leftof(H1,H2)=>house(H1)&house(H2). %~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('H1'),'$VAR'('H2')),and(house('$VAR'('H1')),house('$VAR'('H2')))) %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?H2 isa house " is possible and %~ " ?H1 isa house " is necessarily false %~ It's Proof that: %~ " ?H1 leftof ?H2 " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% poss(house(H2))&nesc(~house(H1))==>nesc(~leftof(H1,H2)). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?H1 leftof ?H2 " is necessarily true and %~ " ?H1 isa house " is necessarily false %~ It's Proof that: %~ " ?H2 isa house " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nesc(leftof(H1,H2))&nesc(~house(H1))==>nesc(~house(H2)). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?H1 leftof ?H2 " is necessarily true and %~ " ?H2 isa house " is possible %~ It's Proof that: %~ " ?H1 isa house " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nesc(leftof(H1,H2))&poss(house(H2))==>nesc(house(H1)). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?H1 isa house " is possible and %~ " ?H2 isa house " is necessarily false %~ It's Proof that: %~ " ?H1 leftof ?H2 " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% poss(house(H1))&nesc(~house(H2))==>nesc(~leftof(H1,H2)). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?H1 leftof ?H2 " is necessarily true and %~ " ?H2 isa house " is necessarily false %~ It's Proof that: %~ " ?H1 isa house " is necessarily false %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nesc(leftof(H1,H2))&nesc(~house(H2))==>nesc(~house(H1)). % AND %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ Whenever: %~ " ?H1 leftof ?H2 " is necessarily true and %~ " ?H1 isa house " is possible %~ It's Proof that: %~ " ?H2 isa house " is necessarily true %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nesc(leftof(H1,H2))&poss(house(H1))==>nesc(house(H2)). ~*/ :- kif_compile. % intractive_test/1 means only run if interactive /*~ %~ kifi = leftof(h1,h2). %~ kifm = nesc( leftof(h1,h2)). %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_02.pl:28 %~ kifi = leftof(h2,h3). %~ kifm = nesc( leftof(h2,h3)). %~ kifi = leftof(h3,h4). %~ kifm = nesc( leftof(h3,h4)). %~ kifi = leftof(h4,h5). %~ kifm = nesc( leftof(h4,h5)). %~ kifm = ( leftof(House_Leftof,House_Leftof1) => %~ house(House_Leftof)&house(House_Leftof1)). %~ kifm = nesc( leftof(h1,h2)). %~ kif_to_boxlog_attvars2 = necessary(leftof(h1,h2)) %~ kifm = nesc( leftof(h2,h3)). %~ kif_to_boxlog_attvars2 = necessary(leftof(h2,h3)) %~ kifm = nesc( leftof(h3,h4)). %~ kif_to_boxlog_attvars2 = necessary(leftof(h3,h4)) %~ kifm = nesc( leftof(h4,h5)). %~ kif_to_boxlog_attvars2 = necessary(leftof(h4,h5)) %~ kifm = ( leftof(House_Leftof,House_Leftof1) => %~ house(House_Leftof)&house(House_Leftof1)). %~ kif_to_boxlog_attvars2 = =>(leftof('$VAR'('House_Leftof'),'$VAR'('House_Leftof1')),and(house('$VAR'('House_Leftof')),house('$VAR'('House_Leftof1')))) ~*/ % intractive_test/1 means only run if interactive :- interactive_test(listing(pfclog)). % mpred_test/1 each become a Junit test that must succeed /*~ %~ message_hook( %~ error(existence_error(procedure,interactive_test/1),context(system:catch/3,Context_Kw)), %~ error, %~ [ '~q/~w: '-[catch,3], %~ 'Unknown procedure: ~q' - [ interactive_test/1]]) catch/3: Unknown procedure: interactive_test/1 ERROR: catch/3: Unknown procedure: interactive_test/1 %~ message_hook( %~ goal_failed(directive,user:interactive_test(listing(pfclog))), %~ warning, %~ [ 'Goal (~w) failed: ~p' - [ directive, %~ user : interactive_test( listing(pfclog))]]) Goal (directive) failed: user:interactive_test(listing(pfclog)) Warning: Goal (directive) failed: user:interactive_test(listing(pfclog)) ~*/ % mpred_test/1 each become a Junit test that must succeed :- mpred_test(pfclog_compile). /*~ %~ ?-( mpred_test("Test_0001_Line_0000__Pfclog_compile_in_user",user:pfclog_compile)). passed=info(why_was_true(user:pfclog_compile)) no_proof_for(pfclog_compile). no_proof_for(pfclog_compile). no_proof_for(pfclog_compile). name='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02-Test_0001_Line_0000__Pfclog_compile_in_user'. JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_02.pl\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-fol-fiveof-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_fol_fiveof_FIVE_LEFTOF_TYPE_02_Test_0001_Line_0000_Pfclog_compile_in_user-junit.xml ~*/ :- mpred_test(pfclog_uncompile). % This is the real test we care about here /*~ %~ ?-( mpred_test("Test_0002_Line_0000__Pfclog_uncompile_in_user",user:pfclog_uncompile)). %~ debugm( baseKB, %~ show_success( baseKB, %~ baseKB : mpred_withdraw( compiled_pfclog, %~ ( mfl4(User,user,'* https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/edit/master/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_02.pl ',36) , %~ ax)))) :- dynamic pfclog/1. :- multifile pfclog/1. :- public pfclog/1. :- module_transparent pfclog/1. pfclog(nesc(leftof(h1, h2))). pfclog(nesc(leftof(h2, h3))). pfclog(nesc(leftof(h3, h4))). pfclog(nesc(leftof(h4, h5))). pfclog((poss(house(A)), nesc(~house(B))==>nesc(~leftof(B, A)))). pfclog((nesc(leftof(A, B)), nesc(~house(A))==>nesc(~house(B)))). pfclog((nesc(leftof(A, B)), poss(house(B))==>nesc(house(A)))). pfclog((poss(house(A)), nesc(~house(B))==>nesc(~leftof(A, B)))). pfclog((nesc(leftof(A, B)), nesc(~house(B))==>nesc(~house(A)))). pfclog((nesc(leftof(A, B)), poss(house(A))==>nesc(house(B)))). %~ debugm( baseKB, %~ show_success( baseKB, %~ baseKB : mpred_withdraw( compiled_pfclog, %~ ( mfl4(User,user,'* https://logicmoo.org:2082/gitlab/logicmoo/logicmoo_workspace/-/edit/master/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_02.pl ',36) , %~ ax)))) passed=info(why_was_true(user:pfclog_uncompile)) no_proof_for(pfclog_uncompile). :- dynamic pfclog/1. :- multifile pfclog/1. :- public pfclog/1. :- module_transparent pfclog/1. pfclog(nesc(leftof(h1, h2))). pfclog(nesc(leftof(h2, h3))). pfclog(nesc(leftof(h3, h4))). pfclog(nesc(leftof(h4, h5))). pfclog((poss(house(A)), nesc(~house(B))==>nesc(~leftof(B, A)))). pfclog((nesc(leftof(A, B)), nesc(~house(A))==>nesc(~house(B)))). pfclog((nesc(leftof(A, B)), poss(house(B))==>nesc(house(A)))). pfclog((poss(house(A)), nesc(~house(B))==>nesc(~leftof(A, B)))). pfclog((nesc(leftof(A, B)), nesc(~house(B))==>nesc(~house(A)))). pfclog((nesc(leftof(A, B)), poss(house(A))==>nesc(house(B)))). no_proof_for(pfclog_uncompile). no_proof_for(pfclog_uncompile). name='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02-Test_0002_Line_0000__Pfclog_uncompile_in_user'. JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_02.pl\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-fol-fiveof-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_fol_fiveof_FIVE_LEFTOF_TYPE_02_Test_0002_Line_0000_Pfclog_uncompile_in_user-junit.xml ~*/ % This is the real test we care about here :- interactive_test(pfclog_recompile). /*~ %~ /var/lib/jenkins/workspace/logicmoo_workspace/packs_sys/logicmoo_base/t/examples/fol/fiveof/five_leftof_type_02.pl:38 %~ message_hook( %~ error(existence_error(procedure,interactive_test/1),context(system:catch/3,Context_Kw)), %~ error, %~ [ '~q/~w: '-[catch,3], %~ 'Unknown procedure: ~q' - [ interactive_test/1]]) catch/3: Unknown procedure: interactive_test/1 ERROR: catch/3: Unknown procedure: interactive_test/1 %~ message_hook( %~ goal_failed(directive,user:interactive_test(pfclog_recompile)), %~ warning, %~ [ 'Goal (~w) failed: ~p' - [ directive, %~ user : interactive_test(pfclog_recompile)]]) Goal (directive) failed: user:interactive_test(pfclog_recompile) Warning: Goal (directive) failed: user:interactive_test(pfclog_recompile) ~*/ :- interactive_test(listing(nesc)). % ensure our rule worked /*~ %~ message_hook( %~ error(existence_error(procedure,interactive_test/1),context(system:catch/3,Context_Kw)), %~ error, %~ [ '~q/~w: '-[catch,3], %~ 'Unknown procedure: ~q' - [ interactive_test/1]]) catch/3: Unknown procedure: interactive_test/1 ERROR: catch/3: Unknown procedure: interactive_test/1 %~ message_hook( %~ goal_failed(directive,user:interactive_test(listing(nesc))), %~ warning, %~ [ 'Goal (~w) failed: ~p' - [ directive, %~ user : interactive_test( listing(nesc))]]) Goal (directive) failed: user:interactive_test(listing(nesc)) Warning: Goal (directive) failed: user:interactive_test(listing(nesc)) ~*/ % ensure our rule worked :- mpred_test(nesc(house(h1))). % ensure we are being nice /*~ %~ ?-( mpred_test("Test_0003_Line_0000__H1_in_user",user:nesc(house(h1)))). failure=info((why_was_true(user:(\+nesc(house(h1)))),nop(ftrace(user:nesc(house(h1)))))) no_proof_for(\+nesc(house(h1))). no_proof_for(\+nesc(house(h1))). no_proof_for(\+nesc(house(h1))). name='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02-Test_0003_Line_0000__H1_in_user'. JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_02.pl\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-fol-fiveof-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_fol_fiveof_FIVE_LEFTOF_TYPE_02_Test_0003_Line_0000_H1_in_user-junit.xml ~*/ % ensure we are being nice :- mpred_test(poss(house(false_positive))). % but not "too" nice /*~ %~ ?-( mpred_test("Test_0004_Line_0000__False_positive_in_user",user:poss(house(false_positive)))). passed=info(why_was_true(user:poss(house(false_positive)))) no_proof_for(poss(house(false_positive))). no_proof_for(poss(house(false_positive))). no_proof_for(poss(house(false_positive))). name='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02-Test_0004_Line_0000__False_positive_in_user'. JUNIT_CLASSNAME='logicmoo.base.fol.fiveof.FIVE_LEFTOF_TYPE_02'. JUNIT_CMD='timeout --foreground --preserve-status -s SIGKILL -k 10s 10s swipl -x /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-clif -t "[\'five_leftof_type_02.pl\']"'. % saving_junit: /var/lib/jenkins/workspace/logicmoo_workspace/test_results/jenkins/Report-logicmoo-base-fol-fiveof-vSTARv0vSTARvvDOTvvSTARv-2-1--grep-2-i-WARN-ERROR-_file-00-fail-pass--Units-Logicmoo_base_fol_fiveof_FIVE_LEFTOF_TYPE_02_Test_0004_Line_0000_False_positive_in_user-junit.xml ~*/ % but not "too" nice :- mpred_test(\+ nesc(house(false_positive))). % lets invalidate a goal=user:(\+nesc(house(false_positive))). time=0.0011267662048339844. passed=passed=info(why_was_true(user:(\+nesc(house(false_positive))))) no_proof_for(\+nesc(house(false_positive))). no_proof_for(\+nesc(house(false_positive))). no_proof_for(\+nesc(house(false_positive))). result=passed. ]]>