logicmoo_workspace
logicmoo_workspace copied to clipboard
Published
20 hours ago •
logicmoo
logicmoo
logicmoo.base.examples.fol.ROOM_NUMBERS_01 JUnit
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 "['room_numbers_01.pfc.pl']")
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/room_numbers_01.pfc.pl % JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/ROOM_NUMBERS_01/ % ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AROOM_NUMBERS_01 % ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/440
%~ 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/room_numbers_01.pfc.pl'),
%~ this_test_might_need( :-( use_module( library(logicmoo_plarkc))))
:- set_kif_option(+assert).
% must_be_satifiable(P):- kif_to_boxlog(P,BoxLog),all_asserted(BoxLog).
% Version A - Two rooms
/*~
~*/
% must_be_satifiable(P):- kif_to_boxlog(P,BoxLog),all_asserted(BoxLog).
% Version A - Two rooms
exists(R1,room_number(R1,22)).
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/room_numbers_01.pfc.pl:10
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_53710,room_number(_53710,22))))))
% xgrun compiled into parser_chat80 0.00 sec, 0 clauses
% xgproc compiled into parser_chat80 0.03 sec, 0 clauses
** Grammar from file /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_nlu/ext/chat80/original/clone.xg: 192 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.70 sec, 3 clauses
% /var/lib/jenkins/.local/share/swi-prolog/pack/logicmoo_utils/prolog/debuggery/dmsg compiled into dmsg 0.14 sec, -16 clauses
=======================================================
exists('$VAR'('Room_number'),room_number('$VAR'('Room_number'),22))
============================================
?- kif_to_boxlog( exists(Room_number,room_number(Room_number,22)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Room_number
%~ " ?Room_number room_number 22 "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Room_number'),necessary(room_number('$VAR'('Room_number'),22)))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Room_number,1,nesc(room_number(Room_number,22)))==>nesc(room_number(Room_number,22)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Room_number nesc(room_number(Room_number,22))
%~ It's Proof that:
%~ " ?Room_number room_number 22 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(Room_number,1,nesc(room_number(Room_number,22))) ==>
nesc( room_number(Room_number,22))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('R1'),necessary(room_number('$VAR'('R1'),22)))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?R1 nesc(room_number(R1,22))
%~ It's Proof that:
%~ " ?R1 room_number 22 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(R1,1,nesc(room_number(R1,22)))==>nesc(room_number(R1,22)).
~*/
exists(R1,room_number(R1,77)).
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(exists(_47136,room_number(_47136,77))))))
=======================================================
exists('$VAR'('Room_number'),room_number('$VAR'('Room_number'),77))
============================================
?- kif_to_boxlog( exists(Room_number,room_number(Room_number,77)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ There exists ?Room_number
%~ " ?Room_number room_number 77 "
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = exists('$VAR'('Room_number'),necessary(room_number('$VAR'('Room_number'),77)))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 1 entailment(s):
'$existential'(Room_number,1,nesc(room_number(Room_number,77)))==>nesc(room_number(Room_number,77)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?Room_number nesc(room_number(Room_number,77))
%~ It's Proof that:
%~ " ?Room_number room_number 77 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
( '$existential'(Room_number,1,nesc(room_number(Room_number,77))) ==>
nesc( room_number(Room_number,77))).
============================================
%~ kif_to_boxlog_attvars2 = exists('$VAR'('R1'),necessary(room_number('$VAR'('R1'),77)))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ by default ?R1 nesc(room_number(R1,77))
%~ It's Proof that:
%~ " ?R1 room_number 77 " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'$existential'(R1,1,nesc(room_number(R1,77)))==>nesc(room_number(R1,77)).
~*/
all(R, (room_number(R,22) => (room(R) & ~big(R)))) .
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( all(R,room_number(R,22)=>(room(R)& ~big(R)))))))
=======================================================
all('$VAR'('Big_Room'),=>(room_number('$VAR'('Big_Room'),22),&(room('$VAR'('Big_Room')),~(big('$VAR'('Big_Room'))))))
============================================
?- kif_to_boxlog( all(Big_Room,room_number(Big_Room,22)=>(room(Big_Room)& ~big(Big_Room))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Big_Room
%~ (If:
%~ ?Big_Room room_number 22 then it is
%~ Implied that:
%~ " ?Big_Room isa room " and
%~ " ?Big_Room isa big " is false)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Big_Room'),necessary(=>(room_number('$VAR'('Big_Room'),22),and(room('$VAR'('Big_Room')),not(big('$VAR'('Big_Room')))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 6 entailment(s):
nesc(room(Big_Room))&poss(big(Big_Room))==>poss(~room_number(Big_Room,22)).
nesc(~big(Big_Room))&poss(~room(Big_Room))==>poss(~room_number(Big_Room,22)).
nesc(room_number(Big_Room,22))&nesc(room(Big_Room))==>nesc(~big(Big_Room)).
nesc(room_number(Big_Room,22))&nesc(~big(Big_Room))==>nesc(room(Big_Room)).
nesc(room_number(Big_Room,22))&poss(big(Big_Room))==>poss(~room(Big_Room)).
nesc(room_number(Big_Room,22))&poss(~room(Big_Room))==>poss(big(Big_Room)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room isa room " is necessarily true and
%~ " ?Big_Room isa big " is possible
%~ It's Proof that:
%~ " ?Big_Room room_number 22 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room(Big_Room))&poss(big(Big_Room))==>poss(~room_number(Big_Room,22)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room isa big " is necessarily false and
%~ " ?Big_Room isa room " is possibly false
%~ It's Proof that:
%~ " ?Big_Room room_number 22 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(~big(Big_Room))&poss(~room(Big_Room))==>poss(~room_number(Big_Room,22)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 22 " is necessarily true and
%~ " ?Big_Room isa room " is necessarily true
%~ It's Proof that:
%~ " ?Big_Room isa big " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,22))&nesc(room(Big_Room))==>nesc(~big(Big_Room)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 22 " is necessarily true and
%~ " ?Big_Room isa big " is necessarily false
%~ It's Proof that:
%~ " ?Big_Room isa room " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,22))&nesc(~big(Big_Room))==>nesc(room(Big_Room)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 22 " is necessarily true and
%~ " ?Big_Room isa big " is possible
%~ It's Proof that:
%~ " ?Big_Room isa room " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,22))&poss(big(Big_Room))==>poss(~room(Big_Room)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 22 " is necessarily true and
%~ " ?Big_Room isa room " is possibly false
%~ It's Proof that:
%~ " ?Big_Room isa big " is possible
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,22))&poss(~room(Big_Room))==>poss(big(Big_Room)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('R'),necessary(=>(room_number('$VAR'('R'),22),and(room('$VAR'('R')),not(big('$VAR'('R')))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R isa big " is necessarily false and
%~ " ?R isa room " is possibly false
%~ It's Proof that:
%~ " ?R room_number 22 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(~big(R))&poss(~room(R))==>poss(~room_number(R,22)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 22 " is necessarily true and
%~ " ?R isa room " is possibly false
%~ It's Proof that:
%~ " ?R isa big " is possible
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,22))&poss(~room(R))==>poss(big(R)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 22 " is necessarily true and
%~ " ?R isa big " is necessarily false
%~ It's Proof that:
%~ " ?R isa room " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,22))&nesc(~big(R))==>nesc(room(R)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R isa room " is necessarily true and
%~ " ?R isa big " is possible
%~ It's Proof that:
%~ " ?R room_number 22 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room(R))&poss(big(R))==>poss(~room_number(R,22)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 22 " is necessarily true and
%~ " ?R isa big " is possible
%~ It's Proof that:
%~ " ?R isa room " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,22))&poss(big(R))==>poss(~room(R)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 22 " is necessarily true and
%~ " ?R isa room " is necessarily true
%~ It's Proof that:
%~ " ?R isa big " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,22))&nesc(room(R))==>nesc(~big(R)).
~*/
all(R, (room_number(R,77) => (room(R) & big(R)))) .
% need proof that
/*~
%~ debugm( baseKB,
%~ show_success( baseKB,
%~ baseKB : ain( clif( all(R,room_number(R,77)=>(room(R)&big(R)))))))
=======================================================
all('$VAR'('Big_Room'),=>(room_number('$VAR'('Big_Room'),77),&(room('$VAR'('Big_Room')),big('$VAR'('Big_Room')))))
============================================
?- kif_to_boxlog( all(Big_Room,room_number(Big_Room,77)=>(room(Big_Room)&big(Big_Room))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Big_Room
%~ (If:
%~ ?Big_Room room_number 77 then it is
%~ Implied that:
%~ " ?Big_Room isa room " and
%~ " ?Big_Room isa big " )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Big_Room'),necessary(=>(room_number('$VAR'('Big_Room'),77),and(room('$VAR'('Big_Room')),big('$VAR'('Big_Room'))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 6 entailment(s):
nesc(big(Big_Room))&poss(~room(Big_Room))==>poss(~room_number(Big_Room,77)).
nesc(room(Big_Room))&poss(~big(Big_Room))==>poss(~room_number(Big_Room,77)).
nesc(room_number(Big_Room,77))&nesc(big(Big_Room))==>nesc(room(Big_Room)).
nesc(room_number(Big_Room,77))&nesc(room(Big_Room))==>nesc(big(Big_Room)).
nesc(room_number(Big_Room,77))&poss(~big(Big_Room))==>poss(~room(Big_Room)).
nesc(room_number(Big_Room,77))&poss(~room(Big_Room))==>poss(~big(Big_Room)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room isa big " is necessarily true and
%~ " ?Big_Room isa room " is possibly false
%~ It's Proof that:
%~ " ?Big_Room room_number 77 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(big(Big_Room))&poss(~room(Big_Room))==>poss(~room_number(Big_Room,77)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room isa room " is necessarily true and
%~ " ?Big_Room isa big " is possibly false
%~ It's Proof that:
%~ " ?Big_Room room_number 77 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room(Big_Room))&poss(~big(Big_Room))==>poss(~room_number(Big_Room,77)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 77 " is necessarily true and
%~ " ?Big_Room isa big " is necessarily true
%~ It's Proof that:
%~ " ?Big_Room isa room " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,77))&nesc(big(Big_Room))==>nesc(room(Big_Room)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 77 " is necessarily true and
%~ " ?Big_Room isa room " is necessarily true
%~ It's Proof that:
%~ " ?Big_Room isa big " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,77))&nesc(room(Big_Room))==>nesc(big(Big_Room)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 77 " is necessarily true and
%~ " ?Big_Room isa big " is possibly false
%~ It's Proof that:
%~ " ?Big_Room isa room " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,77))&poss(~big(Big_Room))==>poss(~room(Big_Room)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big_Room room_number 77 " is necessarily true and
%~ " ?Big_Room isa room " is possibly false
%~ It's Proof that:
%~ " ?Big_Room isa big " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big_Room,77))&poss(~room(Big_Room))==>poss(~big(Big_Room)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('R'),necessary(=>(room_number('$VAR'('R'),77),and(room('$VAR'('R')),big('$VAR'('R'))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R isa big " is necessarily true and
%~ " ?R isa room " is possibly false
%~ It's Proof that:
%~ " ?R room_number 77 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(big(R))&poss(~room(R))==>poss(~room_number(R,77)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 77 " is necessarily true and
%~ " ?R isa room " is possibly false
%~ It's Proof that:
%~ " ?R isa big " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,77))&poss(~room(R))==>poss(~big(R)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 77 " is necessarily true and
%~ " ?R isa big " is necessarily true
%~ It's Proof that:
%~ " ?R isa room " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,77))&nesc(big(R))==>nesc(room(R)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R isa room " is necessarily true and
%~ " ?R isa big " is possibly false
%~ It's Proof that:
%~ " ?R room_number 77 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room(R))&poss(~big(R))==>poss(~room_number(R,77)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 77 " is necessarily true and
%~ " ?R isa big " is possibly false
%~ It's Proof that:
%~ " ?R isa room " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,77))&poss(~big(R))==>poss(~room(R)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 77 " is necessarily true and
%~ " ?R isa room " is necessarily true
%~ It's Proof that:
%~ " ?R isa big " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,77))&nesc(room(R))==>nesc(big(R)).
~*/
% need proof that
?- must_be_satifiable(( room_number(R1,22) & room_number(R2,77) => R1 \= R2 )).
/*~
%~ warn_undefined( baseKB : add_args(
%~ must_be_satifiable( (room_number(R1,22)&room_number(R2,77))=>(R1\=R2)),
%~ ( ~( must_be_satifiable( room_number(R1,22))) v
%~ ~( must_be_satifiable( room_number(R2,77))) v
%~ must_be_satifiable( R1\=R2)), V,Add_argsMust_be_satifiable11,
%~ [],Add_argsMust_be_satifiable9,
%~ Add_argsMust_be_satifiable8,[],[],
%~ Add_argsMust_be_satifiable5,_47350,
%~ [[]],
%~ Add_argsMust_be_satifiable4, Add_argsMust_be_satifiable, Args))
~*/
:- reset_kb(kbii).
% Version B - Simpler
/*~
%~ message_hook_type(error)
%~ message_hook(
%~ error(existence_error(procedure,baseKB:reset_kb/1),context(system:catch/3,Context_Kw)),
%~ error,
%~ [ '~q/~w: '-[catch,3],
%~ 'Unknown procedure: ~q' - [ baseKB : reset_kb/1]])
catch/3: Unknown procedure: baseKB:reset_kb/1
ERROR: catch/3: Unknown procedure: baseKB:reset_kb/1
%~ message_hook_type(warning)
%~ message_hook(
%~ goal_failed(directive,baseKB:reset_kb(kbii)),
%~ warning,
%~ [ 'Goal (~w) failed: ~p' - [ directive,
%~ baseKB : reset_kb(kbii)]])
Goal (directive) failed: baseKB:reset_kb(kbii)
Warning: Goal (directive) failed: baseKB:reset_kb(kbii)
~*/
% Version B - Simpler
all(R, (room_number(R,22) => ( ~big(R)))) .
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(all(_24192,room_number(_24192,22)=>(~big(_24192)))))))
=======================================================
all('$VAR'('Big'),=>(room_number('$VAR'('Big'),22),~(big('$VAR'('Big')))))
============================================
?- kif_to_boxlog( all(Big,room_number(Big,22)=>(~big(Big))) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Big
%~ (If:
%~ ?Big room_number 22 then it is
%~ Implied that:
%~ " ?Big isa big " is false)
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Big'),necessary(=>(room_number('$VAR'('Big'),22),not(big('$VAR'('Big'))))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s):
nesc(room_number(Big,22))==>nesc(~big(Big)).
poss(big(Big))==>poss(~room_number(Big,22)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big room_number 22 " is necessarily true
%~ It's Proof that:
%~ " ?Big isa big " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big,22))==>nesc(~big(Big)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big isa big " is possible
%~ It's Proof that:
%~ " ?Big room_number 22 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(big(Big))==>poss(~room_number(Big,22)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('R'),necessary(=>(room_number('$VAR'('R'),22),not(big('$VAR'('R'))))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R isa big " is possible
%~ It's Proof that:
%~ " ?R room_number 22 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(big(R))==>poss(~room_number(R,22)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 22 " is necessarily true
%~ It's Proof that:
%~ " ?R isa big " is necessarily false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,22))==>nesc(~big(R)).
~*/
all(R, (room_number(R,77) => ( big(R)))) .
% need proof that
/*~
%~ debugm(baseKB,show_success(baseKB,baseKB:ain(clif(all(_48130,room_number(_48130,77)=>big(_48130))))))
=======================================================
all('$VAR'('Big'),=>(room_number('$VAR'('Big'),77),big('$VAR'('Big'))))
============================================
?- kif_to_boxlog( all(Big,room_number(Big,77)=>big(Big)) ).
% In English:
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~
%~ For all ?Big
%~ (If:
%~ ?Big room_number 77 then it is
%~ Implied that:
%~ ?Big isa big )
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ kif_to_boxlog_attvars2 = forall('$VAR'('Big'),necessary(=>(room_number('$VAR'('Big'),77),big('$VAR'('Big')))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results in the following 2 entailment(s):
nesc(room_number(Big,77))==>nesc(big(Big)).
poss(~big(Big))==>poss(~room_number(Big,77)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big room_number 77 " is necessarily true
%~ It's Proof that:
%~ " ?Big isa big " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(Big,77))==>nesc(big(Big)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?Big isa big " is possibly false
%~ It's Proof that:
%~ " ?Big room_number 77 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(~big(Big))==>poss(~room_number(Big,77)).
============================================
%~ kif_to_boxlog_attvars2 = forall('$VAR'('R'),necessary(=>(room_number('$VAR'('R'),77),big('$VAR'('R')))))
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R isa big " is possibly false
%~ It's Proof that:
%~ " ?R room_number 77 " is possibly false
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(~big(R))==>poss(~room_number(R,77)).
% AND
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%~ Whenever:
%~ " ?R room_number 77 " is necessarily true
%~ It's Proof that:
%~ " ?R isa big " is necessarily true
%~
%~ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nesc(room_number(R,77))==>nesc(big(R)).
~*/
% need proof that
?- must_be_satifiable(( room_number(R1,22) & room_number(R2,77) => R1 \= R2 )).
% ISSUE: https://github.com/logicmoo/logicmoo_workspace/issues/440
% EDIT: https://github.com/logicmoo/logicmoo_workspace/edit/master/packs_sys/logicmoo_base/t/examples/fol/room_numbers_01.pfc.pl
% JENKINS: https://jenkins.logicmoo.org/job/logicmoo_workspace/lastBuild/testReport/logicmoo.base.examples.fol/ROOM_NUMBERS_01/
% ISSUE_SEARCH: https://github.com/logicmoo/logicmoo_workspace/issues?q=is%3Aissue+label%3AROOM_NUMBERS_01
/*~
%~ /var/lib/jenkins/workspace/logicmoo_workspace@2/packs_sys/logicmoo_base/t/examples/fol/room_numbers_01.pfc.pl:26
%~ warn_undefined( baseKB : add_args(
%~ must_be_satifiable( (room_number(R1,22)&room_number(R2,77))=>(R1\=R2)),
%~ ( ~( must_be_satifiable( room_number(R1,22))) v
%~ ~( must_be_satifiable( room_number(R2,77))) v
%~ must_be_satifiable( R1\=R2)), V,Add_argsMust_be_satifiable11,
%~ [],Add_argsMust_be_satifiable9,
%~ Add_argsMust_be_satifiable8,[],[],
%~ Add_argsMust_be_satifiable5,_47732,
%~ [[]],
%~ Add_argsMust_be_satifiable4, Add_argsMust_be_satifiable, Args))
~*/
%~ unused(no_junit_results)
logicmoo.base.examples.fol.ROOM_NUMBERS_01 JUnit error = catch/3: Unknown procedure: baseKB:reset_kb/1
logicmoo.base.examples.fol.ROOM_NUMBERS_01 JUnit warning = Goal (directive) failed: baseKB:reset_kb(kbii)
%~ test_completed_exit(48)
totalTime=5.000
FAILED: /var/lib/jenkins/workspace/logicmoo_workspace/bin/lmoo-junit-minor -k room_numbers_01.pfc.pl (returned 48) Add_LABELS='Errors,Warnings' Rem_LABELS='Skipped,Overtime,Skipped,Skipped'
