API tools faq
paste
Advertisement
logicmoo

PTTP EXamples

logicmoo
Jan 28th, 2015
396
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
PHP 97.13 KB | None | 0 0
raw download clone embed print report
  1. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/src_lib/logicmoo_util/logicmoo_util_library.pl:537:
  2.         Goal (directive) failed: user:module_predicates_are_exported(logicmoo_util_library)
  3. %     passed(logicmoo_util_dcg:theCode(A=1),
  4. %         do_dcgTest("",
  5. %                    logicmoo_util_dcg:theCode(A=1),
  6. %                    logicmoo_util_dcg: (A==1)),
  7. %         do_dcgTest("",
  8. %                    logicmoo_util_dcg:theCode(1=1),
  9. %                    logicmoo_util_dcg: (1==1))).
  10. %
  11. %     passed(logicmoo_util_dcg:theRest(A),
  12. %         do_dcgTest([a, b|B],
  13. %                    logicmoo_util_dcg:theRest(A),
  14. %                    logicmoo_util_dcg: (A==[a, b|B])),
  15. %         do_dcgTest([a, b|C],
  16. %                    logicmoo_util_dcg:theRest([a, b|C]),
  17. %                    logicmoo_util_dcg: ([a, b|C]==[a, b|C]))).
  18. %
  19. %     passed(logicmoo_util_dcg:theText([this, is, text]),
  20. %         do_dcgTest("this is text",
  21. %                    logicmoo_util_dcg:theText([this, is, text]),
  22. %                    logicmoo_util_dcg:true),
  23. %         do_dcgTest("this is text",
  24. %                    logicmoo_util_dcg:theText([this, is, text]),
  25. %                    logicmoo_util_dcg:true)).
  26. %
  27. %     passed(logicmoo_util_dcg:theString("this is a string"),
  28. %         do_dcgTest("this is a string",
  29. %                    logicmoo_util_dcg:theString("this is a string"),
  30. %                    logicmoo_util_dcg:true),
  31. %         do_dcgTest("this is a string",
  32. %                    logicmoo_util_dcg:theString("this is a string"),
  33. %                    logicmoo_util_dcg:true)).
  34. %
  35. %     passed(logicmoo_util_dcg:theAll([a, b|A]),
  36. %         do_dcgTest([a, b|A],
  37. %                    logicmoo_util_dcg:theAll([a, b|A]),
  38. %                    logicmoo_util_dcg:true),
  39. %         do_dcgTest([a, b],
  40. %                    logicmoo_util_dcg:theAll([a, b]),
  41. %                    logicmoo_util_dcg:true)).
  42. %
  43. %     passed(logicmoo_util_dcg:dcgStartsWith0(theText([this, is])),
  44. %         do_dcgTest("this is text",
  45. %                    logicmoo_util_dcg:dcgStartsWith0(theText([this, is])),
  46. %                    logicmoo_util_dcg:true),
  47. %         do_dcgTest("this is text",
  48. %                    logicmoo_util_dcg:dcgStartsWith0(theText([this, is])),
  49. %                    logicmoo_util_dcg:true)).
  50. %
  51. %     passed(logicmoo_util_dcg:theCode(A=1),
  52. %         do_dcgTest([a, b|_], logicmoo_util_dcg:theCode(A=1), A==1),
  53. %         do_dcgTest([a, b|_], logicmoo_util_dcg:theCode(1=1), 1==1)).
  54. %
  55. %     passed(logicmoo_util_dcg:theCode(A=1),
  56. %         do_dcgTest("anything", logicmoo_util_dcg:theCode(A=1), A==1),
  57. %         do_dcgTest("anything", logicmoo_util_dcg:theCode(1=1), 1==1)).
  58. %
  59. %     passed(logicmoo_util_dcg:dcgStartsWith(theText([this, is])),
  60. %         do_dcgTest("this is text",
  61. %                    logicmoo_util_dcg:dcgStartsWith(theText([this, is])),
  62. %                    true),
  63. %         do_dcgTest("this is text",
  64. %                    logicmoo_util_dcg:dcgStartsWith(theText([this, is])),
  65. %                    true)).
  66. %
  67. %     passed(logicmoo_util_dcg:dcgStartsWith1(theText([this])),
  68. %         do_dcgTest("this is text",
  69. %                    logicmoo_util_dcg:dcgStartsWith1(theText([this])),
  70. %                    true),
  71. %         do_dcgTest("this is text",
  72. %                    logicmoo_util_dcg:dcgStartsWith1(theText([this])),
  73. %                    true)).
  74. %
  75. not_installing(user,use_module('../ext/moo_ext_lisp_triska'))
  76. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp_statics.pl:177:
  77.         Singleton variables: [G,E,A,M,F,O,D]
  78. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp_statics.pl:181:
  79.         Singleton variables: [G,E,A,M,F,O,D]
  80. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp_statics.pl:255:
  81.         Singleton variables: [Time]
  82. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp_statics.pl:353:
  83.         Singleton variables: [ID]
  84. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp_statics.pl:354:
  85.         Singleton variables: [ID]
  86. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:296:
  87.         Singleton variables: [INFO]
  88. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:386:
  89.         Singleton variable in branch: N
  90. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:734:
  91.         Singleton variable in branch: B
  92. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:830:
  93.         Singleton variable in branch: B
  94. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:860:
  95.         Singleton variables: [ProofID]
  96. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:861:
  97.         Singleton variables: [Body]
  98. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:862:
  99.         Singleton variables: [Head,Body]
  100. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1038:
  101.         Singleton variables: [INFO]
  102. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1041:
  103.         Singleton variables: [N]
  104. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1054:
  105.         Singleton variables: [INFO]
  106. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1058:
  107.         Singleton variables: [INFO]
  108. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1111:
  109.         Singleton variables: [LC]
  110. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1112:
  111.         Singleton variables: [LC]
  112. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1113:
  113.         Singleton variables: [LC]
  114. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1117:
  115.         Singleton variables: [A,L]
  116. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1121:
  117.         Singleton variables: [LC]
  118. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1122:
  119.         Singleton variables: [LC]
  120. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1124:
  121.         Singleton variables: [LC]
  122. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1128:
  123.         Singleton variables: [LC]
  124. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1129:
  125.         Singleton variables: [LC]
  126. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1130:
  127.         Singleton variables: [LC]
  128. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1434:
  129.         Singleton variables: [BB]
  130. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1652:
  131.         Singleton variables: [F,A]
  132. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1653:
  133.         Singleton variables: [F,A]
  134. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1654:
  135.         Singleton variables: [A]
  136. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1655:
  137.         Singleton variables: [F,A]
  138. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1656:
  139.         Singleton variables: [F,A]
  140. Warning: /devel/LogicmooDeveloperFramework/PrologMUD/externals/MUD_ScriptEngines/snark/dbase_rules_pttp.pl:1657:
  141.         Singleton variables: [F,A]
  142. %    'we see this'.
  143. %
  144. %          do_pttp_test(chang_lee_example1).
  145. %
  146.  
  147.  
  148. %                    todo(warn(builtin_why(pretest_call, 1, number_of_rules(1)))).
  149. %
  150. chang_lee_example1:0  assumed_t(p,g(A,B),A,B).
  151.  
  152. %                todo(warn(builtin_why(assumed_t, 10, number_of_rules(1)))).
  153. %
  154. chang_lee_example1:1  assumed_t(p,A,h(A,B),B).
  155. chang_lee_example1:2  assumed_t(p,A,C,F):-assumed_t(p,D,B,A),assumed_t(p,B,C,E),assumed_t(p,D,E,F).
  156. chang_lee_example1:3  assumed_t(p,A,C,F):-assumed_t(p,A,B,D),assumed_t(p,B,E,C),assumed_t(p,D,E,F).
  157. chang_lee_example1:4  query:-assumed_t(p,k(A),A,k(A)).
  158. % 311 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2756066 Lips)
  159.  
  160. Proof time: 0.010423126999999921 seconds
  161. Proof:
  162. length = 4, depth = 1
  163. Goal#  Wff#  Wff Instance
  164. -----  ----  ------------
  165.   [0]  query   query :- [1].
  166.   [1]  assumed_t(p,k(h(_G579,_G579)),h(_G579,_G579),k(h(_G579,_G579)))      assumed_t(p,k(h(_G579,_G579)),h(_G579,_G579),k(h(_G579,_G579))) :- [2] , [3] , [4].
  167.   [2]  assumed_t(p,g(_G579,k(h(_G579,_G579))),_G579,k(h(_G579,_G579)))         assumed_t(p,g(_G579,k(h(_G579,_G579))),_G579,k(h(_G579,_G579))).
  168.   [3]  assumed_t(p,_G579,h(_G579,_G579),_G579)         assumed_t(p,_G579,h(_G579,_G579),_G579).
  169.   [4]  assumed_t(p,g(_G579,k(h(_G579,_G579))),_G579,k(h(_G579,_G579)))         assumed_t(p,g(_G579,k(h(_G579,_G579))),_G579,k(h(_G579,_G579))).
  170. Proof end.
  171. %                   succceeded(user:pttp_prove(chang_lee_example1, query)).
  172. %
  173. %          do_pttp_test(chang_lee_example2).
  174. %
  175.  
  176.  
  177. %               todo(warn(builtin_why(assumed_t, 10, number_of_rules(2)))).
  178. %
  179. chang_lee_example2:0  assumed_t(p,e,A,A).
  180. chang_lee_example2:1  assumed_t(p,A,e,A).
  181. chang_lee_example2:2  assumed_t(p,A,A,e).
  182. chang_lee_example2:3  assumed_t(p,a,b,c).
  183. chang_lee_example2:4  assumed_t(p,A,C,F):-assumed_t(p,D,B,A),assumed_t(p,B,C,E),assumed_t(p,D,E,F).
  184. chang_lee_example2:5  assumed_t(p,A,C,F):-assumed_t(p,A,B,D),assumed_t(p,B,E,C),assumed_t(p,D,E,F).
  185. chang_lee_example2:6  query:-assumed_t(p,b,a,c).
  186. % 73,120 inferences, 0.020 CPU in 0.020 seconds (100% CPU, 3622651 Lips)
  187.  
  188. Proof time: 0.02027707599999995 seconds
  189. Proof:
  190. length = 10, depth = 3
  191. Goal#  Wff#  Wff Instance
  192. -----  ----  ------------
  193.   [0]  query   query :- [1].
  194.   [1]  assumed_t(p,b,a,c)      assumed_t(p,b,a,c) :- [2] , [3] , [10].
  195.   [2]  assumed_t(p,b,b,e)         assumed_t(p,b,b,e).
  196.   [3]  assumed_t(p,b,c,a)         assumed_t(p,b,c,a) :- [4] , [8] , [9].
  197.   [4]  assumed_t(p,a,c,b)            assumed_t(p,a,c,b) :- [5] , [6] , [7].
  198.   [5]  assumed_t(p,a,a,e)               assumed_t(p,a,a,e).
  199.   [6]  assumed_t(p,a,b,c)               assumed_t(p,a,b,c).
  200.   [7]  assumed_t(p,e,b,b)               assumed_t(p,e,b,b).
  201.   [8]  assumed_t(p,c,c,e)            assumed_t(p,c,c,e).
  202.   [9]  assumed_t(p,a,e,a)            assumed_t(p,a,e,a).
  203.  [10]  assumed_t(p,e,c,c)         assumed_t(p,e,c,c).
  204. Proof end.
  205. %                   succceeded(user:pttp_prove(chang_lee_example2, query)).
  206. %
  207. %          do_pttp_test(chang_lee_example3).
  208. %
  209.  
  210. chang_lee_example3:0  assumed_t(p,e,A,A).
  211. chang_lee_example3:1  assumed_t(p,i(A),A,e).
  212. chang_lee_example3:2  assumed_t(p,A,C,F):-assumed_t(p,D,B,A),assumed_t(p,B,C,E),assumed_t(p,D,E,F).
  213. chang_lee_example3:3  assumed_t(p,A,C,F):-assumed_t(p,A,B,D),assumed_t(p,B,E,C),assumed_t(p,D,E,F).
  214. chang_lee_example3:4  query:-assumed_t(p,a,e,a).
  215. % 7,492 inferences, 0.002 CPU in 0.002 seconds (100% CPU, 3693380 Lips)
  216.  
  217. Proof time: 0.0021218909999998203 seconds
  218. Proof:
  219. length = 10, depth = 2
  220. Goal#  Wff#  Wff Instance
  221. -----  ----  ------------
  222.   [0]  query   query :- [1].
  223.   [1]  assumed_t(p,a,e,a)      assumed_t(p,a,e,a) :- [2] , [6] , [7].
  224.   [2]  assumed_t(p,i(i(a)),e,a)         assumed_t(p,i(i(a)),e,a) :- [3] , [4] , [5].
  225.   [3]  assumed_t(p,i(i(a)),i(a),e)            assumed_t(p,i(i(a)),i(a),e).
  226.   [4]  assumed_t(p,i(a),a,e)            assumed_t(p,i(a),a,e).
  227.   [5]  assumed_t(p,e,a,a)            assumed_t(p,e,a,a).
  228.   [6]  assumed_t(p,e,e,e)         assumed_t(p,e,e,e).
  229.   [7]  assumed_t(p,i(i(a)),e,a)         assumed_t(p,i(i(a)),e,a) :- [8] , [9] , [10].
  230.   [8]  assumed_t(p,i(i(a)),i(a),e)            assumed_t(p,i(i(a)),i(a),e).
  231.   [9]  assumed_t(p,i(a),a,e)            assumed_t(p,i(a),a,e).
  232.  [10]  assumed_t(p,e,a,a)            assumed_t(p,e,a,a).
  233. Proof end.
  234. %                   succceeded(user:pttp_prove(chang_lee_example3, query)).
  235. %
  236. %          do_pttp_test(chang_lee_example4).
  237. %
  238.  
  239. chang_lee_example4:0  assumed_t(p,e,A,A).
  240. chang_lee_example4:1  assumed_t(p,i(A),A,e).
  241. chang_lee_example4:2  assumed_t(p,A,C,F):-assumed_t(p,D,B,A),assumed_t(p,B,C,E),assumed_t(p,D,E,F).
  242. chang_lee_example4:3  assumed_t(p,A,C,F):-assumed_t(p,A,B,D),assumed_t(p,B,E,C),assumed_t(p,D,E,F).
  243. chang_lee_example4:4  query:-assumed_t(p,a,_,e).
  244. % 7,324 inferences, 0.002 CPU in 0.002 seconds (100% CPU, 3721032 Lips)
  245.  
  246. Proof time: 0.002049898999999966 seconds
  247. Proof:
  248. length = 10, depth = 2
  249. Goal#  Wff#  Wff Instance
  250. -----  ----  ------------
  251.   [0]  query   query :- [1].
  252.   [1]  assumed_t(p,a,i(a),e)      assumed_t(p,a,i(a),e) :- [2] , [6] , [7].
  253.   [2]  assumed_t(p,i(i(a)),e,a)         assumed_t(p,i(i(a)),e,a) :- [3] , [4] , [5].
  254.   [3]  assumed_t(p,i(i(a)),i(a),e)            assumed_t(p,i(i(a)),i(a),e).
  255.   [4]  assumed_t(p,i(a),a,e)            assumed_t(p,i(a),a,e).
  256.   [5]  assumed_t(p,e,a,a)            assumed_t(p,e,a,a).
  257.   [6]  assumed_t(p,e,i(a),i(a))         assumed_t(p,e,i(a),i(a)).
  258.   [7]  assumed_t(p,i(i(a)),i(a),e)         assumed_t(p,i(i(a)),i(a),e) :- [8] , [9] , [10].
  259.   [8]  assumed_t(p,e,i(i(a)),i(i(a)))            assumed_t(p,e,i(i(a)),i(i(a))).
  260.   [9]  assumed_t(p,i(i(a)),i(a),e)            assumed_t(p,i(i(a)),i(a),e).
  261.  [10]  assumed_t(p,e,e,e)            assumed_t(p,e,e,e).
  262. Proof end.
  263. %                   succceeded(user:pttp_prove(chang_lee_example4, query)).
  264. %
  265. %          do_pttp_test(chang_lee_example5).
  266. %
  267.  
  268. chang_lee_example5:0  assumed_t(p,e,A,A).
  269. chang_lee_example5:1  assumed_t(p,A,e,A).
  270. chang_lee_example5:2  assumed_t(p,A,i(A),e).
  271. chang_lee_example5:3  assumed_t(p,i(A),A,e).
  272. chang_lee_example5:4  assumed_t(s,a).
  273.  
  274. %                      todo(warn(builtin_why(assumed_t, 8, number_of_rules(1)))).
  275. %
  276. chang_lee_example5:5  assumed_t(s,C):-assumed_t(s,A),assumed_t(s,B),assumed_t(p,A,i(B),C).
  277. chang_lee_example5:6  assumed_t(p,A,C,F):-assumed_t(p,D,B,A),assumed_t(p,B,C,E),assumed_t(p,D,E,F).
  278. chang_lee_example5:7  assumed_t(p,A,C,F):-assumed_t(p,A,B,D),assumed_t(p,B,E,C),assumed_t(p,D,E,F).
  279. chang_lee_example5:8  query:-assumed_t(s,e).
  280. % 18,490 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 3170892 Lips)
  281.  
  282. Proof time: 0.005918321000000004 seconds
  283. Proof:
  284. length = 10, depth = 3
  285. Goal#  Wff#  Wff Instance
  286. -----  ----  ------------
  287.   [0]  query   query :- [1].
  288.   [1]  assumed_t(s,e)      assumed_t(s,e) :- [2] , [3] , [4].
  289.   [2]  assumed_t(s,a)         assumed_t(s,a).
  290.   [3]  assumed_t(s,a)         assumed_t(s,a).
  291.   [4]  assumed_t(p,a,i(a),e)         assumed_t(p,a,i(a),e) :- [5] , [6] , [7].
  292.   [5]  assumed_t(p,e,a,a)            assumed_t(p,e,a,a).
  293.   [6]  assumed_t(p,a,i(a),e)            assumed_t(p,a,i(a),e).
  294.   [7]  assumed_t(p,e,e,e)            assumed_t(p,e,e,e) :- [8] , [9] , [10].
  295.   [8]  assumed_t(p,_G14580,i(_G14580),e)               assumed_t(p,_G14580,i(_G14580),e).
  296.   [9]  assumed_t(p,i(_G14580),e,i(_G14580))               assumed_t(p,i(_G14580),e,i(_G14580)).
  297.  [10]  assumed_t(p,_G14580,i(_G14580),e)               assumed_t(p,_G14580,i(_G14580),e).
  298. Proof end.
  299. %                   succceeded(user:pttp_prove(chang_lee_example5, query)).
  300. %
  301. %          do_pttp_test(chang_lee_example6).
  302. %
  303.  
  304.  
  305. %               todo(warn(builtin_why(assumed_t, 8, number_of_rules(2)))).
  306. %
  307. chang_lee_example6:0  assumed_t(p,e,A,A).
  308. chang_lee_example6:1  assumed_t(p,A,e,A).
  309. chang_lee_example6:2  assumed_t(p,A,i(A),e).
  310. chang_lee_example6:3  assumed_t(p,i(A),A,e).
  311. chang_lee_example6:4  assumed_t(s,b).
  312. chang_lee_example6:5  assumed_t(s,C):-assumed_t(s,A),assumed_t(s,B),assumed_t(p,A,i(B),C).
  313. chang_lee_example6:6  assumed_t(p,A,C,F):-assumed_t(p,D,B,A),assumed_t(p,B,C,E),assumed_t(p,D,E,F).
  314. chang_lee_example6:7  assumed_t(p,A,C,F):-assumed_t(p,A,B,D),assumed_t(p,B,E,C),assumed_t(p,D,E,F).
  315. chang_lee_example6:8  query:-assumed_t(s,i(b)).
  316. % 1,381 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 3755044 Lips)
  317.  
  318. Proof time: 0.0004496199999999284 seconds
  319. Proof:
  320. length = 7, depth = 2
  321. Goal#  Wff#  Wff Instance
  322. -----  ----  ------------
  323.   [0]  query   query :- [1].
  324.   [1]  assumed_t(s,i(b))      assumed_t(s,i(b)) :- [2] , [6] , [7].
  325.   [2]  assumed_t(s,e)         assumed_t(s,e) :- [3] , [4] , [5].
  326.   [3]  assumed_t(s,b)            assumed_t(s,b).
  327.   [4]  assumed_t(s,b)            assumed_t(s,b).
  328.   [5]  assumed_t(p,b,i(b),e)            assumed_t(p,b,i(b),e).
  329.   [6]  assumed_t(s,b)         assumed_t(s,b).
  330.   [7]  assumed_t(p,e,i(b),i(b))         assumed_t(p,e,i(b),i(b)).
  331. Proof end.
  332. %                   succceeded(user:pttp_prove(chang_lee_example6, query)).
  333. %
  334. %          do_pttp_test(chang_lee_example7).
  335. %
  336.  
  337. chang_lee_example7:0  assumed_t(p,a).
  338. chang_lee_example7:1  assumed_t(m,a,s(c),s(b)).
  339. chang_lee_example7:2  assumed_t(m,A,A,s(A)).
  340. chang_lee_example7:3  not_proven_t(m,B,A,C);assumed_t(m,A,B,C).
  341. chang_lee_example7:4  not_proven_t(m,A,_,B);assumed_t(d,A,B).
  342. chang_lee_example7:5  not_proven_t(p,A);not_proven_t(m,C,D,B);not_proven_t(d,A,B);assumed_t(d,A,C);assumed_t(d,A,D).
  343. chang_lee_example7:6  query:-assumed_t(d,a,b).
  344. % 965 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 3446921 Lips)
  345.  
  346. Proof time: 0.00035827799999998966 seconds
  347. Proof:
  348. length = 6, depth = 2
  349. Goal#  Wff#  Wff Instance
  350. -----  ----  ------------
  351.   [0]  query   query :- [1].
  352.   [1]  assumed_t(d,a,b)      assumed_t(d,a,b) :- [2] , [3] , [4] , [6].
  353.   [2]  assumed_t(p,a)         assumed_t(p,a).
  354.   [3]  assumed_t(m,b,b,s(b))         assumed_t(m,b,b,s(b)).
  355.   [4]  assumed_t(d,a,s(b))         assumed_t(d,a,s(b)) :- [5].
  356.   [5]  assumed_t(m,a,s(c),s(b))            assumed_t(m,a,s(c),s(b)).
  357.   [6]  red         not_proven_t(d,a,b).
  358. Proof end.
  359. %                   succceeded(user:pttp_prove(chang_lee_example7, query)).
  360. %
  361. %          do_pttp_test(chang_lee_example8).
  362. %
  363.  
  364. chang_lee_example8:0  assumed_t(l,1,a).
  365. chang_lee_example8:1  assumed_t(d,A,A).
  366. chang_lee_example8:2  assumed_t(p,A);assumed_t(d,g(A),A).
  367. chang_lee_example8:3  assumed_t(p,A);assumed_t(l,1,g(A)).
  368. chang_lee_example8:4  assumed_t(p,A);assumed_t(l,g(A),A).
  369. chang_lee_example8:5  not_proven_t(p,A);not_proven_t(d,A,a).
  370. chang_lee_example8:6  not_proven_t(d,B,A);not_proven_t(d,A,C);assumed_t(d,B,C).
  371. chang_lee_example8:7  not_proven_t(l,1,A);not_proven_t(l,A,a);assumed_t(p,f(A)).
  372. chang_lee_example8:8  not_proven_t(l,1,A);not_proven_t(l,A,a);assumed_t(d,f(A),A).
  373. chang_lee_example8:9  query:-assumed_t(p,A),assumed_t(d,A,a).
  374. % 150,653 inferences, 0.022 CPU in 0.022 seconds (100% CPU, 6899058 Lips)
  375.  
  376. Proof time: 0.021924374999999774 seconds
  377. Proof:
  378. length = 13, depth = 6
  379. Goal#  Wff#  Wff Instance
  380. -----  ----  ------------
  381.   [0]  query   query :- [1] , [13].
  382.   [1]  assumed_t(p,a)      assumed_t(p,a) :- [2].
  383.   [2]  not_proven_t(l,1,g(a))         not_proven_t(l,1,g(a)) :- [3] , [5].
  384.   [3]  assumed_t(l,g(a),a)            assumed_t(l,g(a),a) :- [4].
  385.   [4]  red               not_proven_t(p,a).
  386.   [5]  not_proven_t(p,f(g(a)))            not_proven_t(p,f(g(a))) :- [6].
  387.   [6]  assumed_t(d,f(g(a)),a)               assumed_t(d,f(g(a)),a) :- [7] , [11].
  388.   [7]  assumed_t(d,f(g(a)),g(a))                  assumed_t(d,f(g(a)),g(a)) :- [8] , [9].
  389.   [8]  red                     assumed_t(l,1,g(a)).
  390.   [9]  assumed_t(l,g(a),a)                     assumed_t(l,g(a),a) :- [10].
  391.  [10]  red                        not_proven_t(p,a).
  392.  [11]  assumed_t(d,g(a),a)                  assumed_t(d,g(a),a) :- [12].
  393.  [12]  red                     not_proven_t(p,a).
  394.  [13]  assumed_t(d,a,a)      assumed_t(d,a,a).
  395. Proof end.
  396. %                   succceeded(user:pttp_prove(chang_lee_example8, query)).
  397. %
  398. %          do_pttp_test(chang_lee_example9).
  399. %
  400.  
  401. chang_lee_example9:0  assumed_t(l,A,f(A)).
  402. chang_lee_example9:1  not_proven_t(l,A,A).
  403. chang_lee_example9:2  not_proven_t(l,B,A);not_proven_t(l,A,B).
  404. chang_lee_example9:3  not_proven_t(d,B,f(A));assumed_t(l,A,B).
  405. chang_lee_example9:4  assumed_t(p,A);assumed_t(d,h(A),A).
  406. chang_lee_example9:5  assumed_t(p,A);assumed_t(p,h(A)).
  407. chang_lee_example9:6  assumed_t(p,A);assumed_t(l,h(A),A).
  408. chang_lee_example9:7  not_proven_t(p,A);not_proven_t(l,a,A);assumed_t(l,f(a),A).
  409. chang_lee_example9:8  query:-assumed_t(p,A),assumed_t(l,a,A),not_proven_t(l,f(a),A).
  410. % 25,770 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 6416254 Lips)
  411.  
  412. Proof time: 0.004109557999999902 seconds
  413. Proof:
  414. length = 10, depth = 5
  415. Goal#  Wff#  Wff Instance
  416. -----  ----  ------------
  417.   [0]  query   query :- [1] , [9] , [10].
  418.   [1]  assumed_t(p,f(a))      assumed_t(p,f(a)) :- [2].
  419.   [2]  not_proven_t(d,h(f(a)),f(a))         not_proven_t(d,h(f(a)),f(a)) :- [3].
  420.   [3]  not_proven_t(l,a,h(f(a)))            not_proven_t(l,a,h(f(a))) :- [4] , [6].
  421.   [4]  assumed_t(p,h(f(a)))               assumed_t(p,h(f(a))) :- [5].
  422.   [5]  red                  not_proven_t(p,f(a)).
  423.   [6]  not_proven_t(l,f(a),h(f(a)))               not_proven_t(l,f(a),h(f(a))) :- [7].
  424.   [7]  assumed_t(l,h(f(a)),f(a))                  assumed_t(l,h(f(a)),f(a)) :- [8].
  425.   [8]  red                     not_proven_t(p,f(a)).
  426.   [9]  assumed_t(l,a,f(a))      assumed_t(l,a,f(a)).
  427.  [10]  not_proven_t(l,f(a),f(a))      not_proven_t(l,f(a),f(a)).
  428. Proof end.
  429. %                   succceeded(user:pttp_prove(chang_lee_example9, query)).
  430. %
  431. %          do_pttp_test(logicmoo_example1).
  432. %
  433.  
  434. logicmoo_example1:0  assumed_t(mudMother,iJoe,iSue).
  435. logicmoo_example1:1  not_proven_t(mudMother,_,A);mudIsa(A,tFemale).
  436. logicmoo_example1:2  not_proven_t(mudChild,B,A);assumed_t(mudMother,A,B);assumed_t(mudFather,A,B).
  437. logicmoo_example1:3  query:-mudIsa(_,tFemale).
  438. % 162 inferences, 0.000 CPU in 0.000 seconds (101% CPU, 2209824 Lips)
  439.  
  440. Proof time: 0.00017492000000007835 seconds
  441. Proof:
  442. length = 2, depth = 1
  443. Goal#  Wff#  Wff Instance
  444. -----  ----  ------------
  445.   [0]  query   query :- [1].
  446.   [1]  mudIsa(iSue,tFemale)      mudIsa(iSue,tFemale) :- [2].
  447.   [2]  assumed_t(mudMother,iJoe,iSue)         assumed_t(mudMother,iJoe,iSue).
  448. Proof end.
  449. %                   succceeded(user:pttp_prove(logicmoo_example1, query)).
  450. %
  451. %          do_pttp_test(logicmoo_example1_holds).
  452. %
  453.  
  454. logicmoo_example1_holds:0  asserted_t(mudMother,iJoe,iSue).
  455. logicmoo_example1_holds:1  not_asserted_t(mudMother,_,A);mudIsa(A,tFemale).
  456. logicmoo_example1_holds:2  not_asserted_t(mudChild,B,A);proven_t(mudMother,A,B);proven_t(mudFather,A,B).
  457. logicmoo_example1_holds:3  query:-mudIsa(_,tFemale).
  458. % 192 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2662894 Lips)
  459.  
  460. Proof time: 0.00015124399999999483 seconds
  461. Proof:
  462. length = 2, depth = 1
  463. Goal#  Wff#  Wff Instance
  464. -----  ----  ------------
  465.   [0]  query   query :- [1].
  466.   [1]  mudIsa(iSue,tFemale)      mudIsa(iSue,tFemale) :- [2].
  467.   [2]  asserted_t(mudMother,iJoe,iSue)         asserted_t(mudMother,iJoe,iSue).
  468. Proof end.
  469. %                   succceeded(user:pttp_prove(logicmoo_example1_holds, query)).
  470. %
  471. %          do_pttp_test(logicmoo_example2).
  472. %
  473. %        pttp_load_wid(logicmoo_prules).
  474. %
  475. %                pttp_load_wid(logicmoo_kb_refution).
  476. %
  477.  
  478. logicmoo_kb_refution:0  not_asserted_t(A,B,C);proven_t(A,B,C).
  479. logicmoo_kb_refution:1  not_assumed_t(A,B,C);assumed_t(A,B,C).
  480. logicmoo_kb_refution:2  not_proven_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  481. logicmoo_kb_refution:3  not_assertable_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  482. logicmoo_kb_refution:4  not_both_t(proven_t(A,B,C),refuted_t(A,B,C));fallacy_t(A,B,C).
  483. logicmoo_kb_refution:5  not_assumed_t(A,B,C);not_refuted_t(A,B,C),assertable_t(A,B,C),answerable_t(A,B,C).
  484. logicmoo_kb_refution:6  not_refuted_t(A,B,C);not_assumed_t(A,B,C),not_assertable_t(A,B,C),answerable_t(A,B,C).
  485. logicmoo_kb_refution:7  not_askable_t(A,B,C);proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  486. logicmoo_kb_refution:8  not_unknowable_t(A,B,C),answerable_t(A,B,C);not_answerable_t(A,B,C),unknowable_t(A,B,C).
  487. logicmoo_kb_refution:9  askable_t(A,B,C),askable_t(A,B,C);not_askable_t(A,B,C),fallacy_t(A,B,C).
  488. logicmoo_kb_refution:10  not_answerable_t(A,B,C);proven_t(A,B,C);refuted_t(A,B,C).
  489. logicmoo_kb_refution:11  proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  490. logicmoo_prules:1  not_proven_t(mudMother,_,A);mudIsa(A,tFemale).
  491. logicmoo_prules:2  not_proven_t(mudChild,B,A);assumed_t(mudMother,A,B);assumed_t(mudFather,A,B).
  492. logicmoo_prules:3  not_asserted_t(mudMother,_,A);mudIsa(A,tFemale).
  493. logicmoo_prules:4  not_asserted_t(mudChild,B,A);proven_t(mudMother,A,B);proven_t(mudFather,A,B).
  494. logicmoo_example2:1  assumed_t(mudMother,iJoe,iSue).
  495. logicmoo_example2:2  asserted_t(mudChild,iGun,iSonOfGun).
  496. logicmoo_example2:3  not_mudIsa(iGun,tFemale).
  497. logicmoo_example2:4  query:-proven_t($VAR(?MUD-FATHER),iSonOfGun,iGun).
  498. % 306 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 3132454 Lips)
  499.  
  500. Proof time: 0.00019528199999996332 seconds
  501. Proof:
  502. length = 3, depth = 1
  503. Goal#  Wff#  Wff Instance
  504. -----  ----  ------------
  505.   [0]  query   query :- [1].
  506.   [1]  proven_t($VAR(?MUD-FATHER),iSonOfGun,iGun)      proven_t($VAR(?MUD-FATHER),iSonOfGun,iGun) :- [2] , [3].
  507.   [2]  red         not_unknowable_t($VAR(?MUD-FATHER),iSonOfGun,iGun).
  508.   [3]  red         not_refuted_t($VAR(?MUD-FATHER),iSonOfGun,iGun).
  509. Proof end.
  510. %                   succceeded(user:pttp_prove(logicmoo_example2, query)).
  511. %
  512. %          do_pttp_test(logicmoo_example22).
  513. %
  514. %        pttp_load_wid(logicmoo_prules).
  515. %
  516. %                pttp_load_wid(logicmoo_kb_refution).
  517. %
  518.  
  519. logicmoo_kb_refution:0  not_asserted_t(A,B,C);proven_t(A,B,C).
  520. logicmoo_kb_refution:1  not_assumed_t(A,B,C);assumed_t(A,B,C).
  521. logicmoo_kb_refution:2  not_proven_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  522. logicmoo_kb_refution:3  not_assertable_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  523. logicmoo_kb_refution:4  not_both_t(proven_t(A,B,C),refuted_t(A,B,C));fallacy_t(A,B,C).
  524. logicmoo_kb_refution:5  not_assumed_t(A,B,C);not_refuted_t(A,B,C),assertable_t(A,B,C),answerable_t(A,B,C).
  525. logicmoo_kb_refution:6  not_refuted_t(A,B,C);not_assumed_t(A,B,C),not_assertable_t(A,B,C),answerable_t(A,B,C).
  526. logicmoo_kb_refution:7  not_askable_t(A,B,C);proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  527. logicmoo_kb_refution:8  not_unknowable_t(A,B,C),answerable_t(A,B,C);not_answerable_t(A,B,C),unknowable_t(A,B,C).
  528. logicmoo_kb_refution:9  askable_t(A,B,C),askable_t(A,B,C);not_askable_t(A,B,C),fallacy_t(A,B,C).
  529. logicmoo_kb_refution:10  not_answerable_t(A,B,C);proven_t(A,B,C);refuted_t(A,B,C).
  530. logicmoo_kb_refution:11  proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  531. logicmoo_prules:1  not_proven_t(mudMother,_,A);mudIsa(A,tFemale).
  532. logicmoo_prules:2  not_proven_t(mudChild,B,A);assumed_t(mudMother,A,B);assumed_t(mudFather,A,B).
  533. logicmoo_prules:3  not_asserted_t(mudMother,_,A);mudIsa(A,tFemale).
  534. logicmoo_prules:4  not_asserted_t(mudChild,B,A);proven_t(mudMother,A,B);proven_t(mudFather,A,B).
  535. logicmoo_example22:1  asserted_t(mudChild,iGun,iSonOfGun).
  536. logicmoo_example22:2  not_mudIsa(iGun,tFemale).
  537. logicmoo_example22:3  query:-proven_t($VAR(?MUD-FATHER),iSonOfGun,iGun).
  538. % 306 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2783868 Lips)
  539.  
  540. Proof time: 0.00020974099999993 seconds
  541. Proof:
  542. length = 3, depth = 1
  543. Goal#  Wff#  Wff Instance
  544. -----  ----  ------------
  545.   [0]  query   query :- [1].
  546.   [1]  proven_t($VAR(?MUD-FATHER),iSonOfGun,iGun)      proven_t($VAR(?MUD-FATHER),iSonOfGun,iGun) :- [2] , [3].
  547.   [2]  red         not_unknowable_t($VAR(?MUD-FATHER),iSonOfGun,iGun).
  548.   [3]  red         not_refuted_t($VAR(?MUD-FATHER),iSonOfGun,iGun).
  549. Proof end.
  550. %                   succceeded(user:pttp_prove(logicmoo_example22, query)).
  551. %
  552. %          do_pttp_test(logicmoo_example3).
  553. %
  554. %        pttp_load_wid(logicmoo_kb_logic).
  555. %
  556. %                pttp_load_wid(logicmoo_kb_refution).
  557. %
  558.  
  559. logicmoo_kb_refution:0  not_asserted_t(A,B,C);proven_t(A,B,C).
  560. logicmoo_kb_refution:1  not_assumed_t(A,B,C);assumed_t(A,B,C).
  561. logicmoo_kb_refution:2  not_proven_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  562. logicmoo_kb_refution:3  not_assertable_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  563. logicmoo_kb_refution:4  not_both_t(proven_t(A,B,C),refuted_t(A,B,C));fallacy_t(A,B,C).
  564. logicmoo_kb_refution:5  not_assumed_t(A,B,C);not_refuted_t(A,B,C),assertable_t(A,B,C),answerable_t(A,B,C).
  565. logicmoo_kb_refution:6  not_refuted_t(A,B,C);not_assumed_t(A,B,C),not_assertable_t(A,B,C),answerable_t(A,B,C).
  566. logicmoo_kb_refution:7  not_askable_t(A,B,C);proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  567. logicmoo_kb_refution:8  not_unknowable_t(A,B,C),answerable_t(A,B,C);not_answerable_t(A,B,C),unknowable_t(A,B,C).
  568. logicmoo_kb_refution:9  askable_t(A,B,C),askable_t(A,B,C);not_askable_t(A,B,C),fallacy_t(A,B,C).
  569. logicmoo_kb_refution:10  not_answerable_t(A,B,C);proven_t(A,B,C);refuted_t(A,B,C).
  570. logicmoo_kb_refution:11  proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  571. logicmoo_kb_logic:1  not_both_t(pred_t(ptSubclass,A,B),pred_isa_t(A,C));pred_isa_t(B,C).
  572. logicmoo_kb_logic:2  not_both_t(pred_t(subClass,A,C),mudIsa(B,A));mudIsa(B,C).
  573. logicmoo_kb_logic:3  not_pred_t(disjointWith,A,B);pred_isa_t(A,C);pred_isa_t(B,C).
  574. logicmoo_kb_logic:4  not_pred_t(disjointWith,A,C);mudIsa(B,A);mudIsa(B,C).
  575. logicmoo_kb_logic:5  not_both_t(pred_t(genlPreds,A,B),proven_t(A,C,D));proven_t(B,C,D).
  576. logicmoo_kb_logic:6  not_both_t(pred_t(genlPreds,B,A),refuted_t(A,C,D));refuted_t(B,C,D).
  577. logicmoo_kb_logic:7  not_both_t(pred_t(genlInverse,A,B),proven_t(A,D,C));proven_t(B,C,D).
  578. logicmoo_kb_logic:8  not_both_t(pred_t(negationPreds,A,B),proven_t(A,C,D));refuted_t(B,C,D).
  579. logicmoo_kb_logic:9  not_both_t(pred_t(negationInverse,A,B),proven_t(A,D,C));refuted_t(B,C,D).
  580. logicmoo_kb_logic:10  not_both_t(pred_isa_t(predIrreflexive,A),proven_t(A,C,B));refuted_t(A,B,C).
  581. logicmoo_example3:1  pred_t(genlInverse,mudParent,mudChild).
  582. logicmoo_example3:2  pred_t(genlPreds,mudMother,mudParent).
  583. logicmoo_example3:3  pred_isa_t(predIrreflexive,mudChild).
  584. logicmoo_example3:4  asserted_t(mudParent,iSon1,iFather1).
  585. logicmoo_example3:5  query:-refuted_t(mudChild,iSon1,iFather1).
  586. % 248 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2901230 Lips)
  587.  
  588. Proof time: 0.0001702020000000637 seconds
  589. Proof:
  590. length = 3, depth = 1
  591. Goal#  Wff#  Wff Instance
  592. -----  ----  ------------
  593.   [0]  query   query :- [1].
  594.   [1]  refuted_t(mudChild,iSon1,iFather1)      refuted_t(mudChild,iSon1,iFather1) :- [2] , [3].
  595.   [2]  red         not_unknowable_t(mudChild,iSon1,iFather1).
  596.   [3]  red         not_assumed_t(mudChild,iSon1,iFather1).
  597. Proof end.
  598. %                   succceeded(user:pttp_prove(logicmoo_example3, query)).
  599. %
  600. %          do_pttp_test(logicmoo_example4).
  601. %
  602. %        pttp_load_wid(logicmoo_kb_logic).
  603. %
  604. %                pttp_load_wid(logicmoo_kb_refution).
  605. %
  606.  
  607. logicmoo_kb_refution:0  not_asserted_t(A,B,C);proven_t(A,B,C).
  608. logicmoo_kb_refution:1  not_assumed_t(A,B,C);assumed_t(A,B,C).
  609. logicmoo_kb_refution:2  not_proven_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  610. logicmoo_kb_refution:3  not_assertable_t(A,B,C);not_refuted_t(A,B,C),askable_t(A,B,C).
  611. logicmoo_kb_refution:4  not_both_t(proven_t(A,B,C),refuted_t(A,B,C));fallacy_t(A,B,C).
  612. logicmoo_kb_refution:5  not_assumed_t(A,B,C);not_refuted_t(A,B,C),assertable_t(A,B,C),answerable_t(A,B,C).
  613. logicmoo_kb_refution:6  not_refuted_t(A,B,C);not_assumed_t(A,B,C),not_assertable_t(A,B,C),answerable_t(A,B,C).
  614. logicmoo_kb_refution:7  not_askable_t(A,B,C);proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  615. logicmoo_kb_refution:8  not_unknowable_t(A,B,C),answerable_t(A,B,C);not_answerable_t(A,B,C),unknowable_t(A,B,C).
  616. logicmoo_kb_refution:9  askable_t(A,B,C),askable_t(A,B,C);not_askable_t(A,B,C),fallacy_t(A,B,C).
  617. logicmoo_kb_refution:10  not_answerable_t(A,B,C);proven_t(A,B,C);refuted_t(A,B,C).
  618. logicmoo_kb_refution:11  proven_t(A,B,C);unknowable_t(A,B,C);refuted_t(A,B,C).
  619. logicmoo_kb_logic:1  not_both_t(pred_t(ptSubclass,A,B),pred_isa_t(A,C));pred_isa_t(B,C).
  620. logicmoo_kb_logic:2  not_both_t(pred_t(subClass,A,C),mudIsa(B,A));mudIsa(B,C).
  621. logicmoo_kb_logic:3  not_pred_t(disjointWith,A,B);pred_isa_t(A,C);pred_isa_t(B,C).
  622. logicmoo_kb_logic:4  not_pred_t(disjointWith,A,C);mudIsa(B,A);mudIsa(B,C).
  623. logicmoo_kb_logic:5  not_both_t(pred_t(genlPreds,A,B),proven_t(A,C,D));proven_t(B,C,D).
  624. logicmoo_kb_logic:6  not_both_t(pred_t(genlPreds,B,A),refuted_t(A,C,D));refuted_t(B,C,D).
  625. logicmoo_kb_logic:7  not_both_t(pred_t(genlInverse,A,B),proven_t(A,D,C));proven_t(B,C,D).
  626. logicmoo_kb_logic:8  not_both_t(pred_t(negationPreds,A,B),proven_t(A,C,D));refuted_t(B,C,D).
  627. logicmoo_kb_logic:9  not_both_t(pred_t(negationInverse,A,B),proven_t(A,D,C));refuted_t(B,C,D).
  628. logicmoo_kb_logic:10  not_both_t(pred_isa_t(predIrreflexive,A),proven_t(A,C,B));refuted_t(A,B,C).
  629. logicmoo_example4:1  pred_t(genlInverse,mudParent,mudChild).
  630. logicmoo_example4:2  pred_t(genlPreds,mudMother,mudParent).
  631. logicmoo_example4:3  pred_isa_t(predIrreflexive,mudChild).
  632. logicmoo_example4:4  asserted_t(mudParent,iSon1,iFather1).
  633. logicmoo_example4:5  query:-not_assertable_t(mudChild,iSon1,iFather1).
  634. % 128 inferences, 0.000 CPU in 0.000 seconds (101% CPU, 2249679 Lips)
  635.  
  636. Proof time: 0.00014401899999993972 seconds
  637. Proof:
  638. length = 2, depth = 1
  639. Goal#  Wff#  Wff Instance
  640. -----  ----  ------------
  641.   [0]  query   query :- [1].
  642.   [1]  not_assertable_t(mudChild,iSon1,iFather1)      not_assertable_t(mudChild,iSon1,iFather1) :- [2].
  643.   [2]  red         refuted_t(mudChild,iSon1,iFather1).
  644. Proof end.
  645. %                   succceeded(user:pttp_prove(logicmoo_example4, query)).
  646. %
  647. :- dynamic pttp_test_took/3.
  648.  
  649. pttp_test_took(chang_lee_example1, success, 0.010726194999999938).
  650. pttp_test_took(chang_lee_example2, success, 0.02066049999999997).
  651. pttp_test_took(chang_lee_example3, success, 0.002530323000000001).
  652. pttp_test_took(chang_lee_example4, success, 0.002452107000000092).
  653. pttp_test_took(chang_lee_example5, success, 0.006329876999999984).
  654. pttp_test_took(chang_lee_example6, success, 0.0007582100000000924).
  655. pttp_test_took(chang_lee_example7, success, 0.0006418990000001124).
  656. pttp_test_took(chang_lee_example8, success, 0.022421823000000174).
  657. pttp_test_took(chang_lee_example9, success, 0.0045343890000000275).
  658. pttp_test_took(logicmoo_example1, success, 0.0005869039999999437).
  659. pttp_test_took(logicmoo_example1_holds, success, 0.0005333629999997314).
  660. pttp_test_took(logicmoo_example2, success, 0.000433665000000083).
  661. pttp_test_took(logicmoo_example22, success, 0.0004565119999999645).
  662. pttp_test_took(logicmoo_example3, success, 0.0006172200000000849).
  663. pttp_test_took(logicmoo_example4, success, 0.0003437410000000085).
  664.  
  665. Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.1.29-5-g0a3d88a-DIRTY)
  666. Copyright (c) 1990-2014 University of Amsterdam, VU Amsterdam
  667. SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
  668. and you are welcome to redistribute it under certain conditions.
  669. Please visit http://www.swi-prolog.org for details.
  670.  
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!