API tools faq
paste
Advertisement
logicmoo

Untitled

logicmoo
Apr 9th, 2019
579
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 10.65 KB | None | 0 0
raw download clone embed print report
  1.  
  2. %  nat(X):- between(0,inf,X).
  3. %  ~nat(X):- \+ nat(X).
  4.  
  5.  
  6.  
  7. ?- notrace(kif_to_boxlog( all(P,all(X,all(Y, and(P=X*Y , ~(X=1) , ~(Y =1)) => ~prime(P)))), Out)),maplist(dmsg,Out).
  8.  
  9. % proven_tru(X=1) :-
  10. %     nesc(prime(P)).
  11. %     nesc(P=X*Y),
  12. %     falsify(Y=1).
  13.  
  14. % proven_neg(prime(P)) :-
  15. %     nesc(P=X*Y),
  16. %     falsify(X=1),
  17. %     falsify(Y=1).
  18.  
  19. % proven_neg(P=X*Y) :-
  20. %     nesc(prime(P)).
  21. %     falsify(X=1),
  22. %     falsify(Y=1).
  23.  
  24.  
  25.  
  26. ?- notrace(kif_to_boxlog( all(M, and( nat(M) , M>1 ) => exists(Y,exists(X, and(prime(X), prime(Y)) =>  M+M=X+Y ))), Out)),maplist(dmsg,Out).
  27.  
  28. % deduce_tru(M+M=X+Y) :-
  29. %     nesc(prime(X)),
  30. %     nesc(prime(Y)),
  31. %     nesc(nat(M)),
  32. %     nesc(M>1).
  33.  
  34. % proven_neg(prime(X)) :-
  35. %     nesc(prime(Y)),
  36. %     nesc(nat(M)),
  37. %     nesc(M>1),
  38. %     falsify(M+M=X+Y).
  39.  
  40.  
  41. % deduce_neg(M+M=X+Y) :-
  42. %     skolem(M,
  43. %            skF(1,
  44. %                'skMNat>False=+_1_0FnSk'(Y, X),
  45. %                M,
  46. %                [a(nat(M))=true, o(M>1)=true, p(M+M=X+Y)=false, ...(_21563482)])).
  47. % deduce_tru(nat(M)) :-
  48. %     skolem(M,
  49. %            skF(1,
  50. %                'skMNat>False=+_1_0FnSk'(Y, X),
  51. %                M,
  52. %                [a(nat(M))=true, o(M>1)=true, p(M+M=X+Y)=false, ...(_21573706)])).
  53. % deduce_tru(prime(X)) :-
  54. %     skolem(M,
  55. %            skF(1,
  56. %                'skMNat>False=+_1_0FnSk'(Y, X),
  57. %                M,
  58. %                [a(nat(M))=true, o(M>1)=true, p(M+M=X+Y)=false, ...(_21583968)])).
  59. % deduce_tru(M>1) :-
  60. %     skolem(M,
  61. %            skF(1,
  62. %                'skMNat>False=+_1_0FnSk'(Y, X),
  63. %                M,
  64. %                [a(nat(M))=true, o(M>1)=true, p(M+M=X+Y)=false, ...(_21594282)])).
  65.  
  66.  
  67.  
  68.  
  69.  
  70.  ?- cls, notrace(kif_to_boxlog(all(M, and( nat(M) , M>1 ) => exists(Y,exists(X, and(prime(X), prime(Y)) =>  M+M=X+Y ))), Out)),maplist(dmsg,Out).
  71.  
  72. % kif :-
  73. %     all(M, =>(nat(M)&(M>1), exists(Y, exists(X, =>(prime(X)&prime(Y), M+M=X+Y))))).
  74. % maplist(call, [put_attr(Y, skv, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, [_27489472, _27489478]))]),
  75. % attr_unify_hook(skXFalsePrime_1_0FnSk(Y, M), [_27489472, _27489478]).
  76. % nnf :-
  77. %     maplist(call,
  78. %
  79. %             [ put_attr(X, skv, skXFalsePrime_1_0FnSk(Y, M)),
  80. %               put_attr(Y, skv, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X))
  81. %             ]),
  82. %     v(v(~nat(M), ~ (M>1)),
  83. %       v((prime(X)&prime(Y))& ~ (M+M=X+Y), skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [or([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false], p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=true), or(or(a(prime(Y))=false, p(M+M=X+Y)=true), p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=false)])))&v(~skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [or([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false], p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=true), or(or(a(prime(Y))=false, p(M+M=X+Y)=true), p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=false)])), v((prime(X)&prime(Y))& ~ (M+M=X+Y), skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [or(or(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)])))&v(v(v(~prime(X), ~prime(Y)), M+M=X+Y), ~skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [or(or(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)]))))).
  84. % tlog_nnf_out_negated :-
  85. %     (n(~nat(M))&n(~ (M>1)))&v(v(v(n(nesc(prime(X))), n(nesc(prime(Y)))), n(~ (M+M=X+Y)))&n(nesc(skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [v([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false], p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [v(v(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)])))=true), v(v(a(prime(Y))=false, p(M+M=X+Y)=true), p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [v(v(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)])))=false)])))), n(~skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [v([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false], p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [v(v(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)])))=true), v(v(a(prime(Y))=false, p(M+M=X+Y)=true), p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [v(v(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)])))=false)])))&v(v(v(n(nesc(prime(X))), n(nesc(prime(Y)))), n(~ (M+M=X+Y)))&n(nesc(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [v(v(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)])))),  ((n(~prime(X))&n(~prime(Y)))&n(nesc(M+M=X+Y)))&n(~skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [v(v(a(prime(X))=false, q(prime(Y))=false), p(M+M=X+Y)=true)]))))).
  86. %
  87. c_success(baseKB,baseKB:same_clauses((deduce_neg(prime(_27388362)):-nesc(prime(_27434018)),falsify(_27285840+_27285840=_27388362+_27434018),skolem(_27388362,skF(1,skXFalsePrime_1_0FnSk(_27434018,_27285840),_27388362,[((a(prime(_27388362))=false;q(prime(_27434018))=false);p(_27285840+_27285840=_27388362+_27434018)=true)])),skolem(_27434018,skF(1,'skYPrimeFalse=Arg2+_1_1FnSk'(_27285840,_27388362),_27434018,[([[q(prime(_27388362))=true,a(prime(_27434018))=true],p(_27285840+_27285840=_27388362+_27434018)=false];p(skolem(_27388362,skF(1,skXFalsePrime_1_0FnSk(_27434018,_27285840),_27388362,[((a(prime(_27388362))=false;q(prime(_27434018))=false);p(_27285840+_27285840=_27388362+_27434018)=true)])))=true),((a(prime(_27434018))=false;p(_27285840+_27285840=_27388362+_27434018)=true);p(skolem(_27388362,skF(1,skXFalsePrime_1_0FnSk(_27434018,_27285840),_27388362,[((a(prime(_27388362))=false;q(prime(_27434018))=false);p(_27285840+_27285840=_27388362+_27434018)=true)])))=false)])),nesc(nat(_27285840)),nesc(_27285840>1)),(deduce_neg(prime(_27434018)):-nesc(prime(_27388362)),falsify(_27285840+_27285840=_27388362+_27434018),skolem(_27388362,skF(1,skXFalsePrime_1_0FnSk(_27434018,_27285840),_27388362,[((a(prime(_27388362))=false;q(prime(_27434018))=false);p(_27285840+_27285840=_27388362+_27434018)=true)])),skolem(_27434018,skF(1,'skYPrimeFalse=Arg2+_1_1FnSk'(_27285840,_27388362),_27434018,[([[q(prime(_27388362))=true,a(prime(_27434018))=true],p(_27285840+_27285840=_27388362+_27434018)=false];p(skolem(_27388362,skF(1,skXFalsePrime_1_0FnSk(_27434018,_27285840),_27388362,[((a(prime(_27388362))=false;q(prime(_27434018))=false);p(_27285840+_27285840=_27388362+_27434018)=true)])))=true),((a(prime(_27434018))=false;p(_27285840+_27285840=_27388362+_27434018)=true);p(skolem(_27388362,skF(1,skXFalsePrime_1_0FnSk(_27434018,_27285840),_27388362,[((a(prime(_27388362))=false;q(prime(_27434018))=false);p(_27285840+_27285840=_27388362+_27434018)=true)])))=false)])),nesc(nat(_27285840)),nesc(_27285840>1))))
  88.  
  89. % deduce_neg(prime(X)) :-
  90. %     nesc(prime(Y)),
  91. %     falsify(M+M=X+Y),
  92. %     skolem(X,
  93. %            skF(1,
  94. %                skXFalsePrime_1_0FnSk(Y, M),
  95. %                X,
  96. %                [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])),
  97. %     skolem(Y,
  98. %            skF(1,
  99. %                'skYPrimeFalse=Arg2+_1_1FnSk'(M, X),
  100. %                Y,
  101. %
  102. %                [ ([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false];p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=true),
  103. %                  ((a(prime(Y))=false;p(M+M=X+Y)=true);p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=false)
  104. %                ])),
  105. %     nesc(nat(M)),
  106. %     nesc(M>1).
  107. % deduce_tru(M+M=X+Y) :-
  108. %     nesc(prime(X)),
  109. %     nesc(prime(Y)),
  110. %     skolem(X,
  111. %            skF(1,
  112. %                skXFalsePrime_1_0FnSk(Y, M),
  113. %                X,
  114. %                [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])),
  115. %     skolem(Y,
  116. %            skF(1,
  117. %                'skYPrimeFalse=Arg2+_1_1FnSk'(M, X),
  118. %                Y,
  119. %
  120. %                [ ([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false];p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=true),
  121. %                  ((a(prime(Y))=false;p(M+M=X+Y)=true);p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=false)
  122. %                ])),
  123. %     nesc(nat(M)),
  124. %     nesc(M>1).
  125. % make_existential(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])) :-
  126. %     (   ensure_cond(X, prime(X)),
  127. %         never_cond(X, prime(Y))
  128. %     ;   ensure_cond(X, M+M=X+Y)
  129. %     ),
  130. %     skolem(Y,
  131. %            skF(1,
  132. %                'skYPrimeFalse=Arg2+_1_1FnSk'(M, X),
  133. %                Y,
  134. %
  135. %                [ ([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false];p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=true),
  136. %                  ((a(prime(Y))=false;p(M+M=X+Y)=true);p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=false)
  137. %                ])),
  138. %     ensure_cond(X, nat(M)),
  139. %     ensure_cond(X, M>1).
  140. % make_existential(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [([[q(prime(X))=true, a(prime(Y))=true], p(M+M=X+Y)=false];p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=true),  ((a(prime(Y))=false;p(M+M=X+Y)=true);p(skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((a(prime(X))=false;q(prime(Y))=false);p(M+M=X+Y)=true)])))=false)])) :-
  141. %     (   ensure_cond(Y, prime(X)),
  142. %         never_cond(Y, prime(Y))
  143. %     ;   ensure_cond(Y, M+M=X+Y)
  144. %     ),
  145. %     ensure_cond(Y, nat(M)),
  146. %     ensure_cond(Y, M>1).
  147. Out = [(deduce_neg(prime(X)):-nesc(prime(Y)), falsify(M+M=X+Y), skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((...;...);... = ...)])), skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [(...;...)|...])), nesc(nat(M)), nesc(M>1)),  (deduce_tru(M+M=X+Y):-nesc(prime(X)), nesc(prime(Y)), skolem(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [(...;...)])), skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(..., ...), Y, [...|...])), nesc(nat(...)), nesc(... > ...)),  (make_existential(X, skF(1, skXFalsePrime_1_0FnSk(Y, M), X, [((... = ...;... = ...);p(...)=true)])):-(ensure_cond(X, prime(X)), never_cond(X, prime(Y));ensure_cond(X, M+M=X+Y)), skolem(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [(...;...)|...])), ensure_cond(X, nat(M)), ensure_cond(X, M>1)),  (make_existential(Y, skF(1, 'skYPrimeFalse=Arg2+_1_1FnSk'(M, X), Y, [([...|...];... = ...),  (...;...)])):-(ensure_cond(Y, prime(...)), never_cond(Y, prime(...));ensure_cond(Y, ... + ... = ... + ...)), ensure_cond(Y, nat(M)), ensure_cond(Y, M>1))].
  148.  
  149. baseKB: [debug]  ?-
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!