house(H1) & house(H2). /*~ %~ debugm( baseKB, %~ show_success( baseKB, %~ baseKB : ain( clif( leftof(H1,H2)=>(house(H1)&house(H2)))))) ======================================================= =>(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 " %~ %~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %~ 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)))). ============================================ %~ 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 %~ %~ %%%%% goal=baseKB:kif_compile. time=0.31522035598754883. passed=passed=info(why_was_true(baseKB:kif_compile)) no_proof_for(kif_compile). no_proof_for(kif_compile). no_proof_for(kif_compile). result=passed. ]]>