API tools faq
paste
Advertisement
logicmoo

skolems example

logicmoo
Aug 12th, 2017
241
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 20.89 KB | None | 0 0
raw download clone embed print report
  1. /*
  2.  
  3. Started at Sat Aug 12 08:35:33 2017
  4. 32.854 seconds cpu time for 168,603,654 inferences
  5. 727,948 atoms, 15,635 functors, 16,146 predicates, 290 modules, 7,337,370 VM-codes
  6. %
  7.                        Limit    Allocated       In use
  8. Local  stack:    268,435,456      520,192        7,000 Bytes
  9. Global stack:    268,435,456  201,322,480  121,586,632 Bytes
  10. Trail  stack:    268,435,456   50,329,592          784 Bytes
  11. %
  12. 3 garbage collections gained 162,880,288 bytes in 0.017 seconds.
  13. 17 atom garbage collections gained 113,706 atoms in 0.288 seconds.
  14. 1,809 clause garbage collections gained 124,592 clauses in 0.159 seconds.
  15. Stack shifts: 4 local, 17 global, 14 trail in 0.005 seconds
  16. */
  17.  
  18.  
  19. % ==================================================================================================
  20.  
  21. :- test_boxlog(all([[Human, tHuman]],
  22.                    exists([[Heart, tHeart]], hasOrgan(Human, Heart)))).
  23.  
  24.  
  25. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl:14
  26. :- test_boxlog(all([[Human_VAR, tHuman]],
  27.                  exists([[Heart_VAR, tHeart]], hasOrgan(Human_VAR, Heart_VAR)))).
  28. kif :-
  29.       all([[Human, tHuman]], exists([[Heart, tHeart]], hasOrgan(Human, Heart))).
  30. qualify_nesc :-
  31.       all([[Human, tHuman]],
  32.           exists([[Heart, tHeart]], nesc(hasOrgan(Human, Heart)))).
  33. debugm(t123, sc_success(t123, t123:nnf(KB, all([Human, tHuman], exists([[Heart, tHeart]], nesc(b_d(KB, nesc, poss), hasOrgan(Human, Heart)))), v(&(v(&(nesc(b_d(KB, nesc, poss), nesc(b_d(KB, nesc, poss), hasOrgan(Human, Heart))), nesc(b_d(KB, nesc, poss), isa(Heart, tHeart))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), &(nesc(b_d(KB, nesc, poss), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))), isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)))), ~isa(Human, tHuman))))).
  34. nnf :-
  35.       v(&(v(&(nesc(nesc(hasOrgan(Human, Heart))), nesc(isa(Heart, tHeart))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), &(nesc(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))), isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)))), ~isa(Human, tHuman)).
  36. unq :-
  37.       v(&(v(&(nesc(hasOrgan(Human, Heart)), nesc(isa(Heart, tHeart))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), &(nesc(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))), isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)))), ~isa(Human, tHuman)).
  38. th_nnf_in :-
  39.       (   (   tru(hasOrgan(Human, Heart)),
  40.               tru(isa(Heart, tHeart))
  41.           ;   tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  42.           ),
  43.           (   neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  44.           ;   tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))),
  45.               tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart))
  46.           )
  47.       ;   neg(isa(Human, tHuman))
  48.       ).
  49. th_nnf_out :-
  50.       ~ (((n(tru(hasOrgan(Human, Heart)));n(tru(isa(Heart, tHeart)))), n(tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))));n(neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), (n(tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))));n(tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart))))), n(neg(isa(Human, tHuman)))).
  51. unused(proven_tru(isa(Heart, tHeart))) :-
  52.       unused((\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), proven_tru(isa(Human, tHuman)))).
  53. unused(proven_tru(hasOrgan(Human, Heart))) :-
  54.       unused((\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), proven_tru(isa(Human, tHuman)))).
  55. unused(proven_neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))) :-
  56.       proven_not_neg(isa(Human, tHuman)),
  57.       once((   \+ isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)
  58.            ;   \+ hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))
  59.            )).
  60. proven_tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)) :-
  61.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  62.       proven_tru(isa(Human, tHuman)).
  63. proven_tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  64.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  65.       proven_tru(isa(Human, tHuman)).
  66. proven_tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  67.       proven_tru(isa(Human, tHuman)),
  68.       once((   \+ isa(Heart, tHeart)
  69.            ;   \+ hasOrgan(Human, Heart)
  70.            )).
  71. proven_neg(isa(Human, tHuman)) :-
  72.       (   once((   proven_neg(isa(Heart, tHeart))
  73.                ;   proven_neg(hasOrgan(Human, Heart))
  74.                ))
  75.       ;   needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  76.           (   proven_neg(hasOrgan(Human,
  77.                                   skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  78.           ;   proven_neg(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart))
  79.           )
  80.       ).
  81.  
  82.  
  83.  
  84. % ==================================================================================================
  85.  
  86. :- test_boxlog(=>(isa(Human, tHuman), all(Human, exists([[Heart, tHeart]], hasOrgan(Human, Heart))))).
  87.  
  88.  
  89. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl:17
  90. :- test_boxlog(=>(isa(Human_VAR, tHuman), all(Human_VAR, exists([[Heart_VAR, tHeart]], hasOrgan(Human_VAR, Heart_VAR))))).
  91. kif :-
  92.       =>(tHuman(Human), all(Human, exists([[Heart, tHeart]], hasOrgan(Human, Heart)))).
  93. qualify_nesc :-
  94.       nesc(=>(tHuman(Human), all(Human, exists([[Heart, tHeart]], hasOrgan(Human, Heart))))).
  95. debugm(t123, sc_success(t123, t123:nnf(KB, nesc(b_d(KB, nesc, poss), =>(tHuman(Human), all(Human, exists([[Heart, tHeart]], hasOrgan(Human, Heart))))), &(&(nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(nesc(b_d(KB, nesc, poss), hasOrgan(Human, Heart)), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))))), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(nesc(b_d(KB, nesc, poss), isa(Heart, tHeart)), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))))), &(nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))))), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart))))))))).
  96. nnf :-
  97.       &(&(nesc(v(~tHuman(Human), v(nesc(hasOrgan(Human, Heart)), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))))), nesc(v(~tHuman(Human), v(nesc(isa(Heart, tHeart)), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))))), &(nesc(v(~tHuman(Human), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))))), nesc(v(~tHuman(Human), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)))))).
  98. th_nnf_in :-
  99.       ( (   neg(tHuman(Human))
  100.         ;   tru(hasOrgan(Human, Heart))
  101.         ;   tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  102.         ),
  103.         (   neg(tHuman(Human))
  104.         ;   tru(isa(Heart, tHeart))
  105.         ;   tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  106.         )
  107.       ),
  108.       (   neg(tHuman(Human))
  109.       ;   neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  110.       ;   tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  111.       ),
  112.       (   neg(tHuman(Human))
  113.       ;   neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  114.       ;   tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart))
  115.       ).
  116. th_nnf_out :-
  117.       ~ ((n(neg(tHuman(Human))), n(tru(hasOrgan(Human, Heart))), n(tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))));n(neg(tHuman(Human))), n(tru(isa(Heart, tHeart))), n(tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))));n(neg(tHuman(Human))), n(neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), n(tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))));n(neg(tHuman(Human))), n(neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), n(tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)))).
  118. unused(proven_tru(isa(Heart, tHeart))) :-
  119.       unused((\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), proven_tru(tHuman(Human)))).
  120. unused(proven_tru(hasOrgan(Human, Heart))) :-
  121.       unused((\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), proven_tru(tHuman(Human)))).
  122. unused(proven_neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))) :-
  123.       \+ isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart),
  124.       proven_not_neg(tHuman(Human)).
  125. unused(proven_neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))) :-
  126.       \+ hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  127.       proven_not_neg(tHuman(Human)).
  128. proven_tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)) :-
  129.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  130.       proven_tru(tHuman(Human)).
  131. proven_tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  132.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  133.       proven_tru(tHuman(Human)).
  134. proven_tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  135.       \+ isa(Heart, tHeart),
  136.       proven_tru(tHuman(Human)).
  137. proven_tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  138.       \+ hasOrgan(Human, Heart),
  139.       proven_tru(tHuman(Human)).
  140. proven_neg(tHuman(Human)) :-
  141.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  142.       \+ isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart).
  143. proven_neg(tHuman(Human)) :-
  144.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  145.       \+ hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)).
  146. proven_neg(tHuman(Human)) :-
  147.       proven_neg(isa(Heart, tHeart)).
  148. proven_neg(tHuman(Human)) :-
  149.       proven_neg(hasOrgan(Human, Heart)).
  150.  
  151.  
  152.  
  153. % ==================================================================================================
  154.  
  155. :- test_boxlog(=>(isa(Human, tHuman), all(Human, =>(isa(Heart, tHeart), exists(Heart, hasOrgan(Human, Heart)))))).
  156.  
  157.  
  158. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl:20
  159. :- test_boxlog(=>(isa(Human_VAR, tHuman), all(Human_VAR, =>(isa(Heart_VAR, tHeart), exists(Heart_VAR, hasOrgan(Human_VAR, Heart_VAR)))))).
  160. kif :-
  161.       =>(tHuman(Human), all(Human, =>(tHeart(Heart), exists(Heart, hasOrgan(Human, Heart))))).
  162. qualify_nesc :-
  163.       nesc(=>(tHuman(Human), all(Human, =>(tHeart(Heart), exists(Heart, hasOrgan(Human, Heart)))))).
  164. debugm(t123, sc_success(t123, t123:nnf(KB, nesc(b_d(KB, nesc, poss), =>(tHuman(Human), all(Human, =>(tHeart(Heart), exists(Heart, hasOrgan(Human, Heart)))))), &(nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(~tHeart(Heart), v(nesc(b_d(KB, nesc, poss), hasOrgan(Human, Heart)), needs(skArg2ofHasorgan_1FnSk(Human)))))), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(~tHeart(Heart), v(~needs(skArg2ofHasorgan_1FnSk(Human)), hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human)))))))))).
  165. nnf :-
  166.       &(nesc(v(~tHuman(Human), v(~tHeart(Heart), v(nesc(hasOrgan(Human, Heart)), needs(skArg2ofHasorgan_1FnSk(Human)))))), nesc(v(~tHuman(Human), v(~tHeart(Heart), v(~needs(skArg2ofHasorgan_1FnSk(Human)), hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human))))))).
  167. th_nnf_in :-
  168.       (   neg(tHuman(Human))
  169.       ;   neg(tHeart(Heart))
  170.       ;   tru(hasOrgan(Human, Heart))
  171.       ;   tru(needs(skArg2ofHasorgan_1FnSk(Human)))
  172.       ),
  173.       (   neg(tHuman(Human))
  174.       ;   neg(tHeart(Heart))
  175.       ;   neg(needs(skArg2ofHasorgan_1FnSk(Human)))
  176.       ;   tru(hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human)))
  177.       ).
  178. th_nnf_out :-
  179.       ~ (n(neg(tHuman(Human))), n(neg(tHeart(Heart))), n(tru(hasOrgan(Human, Heart))), n(tru(needs(skArg2ofHasorgan_1FnSk(Human))));n(neg(tHuman(Human))), n(neg(tHeart(Heart))), n(neg(needs(skArg2ofHasorgan_1FnSk(Human)))), n(tru(hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human))))).
  180. unused(proven_tru(hasOrgan(Human, Heart))) :-
  181.       unused((\+needs(skArg2ofHasorgan_1FnSk(Human)), proven_tru(tHeart(Heart)), proven_tru(tHuman(Human)))).
  182. unused(proven_neg(needs(skArg2ofHasorgan_1FnSk(Human)))) :-
  183.       \+ hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human)),
  184.       proven_not_neg(tHeart(Heart)),
  185.       proven_not_neg(tHuman(Human)).
  186. proven_tru(hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human))) :-
  187.       needs(skArg2ofHasorgan_1FnSk(Human)),
  188.       proven_tru(tHeart(Heart)),
  189.       proven_tru(tHuman(Human)).
  190. proven_tru(needs(skArg2ofHasorgan_1FnSk(Human))) :-
  191.       \+ hasOrgan(Human, Heart),
  192.       proven_tru(tHeart(Heart)),
  193.       proven_tru(tHuman(Human)).
  194. proven_neg(tHuman(Human)) :-
  195.       proven_not_neg(tHeart(Heart)),
  196.       needs(skArg2ofHasorgan_1FnSk(Human)),
  197.       \+ hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human)).
  198. proven_neg(tHuman(Human)) :-
  199.       proven_not_neg(tHeart(Heart)),
  200.       proven_neg(hasOrgan(Human, Heart)).
  201. proven_neg(tHeart(Heart)) :-
  202.       proven_neg(hasOrgan(Human, Heart)),
  203.       proven_not_neg(tHuman(Human)).
  204. proven_neg(tHeart(Heart)) :-
  205.       needs(skArg2ofHasorgan_1FnSk(Human)),
  206.       proven_neg(hasOrgan(Human, skArg2ofHasorgan_1FnSk(Human))),
  207.       proven_not_neg(tHuman(Human)).
  208.  
  209.  
  210.  
  211. % ==================================================================================================
  212.  
  213.  
  214. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl:23
  215. :- test_boxlog(all(Human_VAR,
  216.                  exists(Heart_VAR,
  217.                         =>(isa(Human_VAR, tHuman), &(isa(Heart_VAR, tHeart), hasOrgan(Human_VAR, Heart_VAR)))))).
  218. kif :-
  219.       all(Human,
  220.           exists(Heart,
  221.                  =>(tHuman(Human), &(tHeart(Heart), hasOrgan(Human, Heart))))).
  222. qualify_nesc :-
  223.       all(Human,
  224.           exists(Heart,
  225.                  nesc(=>(tHuman(Human), &(tHeart(Heart), hasOrgan(Human, Heart)))))).
  226. debugm(t123, sc_success(t123, t123:nnf(KB, all(Human, exists(Heart, nesc(b_d(KB, nesc, poss), =>(tHuman(Human), &(tHeart(Heart), hasOrgan(Human, Heart)))))), &(v(&(nesc(b_d(KB, nesc, poss), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), tHeart(Heart)))), nesc(b_d(KB, nesc, poss), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), hasOrgan(Human, Heart))))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), &(nesc(b_d(KB, nesc, poss), v(~tHuman(Human), tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)))))))))).
  227. nnf :-
  228.       &(v(&(nesc(nesc(v(~tHuman(Human), tHeart(Heart)))), nesc(nesc(v(~tHuman(Human), hasOrgan(Human, Heart))))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), &(nesc(v(~tHuman(Human), tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), nesc(v(~tHuman(Human), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))))))).
  229. unq :-
  230.       &(v(&(nesc(v(~tHuman(Human), tHeart(Heart))), nesc(v(~tHuman(Human), hasOrgan(Human, Heart)))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), &(nesc(v(~tHuman(Human), tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), nesc(v(~tHuman(Human), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))))))).
  231. th_nnf_in :-
  232.       (   (   neg(tHuman(Human))
  233.           ;   tru(isa(Heart, tHeart))
  234.           ),
  235.           (   neg(tHuman(Human))
  236.           ;   tru(hasOrgan(Human, Heart))
  237.           )
  238.       ;   tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  239.       ),
  240.       (   neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  241.       ;   (   neg(tHuman(Human))
  242.           ;   tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart))
  243.           ),
  244.           (   neg(tHuman(Human))
  245.           ;   tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  246.           )
  247.       ).
  248. th_nnf_out :-
  249.       ~ ((n(neg(tHuman(Human))), n(tru(isa(Heart, tHeart)));n(neg(tHuman(Human))), n(tru(hasOrgan(Human, Heart)))), n(tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))));n(neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), (n(neg(tHuman(Human))), n(tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)));n(neg(tHuman(Human))), n(tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)))))).
  250. unused(proven_tru(isa(Heart, tHeart))) :-
  251.       proven_tru(tHuman(Human)),
  252.       unused(\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))).
  253. unused(proven_tru(hasOrgan(Human, Heart))) :-
  254.       proven_tru(tHuman(Human)),
  255.       unused(\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))).
  256. unused(proven_neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))) :-
  257.       proven_not_neg(tHuman(Human)),
  258.       (   \+ isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)
  259.       ;   \+ hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))
  260.       ).
  261. proven_tru(isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart)) :-
  262.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  263.       proven_tru(tHuman(Human)).
  264. proven_tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  265.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  266.       proven_tru(tHuman(Human)).
  267. proven_tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  268.       proven_tru(tHuman(Human)),
  269.       (   \+ isa(Heart, tHeart)
  270.       ;   \+ hasOrgan(Human, Heart)
  271.       ).
  272. proven_neg(tHuman(Human)) :-
  273.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  274.       \+ isa(skIsHeartInArg2ofHasorgan_1FnSk(Human), tHeart).
  275. proven_neg(tHuman(Human)) :-
  276.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  277.       \+ hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)).
  278. proven_neg(tHuman(Human)) :-
  279.       proven_neg(isa(Heart, tHeart)).
  280. proven_neg(tHuman(Human)) :-
  281.       proven_neg(hasOrgan(Human, Heart)).
  282.  
  283.  
  284. % ==================================================================================================
  285. :- test_boxlog(all(Human,
  286.                    =>(isa(Human, tHuman), exists(Heart, =>(isa(Heart, tHeart), hasOrgan(Human, Heart)))))).
  287.  
  288.  
  289. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/t/examples/fol/sanity_exists_01.pl:28
  290. :- test_boxlog(all(Human_VAR,
  291.                  =>(isa(Human_VAR, tHuman), exists(Heart_VAR, =>(isa(Heart_VAR, tHeart), hasOrgan(Human_VAR, Heart_VAR)))))).
  292. kif :-
  293.       all(Human,
  294.           =>(tHuman(Human), exists(Heart, =>(tHeart(Heart), hasOrgan(Human, Heart))))).
  295. qualify_nesc :-
  296.       all(Human,
  297.           nesc(=>(tHuman(Human), exists(Heart, =>(tHeart(Heart), hasOrgan(Human, Heart)))))).
  298. debugm(t123, sc_success(t123, t123:nnf(KB, all(Human, nesc(b_d(KB, nesc, poss), =>(tHuman(Human), exists(Heart, =>(tHeart(Heart), hasOrgan(Human, Heart)))))), &(nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(nesc(b_d(KB, nesc, poss), v(~tHeart(Heart), hasOrgan(Human, Heart))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))))), nesc(b_d(KB, nesc, poss), v(~tHuman(Human), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), v(~tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)))))))))).
  299. nnf :-
  300.       &(nesc(v(~tHuman(Human), v(nesc(v(~tHeart(Heart), hasOrgan(Human, Heart))), needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))))), nesc(v(~tHuman(Human), v(~needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), v(~tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)), hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))))))).
  301. th_nnf_in :-
  302.       (   neg(tHuman(Human))
  303.       ;   (   neg(tHeart(Heart))
  304.           ;   tru(hasOrgan(Human, Heart))
  305.           )
  306.       ;   tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  307.       ),
  308.       (   neg(tHuman(Human))
  309.       ;   neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  310.       ;   neg(tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  311.       ;   tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)))
  312.       ).
  313. th_nnf_out :-
  314.       ~ (n(neg(tHuman(Human))), (n(neg(tHeart(Heart))), n(tru(hasOrgan(Human, Heart)))), n(tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))));n(neg(tHuman(Human))), n(neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), n(neg(tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human)))), n(tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))))).
  315. unused(proven_tru(hasOrgan(Human, Heart))) :-
  316.       proven_tru(tHeart(Heart)),
  317.       unused((\+needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)), proven_tru(tHuman(Human)))).
  318. unused(proven_neg(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)))) :-
  319.       proven_not_neg(tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human))),
  320.       \+ hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  321.       proven_not_neg(tHuman(Human)).
  322. proven_tru(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  323.       proven_tru(tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human))),
  324.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  325.       proven_tru(tHuman(Human)).
  326. proven_tru(needs(skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  327.       proven_tru(tHeart(Heart)),
  328.       \+ hasOrgan(Human, Heart),
  329.       proven_tru(tHuman(Human)).
  330. proven_neg(tHuman(Human)) :-
  331.       proven_not_neg(tHeart(Heart)),
  332.       proven_neg(hasOrgan(Human, Heart)).
  333. proven_neg(tHuman(Human)) :-
  334.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  335.       proven_not_neg(tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human))),
  336.       proven_neg(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))).
  337. proven_neg(tHeart(skIsHeartInArg2ofHasorgan_1FnSk(Human))) :-
  338.       proven_neg(hasOrgan(Human, skIsHeartInArg2ofHasorgan_1FnSk(Human))),
  339.       needs(skIsHeartInArg2ofHasorgan_1FnSk(Human)),
  340.       proven_not_neg(tHuman(Human)).
  341. proven_neg(tHeart(Heart)) :-
  342.       proven_neg(hasOrgan(Human, Heart)),
  343.       proven_not_neg(tHuman(Human)).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!