home *** CD-ROM | disk | FTP | other *** search
/ Turbo Toolbox / Turbo_Toolbox.iso / 1987 / 06 / logelei.pro < prev    next >
Encoding:
Text File  |  1987-05-18  |  3.6 KB  |  174 lines
  1. "Eingabe der Formeln"
  2.  
  3. Start ->
  4.    Lesen(nil,i)
  5.    /;
  6.  
  7. Lesen(nil,i) -> in(i) in-char(c) Lesen(i,i');
  8. Lesen(P,i) -> in(i) in-char(c) Weiter(P,i);
  9.  
  10. Weiter(P,SCHLUSS) -> in(f) in-char(c) Folgt(P,f);
  11. Weiter(P,i) -> Lesen(UND(i,P),i');
  12.  
  13. "Hauptaufrufe"
  14.  
  15. Folgt(P,k) ->
  16.    reset-cpu-time
  17.    Infix(P,i)
  18.    DNF(i,d)
  19.    Check(d)
  20.    ]berpr}fung(k,d)
  21.    cpu-time(t)
  22.    outl(t)
  23.    /;
  24.  
  25. Check(nil) ->
  26.    /
  27.    outm("Die Pr{missen widersprechen einander!")
  28.    fail;
  29. Check(x) ->;
  30.  
  31. Antwort(k,wahr) -> outm("So ist es: ") out(k) outm(" folgt.") /;
  32. Antwort(k,falsch) ->
  33.    outm("Ganz im Gegenteil: NICHT(")
  34.    out(k)
  35.    outm(") folgt!");
  36. Antwort(k,unbestimmt) ->
  37.    out(k)
  38.    outm(" folgt nicht, aber NICHT(")
  39.    out(k)
  40.    outm(") folgt auch nicht.");
  41.  
  42. "Elimination von Junktoren und Verschiebung der Negation"
  43.  
  44. Infix(NICHT(UND(p-hi,p-si)),ODER(p-hi',p-si')) ->
  45.    /
  46.    Infix(NICHT(p-hi),p-hi')
  47.    Infix(NICHT(p-si),p-si');
  48. Infix(NICHT(ODER(p-hi,p-si)),UND(p-hi',p-si')) ->
  49.    /
  50.    Infix(NICHT(p-hi),p-hi')
  51.    Infix(NICHT(p-si),p-si');
  52. Infix(NICHT(WENN(p-hi,p-si)),y) ->
  53.    /
  54.    Infix(UND(p-hi,NICHT(p-si)),y);
  55. Infix(NICHT(NICHT(p-hi)),x) -> / Infix(p-hi,x);
  56. Infix(WENN(p-hi,p-si),ODER(p-hi',p-si')) ->
  57.    /
  58.    Infix(NICHT(p-hi),p-hi')
  59.    Infix(p-si,p-si');
  60. Infix(GDW(p-hi,p-si),ODER(UND(p-hi',p-si'),UND(p-hi'',p-si''))) ->
  61.    /
  62.    Infix(p-hi,p-hi')
  63.    Infix(p-si,p-si')
  64.    Infix(NICHT(p-hi),p-hi'')
  65.    Infix(NICHT(p-si),p-si'');
  66. Infix(NICHT(GDW(p-hi,p-si)),ODER(UND(p-hi',p-si''),UND(p-hi'',p-si'))) ->
  67.    /
  68.    Infix(p-hi,p-hi')
  69.    Infix(p-si,p-si')
  70.    Infix(NICHT(p-hi),p-hi'')
  71.    Infix(NICHT(p-si),p-si'');
  72. Infix(UND(p-hi,p-si),UND(p-hi',p-si')) -> 
  73.    / 
  74.    Infix(p-hi,p-hi') 
  75.    Infix(p-si,p-si');
  76. Infix(ODER(p-hi,p-si),ODER(p-hi',p-si')) ->
  77.    /
  78.    Infix(p-hi,p-hi')
  79.    Infix(p-si,p-si');
  80. Infix(x,x) -> /;
  81.  
  82. "Distributive (Listen-)Normalform"
  83.  
  84. DNF(ODER(p-hi,p-si),l) ->
  85.    /
  86.    DNF(p-hi,p-hi')
  87.    DNF(p-si,p-si')
  88.    append(p-hi',p-si',l);
  89. DNF(UND(p-hi,p-si),f) ->
  90.    /
  91.    DNF(p-hi,p-hi')
  92.    DNF(p-si,p-si')
  93.    Distr(p-hi',p-si',f);
  94. DNF(NICHT(p-hi),<nil,p-hi.nil>.nil) -> /;
  95. DNF(f,<f.nil,nil>.nil) -> /;
  96.  
  97. Distr(x,nil,nil) -> /;
  98. Distr(<p,n>.nil,<p',n'>.r',r'') ->
  99.    ]berlappung(p,n')
  100.    /
  101.    Distr(<p,n>.nil,r',r'');
  102. Distr(<p,n>.nil,<p',n'>.r',r'') ->
  103.    ]berlappung(p',n)
  104.    /
  105.    Distr(<p,n>.nil,r',r'');
  106. Distr(<p,n>.nil,<p',n'>.r',r-neu) ->
  107.    Distr(<p,n>.nil,r',r'')
  108.    append(p,p',p'')
  109.    append(n,n',n'')
  110.    Disjunkte-Vereinigung(<p'',n''>,r'',r-neu)
  111.    /;
  112. Distr(x.r,l,l'') ->
  113.    /
  114.    Distr(r,l,l')
  115.    Distr(x.nil,l,x')
  116.    append(x',l',l'');
  117. Distr(nil,x,x) -> /;
  118.  
  119. "Logik"
  120.  
  121. ]berpr}fung(f,d) -> Positiv(f,d) / Antwort(f,wahr);
  122. ]berpr}fung(f,d) ->
  123.    Negativ(f,d)
  124.    /
  125.    Antwort(f,falsch)
  126.    /;
  127. ]berpr}fung(f,d) ->
  128.    /
  129.    Antwort(f,unbestimmt);
  130.  
  131. Positiv(f,<p,n>.r) ->
  132.    Ele(f,p)
  133.    /
  134.    Positiv(f,r);
  135. Positiv(f,nil) ->;
  136.  
  137. Negativ(f,<p,n>.r) ->
  138.    Ele(f,n)
  139.    /
  140.    Negativ(f,r);
  141. Negativ(f,nil) ->;
  142.  
  143. "Hilfspr{dikate"
  144.  
  145. disjunkt(f.p,n) -> disjunkt(p,n) NEle(f,n);
  146. disjunkt(nil,n) ->;
  147.  
  148. ]berlappung(x.r,l) -> Ele(x,l) /;
  149. ]berlappung(x.r,l) -> ]berlappung(r,l);
  150.  
  151. append(nil,l,l) ->;
  152. append(x.l,l',x.e) -> append(l,l',e);
  153.  
  154. Ele(x,x.r) -> /;
  155. Ele(x,y.r) -> Ele(x,r);
  156.  
  157. NEle(x,y.l) -> dif(x,y) NEle(x,l);
  158. NEle(x,nil) ->;
  159.  
  160. Neu(<p,n>,<p',n'>.l) ->
  161.    NSub(<p,n>,<p',n'>)
  162.    Neu(<p,n>,l);
  163. Neu(x,nil) ->;
  164.  
  165. NSub(<p,n>,<p',n'>) -> NSub(p,p') /;
  166. NSub(<p,n>,<p',n'>) -> NSub(n,n');
  167. NSub(x.r,l) -> NEle(x,l) /;
  168. NSub(x.r,l) -> NSub(r,l);
  169.  
  170. Disjunkte-Vereinigung(x,l,x.l) -> Neu(x,l) /;
  171. Disjunkte-Vereinigung(x,l,l) -> /;
  172.  
  173.  
  174.