Download | Plain Text | No Line Numbers 

  1. % Manuel Mausz, 0728348
  2. % unit tests befinden sich in gol.plt
  3.  
  4. % operator wertigkeit definieren
  5. :- op(425, fy,  -).
  6. :- op(450, yfx, &).
  7. :- op(500, yfx, v).
  8.  
  9. % --------------------------------------------------------------------------
  10.  
  11. % wenn A atom ist, retourniere A
  12. nnf(A, A) :-
  13. 	atomic(A).
  14.  
  15. % wenn A negiert ist und A atom ist, reourniere A negiert
  16. nnf(-A, -A) :-
  17. 	atomic(A).
  18.  
  19. % wenn A doppelt negiert ist, entferne die doppelte negation
  20. nnf(-(-A), X) :-
  21. 	nnf(A, X).
  22.  
  23. % de morgansche gesetze
  24. nnf(-(A & B), X) :-
  25. 	nnf(-A v -B, X).
  26. nnf(-(A v B), X) :-
  27. 	nnf(-A & -B, X).
  28.  
  29. % akzeptiere kon-/disjunktionen, wenn die subterme in NNF sind
  30. nnf(A & B, X & Y) :-
  31. 	nnf(A, X), nnf(B, Y).
  32. nnf(A v B, X v Y) :-
  33. 	nnf(A, X), nnf(B, Y).
  34.  
  35. % --------------------------------------------------------------------------
  36.  
  37. % literal check
  38. literalp(A) :-
  39. 	atomic(A).
  40. literalp(-A) :-
  41. 	atomic(A).
  42.  
  43. % --------------------------------------------------------------------------
  44.  
  45. % anzahl der "oder" (v) zaehlen
  46. no_or(A, X) :-
  47. 	literalp(A), X is 0.
  48. no_or(A v B, X) :-
  49. 	no_or(A, Y1), no_or(B, Y2), X is Y1 + Y2 + 1.
  50. no_or(A & B, X) :-
  51. 	no_or(A, Y1), no_or(B, Y2), X is Y1 + Y2.
  52.  
  53. % --------------------------------------------------------------------------
  54.  
  55. % prove2/3 wrapper fuer prove3/4
  56. prove2(F1, F2, NOW) :-
  57. 	prove2(F1, F2, NOW, _DATA).
  58.  
  59. % axioms
  60. prove2(A, -A, _NOW, axiom([A, -A])).
  61. prove2(-A, A, _NOW, axiom([A, -A])).
  62.  
  63. % (&, literal)
  64. prove2((F1 & F2), A, NOW, undRegel([F1 & F2, A], [Praem1, Praem2])) :-
  65. 	literalp(A), prove2(F1, A, NOW, Praem1), prove2(F2, A, NOW, Praem2).
  66.  
  67. % (literal, &)
  68. prove2(A, (F1 & F2), NOW, undRegel([A, F1 & F2], [Praem1, Praem2])) :-
  69. 	literalp(A), prove2(A, F1, NOW, Praem1), prove2(A, F2, NOW, Praem2).
  70.  
  71. % (v, literal)
  72. prove2((F1 v F2), A, NOW, oderRegel([F1 v F2, A], Praem)) :-
  73. 	literalp(A), prove2(F1, A, NOW, Praem).
  74. prove2((F1 v F2), A, NOW, oderRegel([F1 v F2, A], Praem)) :-
  75. 	literalp(A), prove2(F2, A, NOW, Praem).
  76.  
  77. % (literal, v)
  78. prove2(A, (F1 v F2), NOW, oderRegel([A, F1 v F2], Praem)) :-
  79. 	literalp(A), prove2(A, F1, NOW, Praem).
  80. prove2(A, (F1 v F2), NOW, oderRegel([A, F1 v F2], Praem)) :-
  81. 	literalp(A), prove2(A, F2, NOW, Praem).
  82.  
  83. % (&, &)
  84. prove2((F1 & F2), (F3 & F4), NOW, undRegel([F1 & F2, F3 & F4], [Praem1, Praem2])) :-
  85. 	prove2(F1, (F3 & F4), NOW, Praem1), prove2(F2, (F3 & F4), NOW, Praem2).
  86. prove2((F1 & F2), (F3 & F4), NOW, undRegel([F1 & F2, F3 & F4], [Praem1, Praem2])) :-
  87. 	prove2((F1 & F2), F3, NOW, Praem1), prove2((F1 & F2), F4, NOW, Praem2).
  88.  
  89. % (&, v)
  90. prove2((F1 & F2), (F3 v F4), NOW, undRegel([F1 & F2, F3 v F4], [Praem1, Praem2])) :-
  91. 	prove2(F1, (F3 v F4), NOW, Praem1), prove2(F2, (F3 v F4), NOW, Praem2).
  92. prove2((F1 & F2), (F3 v F4), NOW, oderRegel([F1 & F2, F3 v F4], Praem)) :-
  93. 	prove2((F1 & F2), F3, NOW, Praem).
  94. prove2((F1 & F2), (F3 v F4), NOW, oderRegel([F1 & F2, F3 v F4], Praem)) :-
  95. 	prove2((F1 & F2), F4, NOW, Praem).
  96.  
  97. % (v, &)
  98. prove2((F1 v F2), (F3 & F4), NOW, oderRegel([F1 v F2, F3 & F4], Praem)) :-
  99. 	prove2(F1, (F3 & F4), NOW, Praem).
  100. prove2((F1 v F2), (F3 & F4), NOW, oderRegel([F1 v F2, F3 & F4], Praem)) :-
  101. 	prove2(F2, (F3 & F4), NOW, Praem).
  102. prove2((F1 v F2), (F3 & F4), NOW, undRegel([F1 & F2, F3 v F4], [Praem1, Praem2])) :-
  103. 	prove2((F1 v F2), F3, NOW, Praem1), prove2((F1 v F2), F4, NOW, Praem2).
  104.  
  105. % (v, W)
  106. prove2((F1 v F2), Z, NOW, weakening([F1 v F2, Z], Praem)) :-
  107. 	NOW > 0, Z \== (F1 v F2), Z \== (F2 v F1),
  108. 	prove2((F1 v F2), (F1 v F2), NOW - 1, Praem).
  109.  
  110. % (W, v)
  111. prove2(Z, (F1 v F2), NOW, weakening([Z, F1 v F2], Praem)) :-
  112. 	NOW > 0, Z \== (F1 v F2), Z \== (F2 v F1),
  113. 	prove2((F1 v F2), (F1 v F2), NOW - 1, Praem).
  114.  
  115. % (v, v)
  116. prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
  117. 	prove2(F1, (F3 v F4), NOW, Praem).
  118. prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
  119. 	prove2(F2, (F3 v F4), NOW, Praem).
  120. prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
  121. 	prove2((F1 v F2), F3, NOW, Praem).
  122. prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
  123. 	prove2((F1 v F2), F4, NOW, Praem).
  124.  
  125. % --------------------------------------------------------------------------
  126.  
  127. % zusatzaufgabe 1
  128. writelist([]) :- !.
  129. writelist([X]) :- write(X), !.
  130. writelist([H | T] ) :- write(H), write(', '), writelist(T).
  131.  
  132. writeKonk(Konk) :-
  133. 	write('|- '), writelist(Konk), nl.
  134. writeRegel(Str, Konk, Praem) :-
  135. 	call(Praem),
  136. 	write('-------------------------------------------------- '), write(Str), nl,
  137. 	writeKonk(Konk).
  138. oderRegel(Konk, Praem) :-
  139. 	writeRegel('or', Konk, Praem).
  140. undRegel(Konk, [P1, P2]) :-
  141. 	writeRegel('and', Konk, P1),
  142. 	write('================================================== '), nl,
  143. 	writeRegel('and', Konk, P2).
  144. weakening(Konk, Praem) :-
  145. 	writeRegel('W', Konk, Praem).
  146. axiom(Konk) :-
  147. 	writeKonk(Konk).
  148.  
  149. % --------------------------------------------------------------------------
  150.  
  151. % prover
  152. :- dynamic(prove_print/0).
  153. prove(IN) :-
  154. 	nnf(IN, NNF), no_or(NNF, NOR), prove2(NNF, NNF, NOR, DATA), (prove_print, call(DATA); true).
  155.  
  156. % vim: set noet sw=4 ts=4:
  157.