API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Nov 20th, 2019
94
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 10.71 KB | None | 0 0
raw download clone embed print report
  1. verify(InputFileName) :- see(InputFileName),
  2. read(Prems), read(Goal), read(Proof),
  3. seen,
  4. valid_proof(Prems, Goal, Proof).
  5.  
  6. valid_proof(Prems, G, Proof) :- findlast(Proof, _, [_|[G|_]]), check_rules(Prems, Proof, Proof, 1).
  7.  
  8. findlast([X], [], X).
  9. findlast([H | T], [H | N], X) :- findlast(T, N, X).
  10.  
  11. check_rules(_, [[]], _, _).
  12. check_rules(_, [], _, _).
  13. check_rules(Prems, [[H|H1]|T2], Proof, Count) :- get_rule(Proof, Count, [R|_]), (R == premise, get_prop(Proof, Count, Prop), check_premise(Prop, Prems) ;
  14. R == assumption, check_assumption(Proof, Count) ;
  15. R = copy(_), get_pred_of_prop(R, [_|[Num|_]]), copy(Num, Count, Proof) ;
  16. R = andint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), andint(A, B, Count, Proof) ;
  17. R = andel1(_), get_pred_of_prop(R, [_|[Num|_]]), andel1(Num, Count, Proof) ;
  18. R = andel2(_), get_pred_of_prop(R, [_|[Num|_]]), andel2(Num, Count, Proof) ;
  19. R = orint1(_), get_pred_of_prop(R, [_|[Num|_]]), orint1(Num, Count, Proof) ;
  20. R = orint2(_), get_pred_of_prop(R, [_|[Num|_]]), orint2(Num, Count, Proof) ;
  21. R = orel(_, _, _, _, _), get_pred_of_prop(R, [_|[X|[A|[B|[C|[D|_]]]]]]), orel(X, A, B, C, D, Count, Proof) ;
  22. R = impint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), impint(A, B, Count, Proof) ;
  23. R = impel(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), impel(A, B, Count, Proof) ;
  24. R = negint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), negint(A, B, Count, Proof) ;
  25. R = negel(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), negel(A, B, Count, Proof) ;
  26. R = contel(_), get_pred_of_prop(R, [_|[Num|_]]), contel(Num, Count, Proof) ;
  27. R = negnegint(_), get_pred_of_prop(R, [_|[Num|_]]), negnegint(Num, Count, Proof) ;
  28. R = negnegel(_), get_pred_of_prop(R, [_|[Num|_]]), negnegel(Num, Count, Proof) ;
  29. R = mt(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), mt(A, B, Count, Proof) ;
  30. R = pbc(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), pbc(A, B, Count, Proof) ;
  31. R == lem, lem(Count, Proof)), !,
  32. C1 is Count + 1,
  33. ((list_empty(H1) ; get_list_head(H1, H2), not(is_list(H2))), check_rules(Prems, T2, Proof, C1) ;
  34. nested_list(H), get_tail(H, T), check_rules(Prems, [[T|H1]|T2], Proof, C1) ;
  35. get_list_head(H1, H2), is_list(H2), check_rules(Prems, [H1|T2], Proof, C1)).
  36.  
  37. list_empty([]).
  38. nested_list(A) :- A = [[_]|_] ; A = [_|[_]].
  39. get_tail([_|T], T).
  40.  
  41. check_assumption(Proof, Num) :- row_depth(Proof, Num, Depth), is_list(Depth), findlast(Depth, [_|_], 1).
  42.  
  43. check_premise(Result, H) :- Result == H.
  44. check_premise(Result, [H|T]) :- Result == H ; check_premise(Result, T).
  45.  
  46.  
  47. find_row([[[[H|T]|_]|_]|_], H, [H|T]).
  48. find_row([[[H|T]|_]|_], H, [H|T]).
  49. find_row([[H|T]|_], H, [H|T]).
  50. find_row([[[Hf|Tf]|T2]|[[H|T3]|T4]], Num, Result) :- less_than(H, Num), find_row([[H|T3]|T4], Num, Result) ; find_row([[Hf|Tf]|T2], Num, Result).
  51. find_row([[_|[T1|_]]|T2], Num, Result) :- (not(is_list(T1)), find_row(T2, Num, Result) ; find_row([T1|T2], Num, Result)).
  52.  
  53. less_than(H, Num) :- is_list(H), get_list_head(H, P), less_than(P, Num) ; not(is_list(H)), H =< Num.
  54.  
  55. get_list_head([H|_], H).
  56.  
  57. depth(X, [X|_], [C], C).
  58. depth(X, [H|_], [C|D], C) :- depth(X, H, D, 1).
  59. depth(X, [_|T], D, C) :- C1 is C+1, depth(X, T, D, C1).
  60.  
  61. row_depth(Proof, Row, Depth) :- find_row(Proof, Row, FullRow), depth(FullRow, Proof, Depth, 1).
  62.  
  63. find_row_and_depth(Proof, Num, Row, Depth) :- find_row(Proof, Num, Row), row_depth(Row, Proof, Depth).
  64.  
  65. get_prop(Proof, Num, Prop) :- find_row(Proof, Num, [_|[Prop|_]]).
  66.  
  67. get_rule(Proof, Num, Rule) :- find_row(Proof, Num, [_|[_|Rule]]).
  68.  
  69. get_pred_of_prop(L, List) :- L =.. List.
  70.  
  71. lesser_depth([_], _).
  72. lesser_depth([Ha|Ta], [Hb|Tb]) :- Ha is Hb, lesser_depth(Ta, Tb).
  73.  
  74. check_length(LengthA, LengthB) :- LengthA >= (LengthB - 1).
  75.  
  76. row_after_row_in_box(Proof, RowA, RowB) :-
  77. row_depth(Proof, RowA, DepthA),
  78. row_depth(Proof, RowB, DepthB),
  79. length(DepthA, LenA),
  80. length(DepthB, LenB),
  81. check_length(LenA, LenB),
  82. depthA_right_after_depthB(DepthA, DepthB).
  83.  
  84. depthA_right_after_depthB([A1], [A2|_]) :- A1 > A2.
  85. depthA_right_after_depthB([A1|[B1|_]], [A2|[B2|_]]) :-
  86. A1 = A2, B1 > B2 ;
  87. A1 > A2.
  88.  
  89.  
  90. valid_depth(Proof, RowA, RowB) :- row_depth(Proof, RowA, DepthA), row_depth(Proof, RowB, DepthB),
  91. lesser_depth(DepthA, DepthB).
  92. valid_depth_box(Proof, DepthBox, RowB) :- row_depth(Proof, RowB, DepthB),
  93. lesser_depth(DepthBox, DepthB).
  94.  
  95. check_box(Proof, Start, End, R) :- Start =< End, get_rule(Proof, Start, [Rule|_]), Rule == assumption, row_depth(Proof, Start, [Hs|Ts]), row_depth(Proof, End, [He|Te]), findlast([Hs|Ts], Rs, _), findlast([He|Te], Re, _), Rs = Re, C1 is End+1, row_depth(Proof, C1, [H|T]), findlast([H|T], Rc, _), not(Rc = Re), findlast([Hs|Ts], R, _).
  96.  
  97. copy(A, B, Proof) :-
  98. A < B,
  99. get_prop(Proof, A, PropA),
  100. get_prop(Proof, B, PropB),
  101. PropA==PropB, valid_depth(Proof, A, B).
  102.  
  103. andint(A, B, C, Proof) :-
  104. A < C,
  105. B < C,
  106. get_prop(Proof, A, PropA),
  107. get_prop(Proof, B, PropB),
  108. get_prop(Proof, C, PropC),
  109.  
  110. and(PropA, PropB) = PropC,
  111. valid_depth(Proof, A, C), valid_depth(Proof, B, C).
  112.  
  113. andel1(A, B, Proof) :-
  114. A < B,
  115.  
  116. get_prop(Proof, A, PropA),
  117. get_prop(Proof, B, PropB),
  118.  
  119. get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),
  120.  
  121. PredLeftA = PropB,
  122. valid_depth(Proof, A, B).
  123.  
  124. andel2(A, B, Proof) :-
  125. A < B,
  126.  
  127. get_prop(Proof, A, PropA),
  128. get_prop(Proof, B, PropB),
  129.  
  130. get_pred_of_prop(PropA, [_ | [_ | [PredRightA | _]]]),
  131.  
  132. PredRightA = PropB,
  133. valid_depth(Proof, A, B).
  134.  
  135. orint1(A, B, Proof) :-
  136. A < B,
  137.  
  138. get_prop(Proof, A, PropA),
  139. get_prop(Proof, B, PropB),
  140.  
  141. get_pred_of_prop(PropB, [_ | [PredLeftB | _]]),
  142.  
  143. PredLeftB = PropA,
  144. valid_depth(Proof, A, B).
  145.  
  146. orint2(A, B, Proof) :-
  147. A < B,
  148.  
  149. get_prop(Proof, A, PropA),
  150. get_prop(Proof, B, PropB),
  151.  
  152. get_pred_of_prop(PropB, [_ | [_ | [PredRightB | _]]]),
  153.  
  154. PredRightB = PropA,
  155. valid_depth(Proof, A, B).
  156.  
  157. orel(X, A, B, C, D, E, Proof) :-
  158. A < B,
  159. C < D,
  160. B < E,
  161. D < E,
  162. X < E,
  163.  
  164. check_box(Proof, A, B, Il1),
  165. valid_depth_box(Proof, Il1, E),
  166.  
  167. check_box(Proof, C, D, Il2),
  168. valid_depth_box(Proof, Il2, E),
  169.  
  170. get_prop(Proof, A, PropA),
  171. get_prop(Proof, B, PropB),
  172. get_prop(Proof, C, PropC),
  173. get_prop(Proof, D, PropD),
  174. get_prop(Proof, X, PropX),
  175.  
  176. PropB = PropD,
  177. (PropX = or(PropA, PropC) ; PropX = or(PropC, PropA)).
  178.  
  179. impint(A, B, C, Proof) :-
  180. %fail,
  181. A =< B,
  182. B < C,
  183.  
  184. check_box(Proof, A, B, _),
  185. %valid_depth_box(Proof, Indexlist, C),
  186. row_after_row_in_box(Proof, C, A),
  187. row_after_row_in_box(Proof, C, B),
  188. get_prop(Proof, A, PropA),
  189. get_prop(Proof, B, PropB),
  190. get_prop(Proof, C, PropC),
  191.  
  192. get_pred_of_prop(PropC, [_ | [PredLeftC | [PredRightC | _]]]),
  193.  
  194. PropA = PredLeftC,
  195. PropB = PredRightC.
  196.  
  197. impel(A, B, C, Proof) :-
  198. A < C,
  199. B < C,
  200.  
  201. get_prop(Proof, A, PropA),
  202. get_prop(Proof, B, PropB),
  203. get_prop(Proof, C, PropC),
  204.  
  205. ((get_pred_of_prop(PropB, [_ | [PredLeftB | [PredRightB | _]]]),
  206. PropA = PredLeftB,
  207. PropC = PredRightB) ;
  208. (get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),
  209. PropB = PredLeftA,
  210. PropC = PredRightA)),
  211.  
  212. valid_depth(Proof, A, C), valid_depth(Proof, B, C).
  213.  
  214. negint(A, B, C, Proof) :-
  215. A < B,
  216. A < C,
  217. B < C,
  218.  
  219. check_box(Proof, A, B, Indexlist),
  220. valid_depth_box(Proof, Indexlist, C),
  221.  
  222. get_prop(Proof, A, PropA),
  223. get_prop(Proof, B, PropB),
  224. get_prop(Proof, C, PropC),
  225.  
  226. get_pred_of_prop(PropC, [_ | [PredLeftC | _]]),
  227.  
  228. PropA = PredLeftC,
  229. PropB = cont.
  230.  
  231. negel(A, B, C, Proof) :-
  232. A < C,
  233. B < C,
  234.  
  235. get_prop(Proof, A, PropA),
  236. get_prop(Proof, B, PropB),
  237. get_prop(Proof, C, PropC),
  238.  
  239. ((PropB = neg(_), get_pred_of_prop(PropB, [_ | [PredLeftB | _]]),
  240. PropA = PredLeftB) ;
  241. (PropA = neg(_), get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),
  242. PropB = PredLeftA)),
  243.  
  244. PropC = cont,
  245. valid_depth(Proof, A, C), valid_depth(Proof, B, C).
  246.  
  247. contel(A, B, Proof) :-
  248. A < B,
  249.  
  250. get_prop(Proof, A, PropA),
  251.  
  252. PropA = cont,
  253. valid_depth(Proof, A, B).
  254.  
  255. negnegint(A, B, Proof) :-
  256. A < B,
  257.  
  258. get_prop(Proof, A, PropA),
  259. get_prop(Proof, B, PropB),
  260.  
  261. get_pred_of_prop(PropB, [_|[PredLeftB|_]]),
  262. get_pred_of_prop(PredLeftB, [_|[PredLeftBB|_]]),
  263.  
  264. PropA = PredLeftBB,
  265. valid_depth(Proof, A, B).
  266.  
  267. negnegel(A, B, Proof) :-
  268. A < B,
  269.  
  270. get_prop(Proof, A, PropA),
  271. get_prop(Proof, B, PropB),
  272.  
  273. get_pred_of_prop(PropA, [_|[PredLeftA|_]]),
  274. get_pred_of_prop(PredLeftA, [_|[PredLeftAA|_]]),
  275.  
  276. PropB = PredLeftAA.
  277.  
  278. mt(A, B, C, Proof) :-
  279. A < C,
  280. B < C,
  281.  
  282. get_prop(Proof, A, PropA),
  283. get_prop(Proof, B, PropB),
  284. get_prop(Proof, C, PropC),
  285.  
  286. get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),
  287.  
  288. neg(PredLeftA) = PropC,
  289. neg(PredRightA) = PropB,
  290. valid_depth(Proof, A, C), valid_depth(Proof, B, C).
  291.  
  292. pbc(A, B, C, Proof) :-
  293. A < B,
  294. B < C,
  295.  
  296. check_box(Proof, A, B, Indexlist),
  297. valid_depth_box(Proof, Indexlist, C),
  298.  
  299. get_prop(Proof, A, PropA),
  300. get_prop(Proof, B, PropB),
  301. get_prop(Proof, C, PropC),
  302.  
  303. (PropC = neg(PropA) ;
  304. get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),
  305. PropC = PredLeftA),
  306. PropB == cont.
  307.  
  308. lem(A, Proof) :-
  309.  
  310. get_prop(Proof, A, PropA),
  311.  
  312. get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),
  313.  
  314. (neg(PredLeftA) = PredRightA ; PredLeftA = neg(PredRightA)),
  315. (PropA = or(PredLeftA, PredRightA) ; PropA = or(PredRightA, PredLeftA)).
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!