API tools faq
paste
Advertisement
logicmoo

% \+ if_startup_script(sanity:reexport(kif_sanity_tests)). %

logicmoo
Aug 2nd, 2017
273
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 38.46 KB | None | 0 0
raw download clone embed print report
  1. % \+ if_startup_script(sanity:reexport(kif_sanity_tests)).
  2. % autoloading listing_vars:append/3 from /usr/lib/swipl-7.5.10/library/lists
  3. % autoloading listing_vars:list_to_set/2 from /usr/lib/swipl-7.5.10/library/lists
  4. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:229
  5. % :- test_boxlog(=>(~fallacy_t(PROP_VAR), v(v(unknown_t(PROP_VAR), false_t(PROP_VAR)), true_t(PROP_VAR)))).
  6. % autoloading common_logic_snark:gensym/2 from /usr/lib/swipl-7.5.10/library/gensym
  7. % autoloading common_logic_snark:maplist/2 from /usr/lib/swipl-7.5.10/library/apply
  8. % autoloading common_logic_snark:append/3 from /usr/lib/swipl-7.5.10/library/lists
  9. % kif :-
  10. %       all(PROP,
  11. %           =>(~fallacy_t(PROP), v(v(unknown_t(PROP), false_t(PROP)), true_t(PROP)))).
  12. % qualify_nesc :-
  13. %       all(PROP,
  14. %           nesc(=>(~fallacy_t(PROP), v(v(unknown_t(PROP), false_t(PROP)), true_t(PROP))))).
  15. % autoloading common_logic_sanity:sub_term/2 from /usr/lib/swipl-7.5.10/library/occurs
  16. % autoloading common_logic_compiler:sub_term/2 from /usr/lib/swipl-7.5.10/library/occurs
  17. % nnf :-
  18. %       all(PROP,
  19. %           nesc(v(v(v(unknown_t(PROP), false_t(PROP)), true_t(PROP)), ~ (~fallacy_t(PROP))))).
  20. % unq :-
  21. %       nesc(v(v(v(unknown_t(PROP), false_t(PROP)), true_t(PROP)), ~ (~fallacy_t(PROP)))).
  22. % th_nnf_in :-
  23. %       (   (   (   unknown_t(PROP)
  24. %               ;   false_t(PROP)
  25. %               )
  26. %           ;   true_t(PROP)
  27. %           )
  28. %       ;   ~ (~fallacy_t(PROP))
  29. %       ).
  30. % th_nnf_out :-
  31. %       ~ (((n(unknown_t(PROP)), n(false_t(PROP))), n(true_t(PROP))), n(fallacy_t(PROP))).
  32. % autoloading snark_theorist:append/3 from /usr/lib/swipl-7.5.10/library/lists
  33. % autoloading common_logic_sanity:list_to_set/2 from /usr/lib/swipl-7.5.10/library/lists
  34. % autoloading mpred_type_wff:sub_term/2 from /usr/lib/swipl-7.5.10/library/occurs
  35. % autoloading common_logic_sanity:reverse/2 from /usr/lib/swipl-7.5.10/library/lists
  36. % autoloading dmsg:maplist/2 from /usr/lib/swipl-7.5.10/library/apply
  37. prove_unknown_t(PROP) :-
  38.         prove_not_false_t(PROP),
  39.         prove_not_true_t(PROP),
  40.         prove_not_fallacy_t(PROP).
  41. prove_false_t(PROP) :-
  42.         prove_not_unknown_t(PROP),
  43.         prove_not_true_t(PROP),
  44.         prove_not_fallacy_t(PROP).
  45. prove_true_t(PROP) :-
  46.         prove_not_unknown_t(PROP),
  47.         prove_not_false_t(PROP),
  48.         prove_not_fallacy_t(PROP).
  49. prove_fallacy_t(PROP) :-
  50.         prove_not_unknown_t(PROP),
  51.         prove_not_false_t(PROP),
  52.         prove_not_true_t(PROP).
  53. % autoloading common_logic_boxlog:sub_term/2 from /usr/lib/swipl-7.5.10/library/occurs
  54. % autoloading lockable_vars:maplist/2 from /usr/lib/swipl-7.5.10/library/apply
  55. pfc :-
  56.         prove_not_false_t(PROP), prove_not_true_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  57. pfc :-
  58.         prove_not_unknown_t(PROP), prove_not_true_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  59. pfc :-
  60.         prove_not_unknown_t(PROP), prove_not_false_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  61. pfc :-
  62.         prove_not_unknown_t(PROP), prove_not_false_t(PROP), prove_not_true_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  63. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:230
  64. % :- test_boxlog(=>(~unknown_t(PROP_VAR), v(true_t(PROP_VAR), false_t(PROP_VAR)))).
  65. % kif :-
  66. %       all(PROP, =>(~unknown_t(PROP), v(true_t(PROP), false_t(PROP)))).
  67. % qualify_nesc :-
  68. %       all(PROP, nesc(=>(~unknown_t(PROP), v(true_t(PROP), false_t(PROP))))).
  69. % nnf :-
  70. %       all(PROP, nesc(v(v(true_t(PROP), false_t(PROP)), ~ (~unknown_t(PROP))))).
  71. % unq :-
  72. %       nesc(v(v(true_t(PROP), false_t(PROP)), ~ (~unknown_t(PROP)))).
  73. % th_nnf_in :-
  74. %       (   (   true_t(PROP)
  75. %           ;   false_t(PROP)
  76. %           )
  77. %       ;   ~ (~unknown_t(PROP))
  78. %       ).
  79. % th_nnf_out :-
  80. %       ~ ((n(true_t(PROP)), n(false_t(PROP))), n(unknown_t(PROP))).
  81. prove_true_t(PROP) :-
  82.         prove_not_false_t(PROP),
  83.         prove_not_unknown_t(PROP).
  84. prove_false_t(PROP) :-
  85.         prove_not_true_t(PROP),
  86.         prove_not_unknown_t(PROP).
  87. prove_unknown_t(PROP) :-
  88.         prove_not_true_t(PROP),
  89.         prove_not_false_t(PROP).
  90. pfc :-
  91.         prove_not_false_t(PROP), prove_not_unknown_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  92. pfc :-
  93.         prove_not_true_t(PROP), prove_not_unknown_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  94. pfc :-
  95.         prove_not_true_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  96. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:231
  97. % :- test_boxlog(=>(~false_t(PROP_VAR), v(v(fallacy_t(PROP_VAR), unknown_t(PROP_VAR)), true_t(PROP_VAR)))).
  98. % kif :-
  99. %       all(PROP,
  100. %           =>(~false_t(PROP), v(v(fallacy_t(PROP), unknown_t(PROP)), true_t(PROP)))).
  101. % qualify_nesc :-
  102. %       all(PROP,
  103. %           nesc(=>(~false_t(PROP), v(v(fallacy_t(PROP), unknown_t(PROP)), true_t(PROP))))).
  104. % nnf :-
  105. %       all(PROP,
  106. %           nesc(v(v(v(fallacy_t(PROP), unknown_t(PROP)), true_t(PROP)), ~ (~false_t(PROP))))).
  107. % unq :-
  108. %       nesc(v(v(v(fallacy_t(PROP), unknown_t(PROP)), true_t(PROP)), ~ (~false_t(PROP)))).
  109. % th_nnf_in :-
  110. %       (   (   (   fallacy_t(PROP)
  111. %               ;   unknown_t(PROP)
  112. %               )
  113. %           ;   true_t(PROP)
  114. %           )
  115. %       ;   ~ (~false_t(PROP))
  116. %       ).
  117. % th_nnf_out :-
  118. %       ~ (((n(fallacy_t(PROP)), n(unknown_t(PROP))), n(true_t(PROP))), n(false_t(PROP))).
  119. prove_fallacy_t(PROP) :-
  120.         prove_not_unknown_t(PROP),
  121.         prove_not_true_t(PROP),
  122.         prove_not_false_t(PROP).
  123. prove_unknown_t(PROP) :-
  124.         prove_not_fallacy_t(PROP),
  125.         prove_not_true_t(PROP),
  126.         prove_not_false_t(PROP).
  127. prove_true_t(PROP) :-
  128.         prove_not_fallacy_t(PROP),
  129.         prove_not_unknown_t(PROP),
  130.         prove_not_false_t(PROP).
  131. prove_false_t(PROP) :-
  132.         prove_not_fallacy_t(PROP),
  133.         prove_not_unknown_t(PROP),
  134.         prove_not_true_t(PROP).
  135. pfc :-
  136.         prove_not_unknown_t(PROP), prove_not_true_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  137. pfc :-
  138.         prove_not_fallacy_t(PROP), prove_not_true_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  139. pfc :-
  140.         prove_not_fallacy_t(PROP), prove_not_unknown_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  141. pfc :-
  142.         prove_not_fallacy_t(PROP), prove_not_unknown_t(PROP), prove_not_true_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  143. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:232
  144. % :- test_boxlog(<=>(answerable_t(PROP_VAR), &(askable_t(PROP_VAR), ~unknown_t(PROP_VAR)))).
  145. % kif :-
  146. %       all(PROP, <=>(answerable_t(PROP), &(askable_t(PROP), ~unknown_t(PROP)))).
  147. % qualify_nesc :-
  148. %       all(PROP,
  149. %           nesc(<=>(answerable_t(PROP), &(askable_t(PROP), ~unknown_t(PROP))))).
  150. % nnf :-
  151. %       all(PROP,
  152. %           &(&(nesc(v(askable_t(PROP), ~answerable_t(PROP))), nesc(v(~unknown_t(PROP), ~answerable_t(PROP)))), nesc(v(answerable_t(PROP), ~ &(askable_t(PROP), ~unknown_t(PROP)))))).
  153. % unq :-
  154. %       &(&(nesc(v(askable_t(PROP), ~answerable_t(PROP))), nesc(v(~unknown_t(PROP), ~answerable_t(PROP)))), nesc(v(answerable_t(PROP), ~ &(askable_t(PROP), ~unknown_t(PROP))))).
  155. % th_nnf_in :-
  156. %       ( (   askable_t(PROP)
  157. %         ;   ~answerable_t(PROP)
  158. %         ),
  159. %         (   ~unknown_t(PROP)
  160. %         ;   ~answerable_t(PROP)
  161. %         )
  162. %       ),
  163. %       (   answerable_t(PROP)
  164. %       ;   ~ (askable_t(PROP), ~unknown_t(PROP))
  165. %       ).
  166. % th_nnf_out :-
  167. %       ~ ((n(askable_t(PROP)), answerable_t(PROP);unknown_t(PROP), answerable_t(PROP));n(answerable_t(PROP)), askable_t(PROP), n(unknown_t(PROP))).
  168. prove_askable_t(PROP) :-
  169.         prove_answerable_t(PROP).
  170. prove_not_answerable_t(PROP) :-
  171.         prove_not_askable_t(PROP).
  172. prove_not_unknown_t(PROP) :-
  173.         prove_answerable_t(PROP).
  174. prove_not_answerable_t(PROP) :-
  175.         prove_unknown_t(PROP).
  176. prove_answerable_t(PROP) :-
  177.         prove_askable_t(PROP),
  178.         prove_not_unknown_t(PROP).
  179. prove_not_askable_t(PROP) :-
  180.         prove_not_unknown_t(PROP),
  181.         prove_not_answerable_t(PROP).
  182. prove_unknown_t(PROP) :-
  183.         prove_askable_t(PROP),
  184.         prove_not_answerable_t(PROP).
  185. pfc :-
  186.         prove_answerable_t(PROP), {is_unit(PROP)}==>prove_askable_t(PROP).
  187. pfc :-
  188.         prove_not_askable_t(PROP), {is_unit(PROP)}==>prove_not_answerable_t(PROP).
  189. pfc :-
  190.         prove_answerable_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  191. pfc :-
  192.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_answerable_t(PROP).
  193. pfc :-
  194.         prove_askable_t(PROP), prove_not_unknown_t(PROP), {is_unit(PROP)}==>prove_answerable_t(PROP).
  195. pfc :-
  196.         prove_not_unknown_t(PROP), prove_not_answerable_t(PROP), {is_unit(PROP)}==>prove_not_askable_t(PROP).
  197. pfc :-
  198.         prove_askable_t(PROP), prove_not_answerable_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  199. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:233
  200. % :- test_boxlog(=>(answerable_t(PROP_VAR), v(true_t(PROP_VAR), false_t(PROP_VAR)))).
  201. % kif :-
  202. %       all(PROP, =>(answerable_t(PROP), v(true_t(PROP), false_t(PROP)))).
  203. % qualify_nesc :-
  204. %       all(PROP, nesc(=>(answerable_t(PROP), v(true_t(PROP), false_t(PROP))))).
  205. % nnf :-
  206. %       all(PROP, nesc(v(v(true_t(PROP), false_t(PROP)), ~answerable_t(PROP)))).
  207. % unq :-
  208. %       nesc(v(v(true_t(PROP), false_t(PROP)), ~answerable_t(PROP))).
  209. % th_nnf_in :-
  210. %       (   (   true_t(PROP)
  211. %           ;   false_t(PROP)
  212. %           )
  213. %       ;   ~answerable_t(PROP)
  214. %       ).
  215. % th_nnf_out :-
  216. %       ~ ((n(true_t(PROP)), n(false_t(PROP))), answerable_t(PROP)).
  217. prove_true_t(PROP) :-
  218.         prove_not_false_t(PROP),
  219.         prove_answerable_t(PROP).
  220. prove_false_t(PROP) :-
  221.         prove_not_true_t(PROP),
  222.         prove_answerable_t(PROP).
  223. prove_not_answerable_t(PROP) :-
  224.         prove_not_true_t(PROP),
  225.         prove_not_false_t(PROP).
  226. pfc :-
  227.         prove_not_false_t(PROP), prove_answerable_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  228. pfc :-
  229.         prove_not_true_t(PROP), prove_answerable_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  230. pfc :-
  231.         prove_not_true_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_not_answerable_t(PROP).
  232. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:234
  233. % :- test_boxlog(<=>(askable_t(PROP_VAR), ~fallacy_t(PROP_VAR))).
  234. % kif :-
  235. %       all(PROP, <=>(askable_t(PROP), ~fallacy_t(PROP))).
  236. % qualify_nesc :-
  237. %       all(PROP, nesc(<=>(askable_t(PROP), ~fallacy_t(PROP)))).
  238. % nnf :-
  239. %       all(PROP,
  240. %           &(nesc(v(askable_t(PROP), ~ (~fallacy_t(PROP)))), nesc(v(~askable_t(PROP), ~fallacy_t(PROP))))).
  241. % unq :-
  242. %       &(nesc(v(askable_t(PROP), ~ (~fallacy_t(PROP)))), nesc(v(~askable_t(PROP), ~fallacy_t(PROP)))).
  243. % th_nnf_in :-
  244. %       (   askable_t(PROP)
  245. %       ;   ~ (~fallacy_t(PROP))
  246. %       ),
  247. %       (   ~askable_t(PROP)
  248. %       ;   ~fallacy_t(PROP)
  249. %       ).
  250. % th_nnf_out :-
  251. %       ~ (n(askable_t(PROP)), n(fallacy_t(PROP));askable_t(PROP), fallacy_t(PROP)).
  252. prove_askable_t(PROP) :-
  253.         prove_not_fallacy_t(PROP).
  254. prove_fallacy_t(PROP) :-
  255.         prove_not_askable_t(PROP).
  256. prove_not_askable_t(PROP) :-
  257.         prove_fallacy_t(PROP).
  258. prove_not_fallacy_t(PROP) :-
  259.         prove_askable_t(PROP).
  260. pfc :-
  261.         prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_askable_t(PROP).
  262. pfc :-
  263.         prove_not_askable_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  264. pfc :-
  265.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_askable_t(PROP).
  266. pfc :-
  267.         prove_askable_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  268. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:235
  269. % :- test_boxlog(=>(askable_t(PROP_VAR), v(v(true_t(PROP_VAR), unknown_t(PROP_VAR)), false_t(PROP_VAR)))).
  270. % kif :-
  271. %       all(PROP,
  272. %           =>(askable_t(PROP), v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP)))).
  273. % qualify_nesc :-
  274. %       all(PROP,
  275. %           nesc(=>(askable_t(PROP), v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP))))).
  276. % nnf :-
  277. %       all(PROP,
  278. %           nesc(v(v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP)), ~askable_t(PROP)))).
  279. % unq :-
  280. %       nesc(v(v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP)), ~askable_t(PROP))).
  281. % th_nnf_in :-
  282. %       (   (   (   true_t(PROP)
  283. %               ;   unknown_t(PROP)
  284. %               )
  285. %           ;   false_t(PROP)
  286. %           )
  287. %       ;   ~askable_t(PROP)
  288. %       ).
  289. % th_nnf_out :-
  290. %       ~ (((n(true_t(PROP)), n(unknown_t(PROP))), n(false_t(PROP))), askable_t(PROP)).
  291. prove_true_t(PROP) :-
  292.         prove_not_unknown_t(PROP),
  293.         prove_not_false_t(PROP),
  294.         prove_askable_t(PROP).
  295. prove_unknown_t(PROP) :-
  296.         prove_not_true_t(PROP),
  297.         prove_not_false_t(PROP),
  298.         prove_askable_t(PROP).
  299. prove_false_t(PROP) :-
  300.         prove_not_true_t(PROP),
  301.         prove_not_unknown_t(PROP),
  302.         prove_askable_t(PROP).
  303. prove_not_askable_t(PROP) :-
  304.         prove_not_true_t(PROP),
  305.         prove_not_unknown_t(PROP),
  306.         prove_not_false_t(PROP).
  307. pfc :-
  308.         prove_not_unknown_t(PROP), prove_not_false_t(PROP), prove_askable_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  309. pfc :-
  310.         prove_not_true_t(PROP), prove_not_false_t(PROP), prove_askable_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  311. pfc :-
  312.         prove_not_true_t(PROP), prove_not_unknown_t(PROP), prove_askable_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  313. pfc :-
  314.         prove_not_true_t(PROP), prove_not_unknown_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_not_askable_t(PROP).
  315. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:236
  316. % :- test_boxlog(v(askable_t(PROP_VAR), fallacy_t(PROP_VAR))).
  317. % kif :-
  318. %       all(PROP, v(askable_t(PROP), fallacy_t(PROP))).
  319. % qualify_nesc :-
  320. %       all(PROP, nesc(v(askable_t(PROP), fallacy_t(PROP)))).
  321. % nnf :-
  322. %       all(PROP, nesc(v(askable_t(PROP), fallacy_t(PROP)))).
  323. % unq :-
  324. %       nesc(v(askable_t(PROP), fallacy_t(PROP))).
  325. % th_nnf_in :-
  326. %       (   askable_t(PROP)
  327. %       ;   fallacy_t(PROP)
  328. %       ).
  329. % th_nnf_out :-
  330. %       ~ (n(askable_t(PROP)), n(fallacy_t(PROP))).
  331. prove_askable_t(PROP) :-
  332.         prove_not_fallacy_t(PROP).
  333. prove_fallacy_t(PROP) :-
  334.         prove_not_askable_t(PROP).
  335. pfc :-
  336.         prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_askable_t(PROP).
  337. pfc :-
  338.         prove_not_askable_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  339. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:237
  340. % :- test_boxlog(=>(asserted_t(PROP_VAR), true_t(PROP_VAR))).
  341. % kif :-
  342. %       all(PROP, =>(asserted_t(PROP), true_t(PROP))).
  343. % qualify_nesc :-
  344. %       all(PROP, nesc(=>(asserted_t(PROP), true_t(PROP)))).
  345. % nnf :-
  346. %       all(PROP, nesc(v(true_t(PROP), ~asserted_t(PROP)))).
  347. % unq :-
  348. %       nesc(v(true_t(PROP), ~asserted_t(PROP))).
  349. % th_nnf_in :-
  350. %       (   true_t(PROP)
  351. %       ;   ~asserted_t(PROP)
  352. %       ).
  353. % th_nnf_out :-
  354. %       ~ (n(true_t(PROP)), asserted_t(PROP)).
  355. prove_true_t(PROP) :-
  356.         prove_asserted_t(PROP).
  357. prove_not_asserted_t(PROP) :-
  358.         prove_not_true_t(PROP).
  359. pfc :-
  360.         prove_asserted_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  361. pfc :-
  362.         prove_not_true_t(PROP), {is_unit(PROP)}==>prove_not_asserted_t(PROP).
  363. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:238
  364. % :- test_boxlog(=>(fallacy_t(PROP_VAR), &(&(&(false_t(PROP_VAR), true_t(PROP_VAR)), ~unknown_t(PROP_VAR)), ~possible_t(PROP_VAR)))).
  365. % kif :-
  366. %       all(PROP,
  367. %           =>(fallacy_t(PROP), &(&(&(false_t(PROP), true_t(PROP)), ~unknown_t(PROP)), ~possible_t(PROP)))).
  368. % qualify_nesc :-
  369. %       all(PROP,
  370. %           nesc(=>(fallacy_t(PROP), &(&(&(false_t(PROP), true_t(PROP)), ~unknown_t(PROP)), ~possible_t(PROP))))).
  371. % nnf :-
  372. %       all(PROP,
  373. %           &(&(&(nesc(v(false_t(PROP), ~fallacy_t(PROP))), nesc(v(true_t(PROP), ~fallacy_t(PROP)))), nesc(v(~unknown_t(PROP), ~fallacy_t(PROP)))), nesc(v(~possible_t(PROP), ~fallacy_t(PROP))))).
  374. % unq :-
  375. %       &(&(&(nesc(v(false_t(PROP), ~fallacy_t(PROP))), nesc(v(true_t(PROP), ~fallacy_t(PROP)))), nesc(v(~unknown_t(PROP), ~fallacy_t(PROP)))), nesc(v(~possible_t(PROP), ~fallacy_t(PROP)))).
  376. % th_nnf_in :-
  377. %       ( ( (   false_t(PROP)
  378. %           ;   ~fallacy_t(PROP)
  379. %           ),
  380. %           (   true_t(PROP)
  381. %           ;   ~fallacy_t(PROP)
  382. %           )
  383. %         ),
  384. %         (   ~unknown_t(PROP)
  385. %         ;   ~fallacy_t(PROP)
  386. %         )
  387. %       ),
  388. %       (   ~possible_t(PROP)
  389. %       ;   ~fallacy_t(PROP)
  390. %       ).
  391. % th_nnf_out :-
  392. %       ~ (((n(false_t(PROP)), fallacy_t(PROP);n(true_t(PROP)), fallacy_t(PROP));unknown_t(PROP), fallacy_t(PROP));possible_t(PROP), fallacy_t(PROP)).
  393. prove_false_t(PROP) :-
  394.         prove_fallacy_t(PROP).
  395. prove_not_fallacy_t(PROP) :-
  396.         prove_not_false_t(PROP).
  397. prove_true_t(PROP) :-
  398.         prove_fallacy_t(PROP).
  399. prove_not_fallacy_t(PROP) :-
  400.         prove_not_true_t(PROP).
  401. prove_not_unknown_t(PROP) :-
  402.         prove_fallacy_t(PROP).
  403. prove_not_fallacy_t(PROP) :-
  404.         prove_unknown_t(PROP).
  405. prove_not_possible_t(PROP) :-
  406.         prove_fallacy_t(PROP).
  407. prove_not_fallacy_t(PROP) :-
  408.         prove_possible_t(PROP).
  409. pfc :-
  410.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  411. pfc :-
  412.         prove_not_false_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  413. pfc :-
  414.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  415. pfc :-
  416.         prove_not_true_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  417. pfc :-
  418.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  419. pfc :-
  420.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  421. pfc :-
  422.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_possible_t(PROP).
  423. pfc :-
  424.         prove_possible_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  425. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:239
  426. % :- test_boxlog(=>(&(true_t(PROP_VAR), false_t(PROP_VAR)), fallacy_t(PROP_VAR))).
  427. % kif :-
  428. %       all(PROP, =>(&(true_t(PROP), false_t(PROP)), fallacy_t(PROP))).
  429. % qualify_nesc :-
  430. %       all(PROP, nesc(=>(&(true_t(PROP), false_t(PROP)), fallacy_t(PROP)))).
  431. % nnf :-
  432. %       all(PROP, nesc(v(fallacy_t(PROP), ~ &(true_t(PROP), false_t(PROP))))).
  433. % unq :-
  434. %       nesc(v(fallacy_t(PROP), ~ &(true_t(PROP), false_t(PROP)))).
  435. % th_nnf_in :-
  436. %       (   fallacy_t(PROP)
  437. %       ;   ~ (true_t(PROP), false_t(PROP))
  438. %       ).
  439. % th_nnf_out :-
  440. %       ~ (n(fallacy_t(PROP)), true_t(PROP), false_t(PROP)).
  441. prove_fallacy_t(PROP) :-
  442.         prove_true_t(PROP),
  443.         prove_false_t(PROP).
  444. prove_not_true_t(PROP) :-
  445.         prove_false_t(PROP),
  446.         prove_not_fallacy_t(PROP).
  447. prove_not_false_t(PROP) :-
  448.         prove_true_t(PROP),
  449.         prove_not_fallacy_t(PROP).
  450. pfc :-
  451.         prove_true_t(PROP), prove_false_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  452. pfc :-
  453.         prove_false_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  454. pfc :-
  455.         prove_true_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  456. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:240
  457. % :- test_boxlog(v(v(true_t(PROP_VAR), unknown_t(PROP_VAR)), false_t(PROP_VAR))).
  458. % kif :-
  459. %       all(PROP, v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP))).
  460. % qualify_nesc :-
  461. %       all(PROP, nesc(v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP)))).
  462. % nnf :-
  463. %       all(PROP, nesc(v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP)))).
  464. % unq :-
  465. %       nesc(v(v(true_t(PROP), unknown_t(PROP)), false_t(PROP))).
  466. % th_nnf_in :-
  467. %       (   (   true_t(PROP)
  468. %           ;   unknown_t(PROP)
  469. %           )
  470. %       ;   false_t(PROP)
  471. %       ).
  472. % th_nnf_out :-
  473. %       ~ ((n(true_t(PROP)), n(unknown_t(PROP))), n(false_t(PROP))).
  474. prove_true_t(PROP) :-
  475.         prove_not_unknown_t(PROP),
  476.         prove_not_false_t(PROP).
  477. prove_unknown_t(PROP) :-
  478.         prove_not_true_t(PROP),
  479.         prove_not_false_t(PROP).
  480. prove_false_t(PROP) :-
  481.         prove_not_true_t(PROP),
  482.         prove_not_unknown_t(PROP).
  483. pfc :-
  484.         prove_not_unknown_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  485. pfc :-
  486.         prove_not_true_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  487. pfc :-
  488.         prove_not_true_t(PROP), prove_not_unknown_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  489. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:242
  490. % :- test_boxlog(=>(true_t(PROP_VAR), possible_t(PROP_VAR))).
  491. % kif :-
  492. %       all(PROP, =>(true_t(PROP), possible_t(PROP))).
  493. % qualify_nesc :-
  494. %       all(PROP, nesc(=>(true_t(PROP), possible_t(PROP)))).
  495. % nnf :-
  496. %       all(PROP, nesc(v(possible_t(PROP), ~true_t(PROP)))).
  497. % unq :-
  498. %       nesc(v(possible_t(PROP), ~true_t(PROP))).
  499. % th_nnf_in :-
  500. %       (   possible_t(PROP)
  501. %       ;   ~true_t(PROP)
  502. %       ).
  503. % th_nnf_out :-
  504. %       ~ (n(possible_t(PROP)), true_t(PROP)).
  505. prove_possible_t(PROP) :-
  506.         prove_true_t(PROP).
  507. prove_not_true_t(PROP) :-
  508.         prove_not_possible_t(PROP).
  509. pfc :-
  510.         prove_true_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  511. pfc :-
  512.         prove_not_possible_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  513. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:243
  514. % :- test_boxlog(=>(possible_t(PROP_VAR), &(~false_t(PROP_VAR), ~fallacy_t(PROP_VAR)))).
  515. % kif :-
  516. %       all(PROP, =>(possible_t(PROP), &(~false_t(PROP), ~fallacy_t(PROP)))).
  517. % qualify_nesc :-
  518. %       all(PROP,
  519. %           nesc(=>(possible_t(PROP), &(~false_t(PROP), ~fallacy_t(PROP))))).
  520. % nnf :-
  521. %       all(PROP,
  522. %           &(nesc(v(~possible_t(PROP), ~false_t(PROP))), nesc(v(~possible_t(PROP), ~fallacy_t(PROP))))).
  523. % unq :-
  524. %       &(nesc(v(~possible_t(PROP), ~false_t(PROP))), nesc(v(~possible_t(PROP), ~fallacy_t(PROP)))).
  525. % th_nnf_in :-
  526. %       (   ~possible_t(PROP)
  527. %       ;   ~false_t(PROP)
  528. %       ),
  529. %       (   ~possible_t(PROP)
  530. %       ;   ~fallacy_t(PROP)
  531. %       ).
  532. % th_nnf_out :-
  533. %       ~ (possible_t(PROP), false_t(PROP);possible_t(PROP), fallacy_t(PROP)).
  534. prove_not_possible_t(PROP) :-
  535.         prove_false_t(PROP).
  536. prove_not_false_t(PROP) :-
  537.         prove_possible_t(PROP).
  538. prove_not_possible_t(PROP) :-
  539.         prove_fallacy_t(PROP).
  540. prove_not_fallacy_t(PROP) :-
  541.         prove_possible_t(PROP).
  542. pfc :-
  543.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_possible_t(PROP).
  544. pfc :-
  545.         prove_possible_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  546. pfc :-
  547.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_possible_t(PROP).
  548. pfc :-
  549.         prove_possible_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  550. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:245
  551. % :- test_boxlog(=>(~true_t(PROP_VAR), v(v(false_t(PROP_VAR), fallacy_t(PROP_VAR)), possible_t(PROP_VAR)))).
  552. % kif :-
  553. %       all(PROP,
  554. %           =>(~true_t(PROP), v(v(false_t(PROP), fallacy_t(PROP)), possible_t(PROP)))).
  555. % qualify_nesc :-
  556. %       all(PROP,
  557. %           nesc(=>(~true_t(PROP), v(v(false_t(PROP), fallacy_t(PROP)), possible_t(PROP))))).
  558. % nnf :-
  559. %       all(PROP,
  560. %           nesc(v(v(v(false_t(PROP), fallacy_t(PROP)), possible_t(PROP)), ~ (~true_t(PROP))))).
  561. % unq :-
  562. %       nesc(v(v(v(false_t(PROP), fallacy_t(PROP)), possible_t(PROP)), ~ (~true_t(PROP)))).
  563. % th_nnf_in :-
  564. %       (   (   (   false_t(PROP)
  565. %               ;   fallacy_t(PROP)
  566. %               )
  567. %           ;   possible_t(PROP)
  568. %           )
  569. %       ;   ~ (~true_t(PROP))
  570. %       ).
  571. % th_nnf_out :-
  572. %       ~ (((n(false_t(PROP)), n(fallacy_t(PROP))), n(possible_t(PROP))), n(true_t(PROP))).
  573. prove_false_t(PROP) :-
  574.         prove_not_fallacy_t(PROP),
  575.         prove_not_possible_t(PROP),
  576.         prove_not_true_t(PROP).
  577. prove_fallacy_t(PROP) :-
  578.         prove_not_false_t(PROP),
  579.         prove_not_possible_t(PROP),
  580.         prove_not_true_t(PROP).
  581. prove_possible_t(PROP) :-
  582.         prove_not_false_t(PROP),
  583.         prove_not_fallacy_t(PROP),
  584.         prove_not_true_t(PROP).
  585. prove_true_t(PROP) :-
  586.         prove_not_false_t(PROP),
  587.         prove_not_fallacy_t(PROP),
  588.         prove_not_possible_t(PROP).
  589. pfc :-
  590.         prove_not_fallacy_t(PROP), prove_not_possible_t(PROP), prove_not_true_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  591. pfc :-
  592.         prove_not_false_t(PROP), prove_not_possible_t(PROP), prove_not_true_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  593. pfc :-
  594.         prove_not_false_t(PROP), prove_not_fallacy_t(PROP), prove_not_true_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  595. pfc :-
  596.         prove_not_false_t(PROP), prove_not_fallacy_t(PROP), prove_not_possible_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  597. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:246
  598. % :- test_boxlog(<=>(false_t(PROP_VAR), &(&(~true_t(PROP_VAR), ~possible_t(PROP_VAR)), ~unknown_t(PROP_VAR)))).
  599. % kif :-
  600. %       all(PROP,
  601. %           <=>(false_t(PROP), &(&(~true_t(PROP), ~possible_t(PROP)), ~unknown_t(PROP)))).
  602. % qualify_nesc :-
  603. %       all(PROP,
  604. %           nesc(<=>(false_t(PROP), &(&(~true_t(PROP), ~possible_t(PROP)), ~unknown_t(PROP))))).
  605. % nnf :-
  606. %       all(PROP,
  607. %           &(nesc(v(false_t(PROP), ~ &(&(~true_t(PROP), ~possible_t(PROP)), ~unknown_t(PROP)))), &(&(nesc(v(~false_t(PROP), ~true_t(PROP))), nesc(v(~false_t(PROP), ~possible_t(PROP)))), nesc(v(~false_t(PROP), ~unknown_t(PROP)))))).
  608. % unq :-
  609. %       &(nesc(v(false_t(PROP), ~ &(&(~true_t(PROP), ~possible_t(PROP)), ~unknown_t(PROP)))), &(&(nesc(v(~false_t(PROP), ~true_t(PROP))), nesc(v(~false_t(PROP), ~possible_t(PROP)))), nesc(v(~false_t(PROP), ~unknown_t(PROP))))).
  610. % th_nnf_in :-
  611. %       (   false_t(PROP)
  612. %       ;   ~ ((~true_t(PROP), ~possible_t(PROP)), ~unknown_t(PROP))
  613. %       ),
  614. %       ( (   ~false_t(PROP)
  615. %         ;   ~true_t(PROP)
  616. %         ),
  617. %         (   ~false_t(PROP)
  618. %         ;   ~possible_t(PROP)
  619. %         )
  620. %       ),
  621. %       (   ~false_t(PROP)
  622. %       ;   ~unknown_t(PROP)
  623. %       ).
  624. % th_nnf_out :-
  625. %       ~ (n(false_t(PROP)), (n(true_t(PROP)), n(possible_t(PROP))), n(unknown_t(PROP));(false_t(PROP), true_t(PROP);false_t(PROP), possible_t(PROP));false_t(PROP), unknown_t(PROP)).
  626. prove_false_t(PROP) :-
  627.         prove_not_true_t(PROP),
  628.         prove_not_possible_t(PROP),
  629.         prove_not_unknown_t(PROP).
  630. prove_true_t(PROP) :-
  631.         prove_not_possible_t(PROP),
  632.         prove_not_unknown_t(PROP),
  633.         prove_not_false_t(PROP).
  634. prove_possible_t(PROP) :-
  635.         prove_not_true_t(PROP),
  636.         prove_not_unknown_t(PROP),
  637.         prove_not_false_t(PROP).
  638. prove_unknown_t(PROP) :-
  639.         prove_not_true_t(PROP),
  640.         prove_not_possible_t(PROP),
  641.         prove_not_false_t(PROP).
  642. prove_not_false_t(PROP) :-
  643.         prove_true_t(PROP).
  644. prove_not_true_t(PROP) :-
  645.         prove_false_t(PROP).
  646. prove_not_false_t(PROP) :-
  647.         prove_possible_t(PROP).
  648. prove_not_possible_t(PROP) :-
  649.         prove_false_t(PROP).
  650. prove_not_false_t(PROP) :-
  651.         prove_unknown_t(PROP).
  652. prove_not_unknown_t(PROP) :-
  653.         prove_false_t(PROP).
  654. pfc :-
  655.         prove_not_true_t(PROP), prove_not_possible_t(PROP), prove_not_unknown_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  656. pfc :-
  657.         prove_not_possible_t(PROP), prove_not_unknown_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_true_t(PROP).
  658. pfc :-
  659.         prove_not_true_t(PROP), prove_not_unknown_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  660. pfc :-
  661.         prove_not_true_t(PROP), prove_not_possible_t(PROP), prove_not_false_t(PROP), {is_unit(PROP)}==>prove_unknown_t(PROP).
  662. pfc :-
  663.         prove_true_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  664. pfc :-
  665.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  666. pfc :-
  667.         prove_possible_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  668. pfc :-
  669.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_possible_t(PROP).
  670. pfc :-
  671.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  672. pfc :-
  673.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  674. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:247
  675. % :- test_boxlog(=>(true_t(PROP_VAR), &(&(~false_t(PROP_VAR), possible_t(PROP_VAR)), ~unknown_t(PROP_VAR)))).
  676. % kif :-
  677. %       all(PROP,
  678. %           =>(true_t(PROP), &(&(~false_t(PROP), possible_t(PROP)), ~unknown_t(PROP)))).
  679. % qualify_nesc :-
  680. %       all(PROP,
  681. %           nesc(=>(true_t(PROP), &(&(~false_t(PROP), possible_t(PROP)), ~unknown_t(PROP))))).
  682. % nnf :-
  683. %       all(PROP,
  684. %           &(&(nesc(v(possible_t(PROP), ~true_t(PROP))), nesc(v(~false_t(PROP), ~true_t(PROP)))), nesc(v(~unknown_t(PROP), ~true_t(PROP))))).
  685. % unq :-
  686. %       &(&(nesc(v(possible_t(PROP), ~true_t(PROP))), nesc(v(~false_t(PROP), ~true_t(PROP)))), nesc(v(~unknown_t(PROP), ~true_t(PROP)))).
  687. % th_nnf_in :-
  688. %       ( (   possible_t(PROP)
  689. %         ;   ~true_t(PROP)
  690. %         ),
  691. %         (   ~false_t(PROP)
  692. %         ;   ~true_t(PROP)
  693. %         )
  694. %       ),
  695. %       (   ~unknown_t(PROP)
  696. %       ;   ~true_t(PROP)
  697. %       ).
  698. % th_nnf_out :-
  699. %       ~ ((n(possible_t(PROP)), true_t(PROP);false_t(PROP), true_t(PROP));unknown_t(PROP), true_t(PROP)).
  700. prove_possible_t(PROP) :-
  701.         prove_true_t(PROP).
  702. prove_not_true_t(PROP) :-
  703.         prove_not_possible_t(PROP).
  704. prove_not_false_t(PROP) :-
  705.         prove_true_t(PROP).
  706. prove_not_true_t(PROP) :-
  707.         prove_false_t(PROP).
  708. prove_not_unknown_t(PROP) :-
  709.         prove_true_t(PROP).
  710. prove_not_true_t(PROP) :-
  711.         prove_unknown_t(PROP).
  712. pfc :-
  713.         prove_true_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  714. pfc :-
  715.         prove_not_possible_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  716. pfc :-
  717.         prove_true_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  718. pfc :-
  719.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  720. pfc :-
  721.         prove_true_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  722. pfc :-
  723.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  724. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:248
  725. % :- test_boxlog(=>(~asserted_t(PROP_VAR), v(v(possible_t(PROP_VAR), false_t(PROP_VAR)), fallacy_t(PROP_VAR)))).
  726. % kif :-
  727. %       all(PROP,
  728. %           =>(~asserted_t(PROP), v(v(possible_t(PROP), false_t(PROP)), fallacy_t(PROP)))).
  729. % qualify_nesc :-
  730. %       all(PROP,
  731. %           nesc(=>(~asserted_t(PROP), v(v(possible_t(PROP), false_t(PROP)), fallacy_t(PROP))))).
  732. % nnf :-
  733. %       all(PROP,
  734. %           nesc(v(v(v(possible_t(PROP), false_t(PROP)), fallacy_t(PROP)), ~ (~asserted_t(PROP))))).
  735. % unq :-
  736. %       nesc(v(v(v(possible_t(PROP), false_t(PROP)), fallacy_t(PROP)), ~ (~asserted_t(PROP)))).
  737. % th_nnf_in :-
  738. %       (   (   (   possible_t(PROP)
  739. %               ;   false_t(PROP)
  740. %               )
  741. %           ;   fallacy_t(PROP)
  742. %           )
  743. %       ;   ~ (~asserted_t(PROP))
  744. %       ).
  745. % th_nnf_out :-
  746. %       ~ (((n(possible_t(PROP)), n(false_t(PROP))), n(fallacy_t(PROP))), n(asserted_t(PROP))).
  747. prove_possible_t(PROP) :-
  748.         prove_not_false_t(PROP),
  749.         prove_not_fallacy_t(PROP),
  750.         prove_not_asserted_t(PROP).
  751. prove_false_t(PROP) :-
  752.         prove_not_possible_t(PROP),
  753.         prove_not_fallacy_t(PROP),
  754.         prove_not_asserted_t(PROP).
  755. prove_fallacy_t(PROP) :-
  756.         prove_not_possible_t(PROP),
  757.         prove_not_false_t(PROP),
  758.         prove_not_asserted_t(PROP).
  759. prove_asserted_t(PROP) :-
  760.         prove_not_possible_t(PROP),
  761.         prove_not_false_t(PROP),
  762.         prove_not_fallacy_t(PROP).
  763. pfc :-
  764.         prove_not_false_t(PROP), prove_not_fallacy_t(PROP), prove_not_asserted_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  765. pfc :-
  766.         prove_not_possible_t(PROP), prove_not_fallacy_t(PROP), prove_not_asserted_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  767. pfc :-
  768.         prove_not_possible_t(PROP), prove_not_false_t(PROP), prove_not_asserted_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  769. pfc :-
  770.         prove_not_possible_t(PROP), prove_not_false_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_asserted_t(PROP).
  771. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:249
  772. % :- test_boxlog(=>(~possible_t(PROP_VAR), v(false_t(PROP_VAR), fallacy_t(PROP_VAR)))).
  773. % kif :-
  774. %       all(PROP, =>(~possible_t(PROP), v(false_t(PROP), fallacy_t(PROP)))).
  775. % qualify_nesc :-
  776. %       all(PROP, nesc(=>(~possible_t(PROP), v(false_t(PROP), fallacy_t(PROP))))).
  777. % nnf :-
  778. %       all(PROP,
  779. %           nesc(v(v(false_t(PROP), fallacy_t(PROP)), ~ (~possible_t(PROP))))).
  780. % unq :-
  781. %       nesc(v(v(false_t(PROP), fallacy_t(PROP)), ~ (~possible_t(PROP)))).
  782. % th_nnf_in :-
  783. %       (   (   false_t(PROP)
  784. %           ;   fallacy_t(PROP)
  785. %           )
  786. %       ;   ~ (~possible_t(PROP))
  787. %       ).
  788. % th_nnf_out :-
  789. %       ~ ((n(false_t(PROP)), n(fallacy_t(PROP))), n(possible_t(PROP))).
  790. prove_false_t(PROP) :-
  791.         prove_not_fallacy_t(PROP),
  792.         prove_not_possible_t(PROP).
  793. prove_fallacy_t(PROP) :-
  794.         prove_not_false_t(PROP),
  795.         prove_not_possible_t(PROP).
  796. prove_possible_t(PROP) :-
  797.         prove_not_false_t(PROP),
  798.         prove_not_fallacy_t(PROP).
  799. pfc :-
  800.         prove_not_fallacy_t(PROP), prove_not_possible_t(PROP), {is_unit(PROP)}==>prove_false_t(PROP).
  801. pfc :-
  802.         prove_not_false_t(PROP), prove_not_possible_t(PROP), {is_unit(PROP)}==>prove_fallacy_t(PROP).
  803. pfc :-
  804.         prove_not_false_t(PROP), prove_not_fallacy_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  805. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:250
  806. % :- test_boxlog(=>(possible_t(PROP_VAR), &(~false_t(PROP_VAR), ~fallacy_t(PROP_VAR)))).
  807. % kif :-
  808. %       all(PROP, =>(possible_t(PROP), &(~false_t(PROP), ~fallacy_t(PROP)))).
  809. % qualify_nesc :-
  810. %       all(PROP,
  811. %           nesc(=>(possible_t(PROP), &(~false_t(PROP), ~fallacy_t(PROP))))).
  812. % nnf :-
  813. %       all(PROP,
  814. %           &(nesc(v(~possible_t(PROP), ~false_t(PROP))), nesc(v(~possible_t(PROP), ~fallacy_t(PROP))))).
  815. % unq :-
  816. %       &(nesc(v(~possible_t(PROP), ~false_t(PROP))), nesc(v(~possible_t(PROP), ~fallacy_t(PROP)))).
  817. % th_nnf_in :-
  818. %       (   ~possible_t(PROP)
  819. %       ;   ~false_t(PROP)
  820. %       ),
  821. %       (   ~possible_t(PROP)
  822. %       ;   ~fallacy_t(PROP)
  823. %       ).
  824. % th_nnf_out :-
  825. %       ~ (possible_t(PROP), false_t(PROP);possible_t(PROP), fallacy_t(PROP)).
  826. prove_not_possible_t(PROP) :-
  827.         prove_false_t(PROP).
  828. prove_not_false_t(PROP) :-
  829.         prove_possible_t(PROP).
  830. prove_not_possible_t(PROP) :-
  831.         prove_fallacy_t(PROP).
  832. prove_not_fallacy_t(PROP) :-
  833.         prove_possible_t(PROP).
  834. pfc :-
  835.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_possible_t(PROP).
  836. pfc :-
  837.         prove_possible_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  838. pfc :-
  839.         prove_fallacy_t(PROP), {is_unit(PROP)}==>prove_not_possible_t(PROP).
  840. pfc :-
  841.         prove_possible_t(PROP), {is_unit(PROP)}==>prove_not_fallacy_t(PROP).
  842. % /home/prologmud_server/lib/swipl/pack/logicmoo_base/prolog/logicmoo/common_logic/common_logic_sanity.pl:251
  843. % :- test_boxlog(=>(unknown_t(PROP_VAR), &(&(&(~true_t(PROP_VAR), possible_t(PROP_VAR)), ~asserted_t(PROP_VAR)), ~false_t(PROP_VAR)))).
  844. % kif :-
  845. %       all(PROP,
  846. %           =>(unknown_t(PROP), &(&(&(~true_t(PROP), possible_t(PROP)), ~asserted_t(PROP)), ~false_t(PROP)))).
  847. % qualify_nesc :-
  848. %       all(PROP,
  849. %           nesc(=>(unknown_t(PROP), &(&(&(~true_t(PROP), possible_t(PROP)), ~asserted_t(PROP)), ~false_t(PROP))))).
  850. % nnf :-
  851. %       all(PROP,
  852. %           &(&(&(nesc(v(possible_t(PROP), ~unknown_t(PROP))), nesc(v(~true_t(PROP), ~unknown_t(PROP)))), nesc(v(~asserted_t(PROP), ~unknown_t(PROP)))), nesc(v(~false_t(PROP), ~unknown_t(PROP))))).
  853. % unq :-
  854. %       &(&(&(nesc(v(possible_t(PROP), ~unknown_t(PROP))), nesc(v(~true_t(PROP), ~unknown_t(PROP)))), nesc(v(~asserted_t(PROP), ~unknown_t(PROP)))), nesc(v(~false_t(PROP), ~unknown_t(PROP)))).
  855. % th_nnf_in :-
  856. %       ( ( (   possible_t(PROP)
  857. %           ;   ~unknown_t(PROP)
  858. %           ),
  859. %           (   ~true_t(PROP)
  860. %           ;   ~unknown_t(PROP)
  861. %           )
  862. %         ),
  863. %         (   ~asserted_t(PROP)
  864. %         ;   ~unknown_t(PROP)
  865. %         )
  866. %       ),
  867. %       (   ~false_t(PROP)
  868. %       ;   ~unknown_t(PROP)
  869. %       ).
  870. % th_nnf_out :-
  871. %       ~ (((n(possible_t(PROP)), unknown_t(PROP);true_t(PROP), unknown_t(PROP));asserted_t(PROP), unknown_t(PROP));false_t(PROP), unknown_t(PROP)).
  872. prove_possible_t(PROP) :-
  873.         prove_unknown_t(PROP).
  874. prove_not_unknown_t(PROP) :-
  875.         prove_not_possible_t(PROP).
  876. prove_not_true_t(PROP) :-
  877.         prove_unknown_t(PROP).
  878. prove_not_unknown_t(PROP) :-
  879.         prove_true_t(PROP).
  880. prove_not_asserted_t(PROP) :-
  881.         prove_unknown_t(PROP).
  882. prove_not_unknown_t(PROP) :-
  883.         prove_asserted_t(PROP).
  884. prove_not_false_t(PROP) :-
  885.         prove_unknown_t(PROP).
  886. prove_not_unknown_t(PROP) :-
  887.         prove_false_t(PROP).
  888. pfc :-
  889.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_possible_t(PROP).
  890. pfc :-
  891.         prove_not_possible_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  892. pfc :-
  893.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_true_t(PROP).
  894. pfc :-
  895.         prove_true_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  896. pfc :-
  897.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_asserted_t(PROP).
  898. pfc :-
  899.         prove_asserted_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  900. pfc :-
  901.         prove_unknown_t(PROP), {is_unit(PROP)}==>prove_not_false_t(PROP).
  902. pfc :-
  903.         prove_false_t(PROP), {is_unit(PROP)}==>prove_not_unknown_t(PROP).
  904. :- dynamic clif/1.
  905. :- multifile clif/1.
  906. :- public clif/1.
  907. :- module_transparent clif/1.
  908.  
  909.  
  910. :- dynamic boxlog/1.
  911. :- multifile boxlog/1.
  912. :- public boxlog/1.
  913. :- module_transparent boxlog/1.
  914.  
  915.  
  916. :- dynamic boxlog/1.
  917. :- multifile boxlog/1.
  918. :- public boxlog/1.
  919. :- module_transparent boxlog/1.
  920.  
  921.  
  922. :- dynamic pfclog/1.
  923. :- multifile pfclog/1.
  924. :- public pfclog/1.
  925. :- module_transparent pfclog/1.
  926.  
  927.  
  928. :- dynamic pfclog/1.
  929. :- multifile pfclog/1.
  930. :- public pfclog/1.
  931. :- module_transparent pfclog/1.
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!