API tools faq
paste
Advertisement
logicmoo

Untitled

logicmoo
Jan 17th, 2015
422
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
ZXBasic 8.28 KB | None | 0 0
raw download clone embed print report
  1. Proof:
  2. length = 4, depth = 2
  3. Goal#  Wff#  Wff Instance
  4. -----  ----  ------------
  5.   [0]  query   query :- [1].
  6.   [1]  asserted_t(fatherOf,phil,gun)      asserted_t(fatherOf,phil,gun) :- [2] , [3].
  7.   [2]  asserted_t(sonOf,gun,phil)         asserted_t(sonOf,gun,phil).
  8.   [3]  not_asserted_t(motherOf,phil,gun)         not_asserted_t(motherOf,phil,gun) :- [4].
  9.   [4]  not_asserted_t(female,gun)            not_asserted_t(female,gun).
  10. Proof END.
  11. %    succceeded(dbase_rules_pttp:pttp_prove(logicmoo_example22, query)).
  12. %
  13. %               do_pttp_test(logicmoo_example4).
  14. %
  15. %            pttp_load_wid(logicmoo_kb_refution).
  16. %
  17.  
  18. logicmoo_kb_refution:0  not_asserted_t(A,B,C);proven_t(A,B,C),not_refuted_t(A,B,C),not_unknowable_t(A,B,C).
  19. logicmoo_kb_refution:1  not_proven_t(A,B,C);not_refuted_t(A,B,C),not_unknowable_t(A,B,C).
  20. logicmoo_kb_refution:2  not_refuted_t(A,B,C);not_proven_t(A,B,C),not_asserted_t(A,B,C),not_unknowable_t(A,B,C).
  21. logicmoo_kb_refution:3  not_unknowable_t(A,B,C);not_proven_t(A,B,C),not_asserted_t(A,B,C),not_refuted_t(A,B,C).
  22. logicmoo_kb_refution:4  proven_t(A,B,C);not_refuted_t(A,B,C);refuted_t(A,B,C);unknowable_t(A,B,C).
  23. logicmoo_kb_refution:5  asserted_t(A,B,C);refuted_t(A,B,C);unknowable_t(A,B,C);not_asserted_t(unknowable,A,B,C).
  24. logicmoo_kb_refution:6  refuted_t(A,B,C);unknowable_t(A,B,C);not_unknowable_t(A,B,C).
  25. logicmoo_kb_refution:7  unknowable_t(A,B,C);proven_t(A,B,C);refuted_t(A,B,C).
  26. logicmoo_kb_refution:8  not_both_t(secondOrder_t(genls,A,B),secondOrder_isa_t(A,C));secondOrder_isa_t(B,C).
  27. logicmoo_kb_refution:9  not_both_t(secondOrder_t(disjointWith,A,B),proven_t(A,C,D));refuted_t(B,C,D).
  28. logicmoo_kb_refution:10  not_both_t(secondOrder_t(genlPreds,A,B),proven_t(A,C,D));proven_t(B,C,D).
  29. logicmoo_kb_refution:11  not_both_t(secondOrder_t(genlInverse,A,B),proven_t(A,D,C));proven_t(B,C,D).
  30. logicmoo_kb_refution:12  not_both_t(secondOrder_t(negationPreds,A,B),proven_t(A,C,D));refuted_t(B,C,D).
  31. logicmoo_kb_refution:13  not_both_t(secondOrder_t(negationInverse,A,B),proven_t(A,D,C));refuted_t(B,C,D).
  32. logicmoo_kb_refution:14  not_both_t(secondOrder_isa_t(transitive,A), (proven_t(A,C,B),proven_t(A,B,D)));proven_t(A,C,D).
  33. logicmoo_kb_refution:15  not_both_t(secondOrder_isa_t(reflexive,A),proven_t(A,C,B));proven_t(A,B,C).
  34. logicmoo_kb_refution:16  not_both_t(secondOrder_isa_t(symmetric,A),proven_t(A,C,B));proven_t(A,B,C).
  35. logicmoo_kb_refution:17  not_both_t(secondOrder_isa_t(irreflexive,A),proven_t(A,C,B));refuted_t(A,B,C).
  36. logicmoo_kb_refution:18  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlInverse,A,B));proven_t(irreflexive,B).
  37. logicmoo_kb_refution:19  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlPreds,B,A));proven_t(irreflexive,B).
  38. logicmoo_example4:1  secondOrder_t(genlInverse,parentOf,sonOf).
  39. logicmoo_example4:2  secondOrder_t(genlPreds,motherOf,parentOf).
  40. logicmoo_example4:3  secondOrder_isa_t(irreflexive,sonOf).
  41. logicmoo_example4:4  asserted_t(parentOf,son_1,father_1).
  42. logicmoo_example4:5  query:-refuted_t(sonOf,son_1,father_1).2.5.
  43. % 2,632 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 6136772 Lips)
  44.  
  45. Proof time: 0.0005372789999995575 seconds
  46. Proof:
  47. length = 6, depth = 3
  48. Goal#  Wff#  Wff Instance
  49. -----  ----  ------------
  50.   [0]  query   query :- [1].
  51.   [1]  refuted_t(sonOf,son_1,father_1)      refuted_t(sonOf,son_1,father_1) :- [2] , [3].
  52.   [2]  secondOrder_isa_t(irreflexive,sonOf)         secondOrder_isa_t(irreflexive,sonOf).
  53.   [3]  proven_t(sonOf,father_1,son_1)         proven_t(sonOf,father_1,son_1) :- [4] , [5].
  54.   [4]  secondOrder_t(genlInverse,parentOf,sonOf)            secondOrder_t(genlInverse,parentOf,sonOf).
  55.   [5]  proven_t(parentOf,son_1,father_1)            proven_t(parentOf,son_1,father_1) :- [6].
  56.   [6]  asserted_t(parentOf,son_1,father_1)               asserted_t(parentOf,son_1,father_1).
  57. Proof END.
  58. %    succceeded(dbase_rules_pttp:pttp_prove(logicmoo_example4, query)).
  59. %
  60. %               do_pttp_test(logicmoo_example3).
  61. %
  62. %            pttp_load_wid(logicmoo_kb_logic).
  63. %
  64.  
  65. logicmoo_kb_logic:0  not_asserted_t(A,B,C);proven_t(A,B,C).
  66. logicmoo_kb_logic:1  not_proven_t(A,B,C);possible_t(A,B,C),not_unknowable_t(A,B,C),not_refuted_t(A,B,C).
  67. logicmoo_kb_logic:2  not_possible_t(A,B,C);not_refuted_t(A,B,C).
  68. logicmoo_kb_logic:3  not_refuted_t(A,B,C);not_proven_t(A,B,C).
  69. logicmoo_kb_logic:4  not_unknowable_t(A,B,C);not_proven_t(A,B,C),not_asserted_t(A,B,C),not_refuted_t(A,B,C).
  70. logicmoo_kb_logic:5  asserted_t(A,B,C);not_proven_t(A,B,C).
  71. logicmoo_kb_logic:6  proven_t(A,B,C);not_asserted_t(A,B,C).
  72. logicmoo_kb_logic:7  possible_t(A,B,C);refuted_t(A,B,C).
  73. logicmoo_kb_logic:8  refuted_t(A,B,C);possible_t(A,B,C).
  74. logicmoo_kb_logic:9  unknowable_t(A,B,C);possible_t(A,B,C).
  75. logicmoo_kb_logic:10  not_both_t(secondOrder_t(genls,A,B),secondOrder_isa_t(A,C));secondOrder_isa_t(B,C).
  76. logicmoo_kb_logic:11  not_both_t(secondOrder_t(disjointWith,A,B),asserted_t(A,C,D));refuted_t(B,C,D).
  77. logicmoo_kb_logic:12  not_both_t(secondOrder_t(genlPreds,A,B),asserted_t(A,C,D));proven_t(B,C,D).
  78. logicmoo_kb_logic:13  not_both_t(secondOrder_t(genlInverse,A,B),asserted_t(A,D,C));proven_t(B,C,D).
  79. logicmoo_kb_logic:14  not_both_t(secondOrder_t(negationPreds,A,B),asserted_t(A,C,D));refuted_t(B,C,D).
  80. logicmoo_kb_logic:15  not_both_t(secondOrder_t(negationInverse,A,B),asserted_t(A,D,C));refuted_t(B,C,D).
  81. logicmoo_kb_logic:16  not_both_t(secondOrder_isa_t(transitive,A), (asserted_t(A,C,B),asserted_t(A,B,D)));proven_t(A,C,D).
  82. logicmoo_kb_logic:17  not_secondOrder_isa_t(reflexive,A);proven_t(A,B,B).
  83. logicmoo_kb_logic:18  not_both_t(secondOrder_isa_t(symmetric,A),asserted_t(A,C,B));proven_t(A,B,C).
  84. logicmoo_kb_logic:19  not_both_t(secondOrder_isa_t(irreflexive,A),asserted_t(A,C,B));not_asserted_t(A,B,C).
  85. logicmoo_kb_logic:20  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlInverse,A,B));proven_t(irreflexive,B).
  86. logicmoo_kb_logic:21  not_both_t(secondOrder_isa_t(irreflexive,A),secondOrder_t(genlPreds,B,A));proven_t(irreflexive,B).
  87. logicmoo_example3:1  secondOrder_t(genlInverse,parentOf,sonOf).
  88. logicmoo_example3:2  secondOrder_t(genlPreds,motherOf,parentOf).
  89. logicmoo_example3:3  secondOrder_isa_t(irreflexive,sonOf).
  90. logicmoo_example3:4  asserted_t(parentOf,son_1,father_1).
  91. logicmoo_example3:5  query:-not_asserted_t(sonOf,son_1,father_1).2.5.
  92. % 3,709 inferences, 0.001 CPU in 0.001 seconds (98% CPU, 6710596 Lips)
  93.  
  94. Proof time: 0.0006547660000002509 seconds
  95. Proof:
  96. length = 6, depth = 3
  97. Goal#  Wff#  Wff Instance
  98. -----  ----  ------------
  99.   [0]  query   query :- [1].
  100.   [1]  not_asserted_t(sonOf,son_1,father_1)      not_asserted_t(sonOf,son_1,father_1) :- [2] , [3].
  101.   [2]  secondOrder_isa_t(irreflexive,sonOf)         secondOrder_isa_t(irreflexive,sonOf).
  102.   [3]  asserted_t(sonOf,father_1,son_1)         asserted_t(sonOf,father_1,son_1) :- [4].
  103.   [4]  proven_t(sonOf,father_1,son_1)            proven_t(sonOf,father_1,son_1) :- [5] , [6].
  104.   [5]  secondOrder_t(genlInverse,parentOf,sonOf)               secondOrder_t(genlInverse,parentOf,sonOf).
  105.   [6]  asserted_t(parentOf,son_1,father_1)               asserted_t(parentOf,son_1,father_1).
  106. Proof END.
  107. %    succceeded(dbase_rules_pttp:pttp_prove(logicmoo_example3, query)).
  108. %
  109. :- dynamic pttp_test_took/3.
  110.  
  111. pttp_test_took(chang_lee_example1, success, 0.017774654000000112).
  112. pttp_test_took(chang_lee_example2, success, 0.007574271999999382).
  113. pttp_test_took(chang_lee_example3, success, 0.0016142770000016071).
  114. pttp_test_took(chang_lee_example4, success, 0.0005561190000022975).
  115. pttp_test_took(chang_lee_example5, success, 0.0003571740000012369).
  116. pttp_test_took(chang_lee_example6, success, 0.0005447289999978011).
  117. pttp_test_took(chang_lee_example7, success, 0.0004462469999992891).
  118. pttp_test_took(chang_lee_example8, success, 0.018975419000000215).
  119. pttp_test_took(chang_lee_example9, success, 0.001030349000000541).
  120. pttp_test_took(logicmoo_example1, success, 0.000303224999999685).
  121. pttp_test_took(logicmoo_example1_holds, success, 0.00029053800000156116).
  122. pttp_test_took(logicmoo_example1_holds2, failure, 0.00021594500000077232).
  123. pttp_test_took(logicmoo_example2, success, 0.0004661060000010764).
  124. pttp_test_took(logicmoo_example22, success, 0.0004307779999983552).
  125. pttp_test_took(logicmoo_example4, success, 0.0007900379999981055).
  126. pttp_test_took(logicmoo_example3, success, 0.0009260170000011669).
  127.  
  128. %       gripe_pttp_failure(logicmoo_example1_holds2).
  129. %
  130. true.
  131.  
  132. 2 ?-
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!