/*
Autor: MB
Datum: MAY 2016
Entscheidungsverfahren fuer LP ausgehend von Wahrheitsbedingungen.
Analog zum entsprechenden Vorgehen in der Aussagenlogik.
LP hat dieselben Theorem wie die Aussagenlogik.
Es interessieren also eigentlich nur Widerlegungen von Folgerungen, d.h.
Erfuellbarkeit der Konjunktionen von Praemissen und reiner Falschheit
der Konklusion einer mutmasslichen Folgerung.
(Die benoetigten Hilfspraedikate zur Zerlegung einer Formel befinden sich
im hinteren Teil des Files.)
*/



% Teil 1. Tests fuer Theoreme und Folgerungen

ueberpruefe(Formel):- flacheTermliste(Formel,Termliste),
                      anzahlVariablen(Termliste,_,N),
                      Belegungen is 3 ** N,
                      findall(_,(berechne(Formel,w);berechne(Formel,b)),Loesungsliste),
                      length(Loesungsliste,Belegungen),
                      writeln('Die Formel ist LP-parakonsistent gültig!'), !.
ueberpruefe(_):- writeln('Die Formel ist nicht LP-parakonsistent gültig!').

% Test fuer Hilbert/Ackermann Axiom 1:  ueberpruefe(wenn_dann(P, wenn_dann(Q,P))).
% Test fuer Transitivitaet:  ueberpruefe(wenn_dann(und(wenn_dann(P,Q),wenn_dann(Q,R)), wenn_dann(P,R))).
% Test fuer ungueltige Formel: ueberpruefe(wenn_dann(P,wenn_dann(P,Q))).

reductio(Praemisse,Konklusion):-
                      (berechne(Praemisse,w);berechne(Praemisse,b)),
                      berechne(Konklusion,f),
                      writeln('Die Folgerung ist nicht LP-parakonsistent gültig!'), !.
reductio(_,_):- writeln('Die Folgerung ist LP-parakonsistent gültig!').

% Test fuer Ex Falso Quodlibet: reductio(und(P,nicht(P)),Q).
% Test fuer Konjunktionsbeseitigung: reductio(und(P,Q),Q).

% Teil 2. LP-Wahrheitsbedingungen
% LP-Wahrheitsbedingungen: es gibt die Wahrheitswerte w, f, b.
% Designierte Wahrheitswerte sind: w, b.
nicht(A):-
  berechne(A, AE),           % die evtl. komplexe Aussage im Skopus auswerten
  nicht(AE, w).
nicht(w, f).
nicht(f, w).
nicht(b, b).

und(A, B):-
  berechne(A, AE),
  berechne(B, BE),
  und(AE, BE, w).
und(w, w, w).
und(w, f, f).
und(f, w, f).
und(f, f, f).
und(b, w, b).
und(b, f, f).
und(b, b, b).
und(w, b, b).
und(f, b, f).

oder(A, B):-
  berechne(A, AE),
  berechne(B, BE),
  oder(AE, BE, w).
oder(w, w, w).
oder(w, f, w).
oder(f, w, w).
oder(f, f, f).
oder(b, w, w).
oder(w, b, w).
oder(b, f, b).
oder(f, b, b).
oder(b, b, b).

entweder_oder(A, B):-
  berechne(A, AE),
  berechne(B, BE),
  entweder_oder(AE, BE, w).
entweder_oder(w, w, f).
entweder_oder(w, f, w).
entweder_oder(f, w, w).
entweder_oder(f, f, f).
entweder_oder(b, w, f).
entweder_oder(w, b, f).
entweder_oder(f, b, b).
entweder_oder(b, f, b).
entweder_oder(b, b, b).

wenn_dann(A, B):-
  berechne(A, AE),
  berechne(B, BE),
  wenn_dann(AE, BE, w).
wenn_dann(w, w, w).
wenn_dann(w, f, f).
wenn_dann(f, w, w).
wenn_dann(f, f, w).
wenn_dann(w, b, b).
wenn_dann(b, w, w).
wenn_dann(b, f, b).
wenn_dann(f, b, w).
wenn_dann(b, b, b).

genau_dann(A, B):-
  berechne(A, AE),
  berechne(B, BE),
  genau_dann(AE, BE, w).
genau_dann(w, w, w).
genau_dann(w, f, f).
genau_dann(f, w, f).
genau_dann(f, f, w).
genau_dann(w, b, b).
genau_dann(b, w, b).
genau_dann(b, f, b).
genau_dann(f, b, b).
genau_dann(b, b, b).

berechne(w, w).
berechne(b, b).
berechne(f, f):- !.
berechne(nicht(A), B):-
  berechne(A, AE),
  nicht(AE, B).
berechne(und(A, B), C):-
  berechne(A, AE),
  berechne(B, BE),
  und(AE, BE, C).
berechne(oder(A, B), C):-
  berechne(A, AE),
  berechne(B, BE),
  oder(AE, BE, C).
berechne(entweder_oder(A, B), C):-
  berechne(A, AE),
  berechne(B, BE),
  entweder_oder(AE, BE, C).
berechne(wenn_dann(A, B), C):-
  berechne(A, AE),
  berechne(B, BE),
  wenn_dann(AE, BE, C).
berechne(genau_dann(A, B), C):-
  berechne(A, AE),
  berechne(B, BE),
  genau_dann(AE, BE, C).
  
% Teil 3. Hilfspraedikate zur Zerlegung von Formeln
anzahlVariablen([],[],0).
anzahlVariablen([H|T],Variablen,N):- var(H),
                                     anzahlVariablen(T,TailVariablen,NT),
                                     memberVariable(H,TailVariablen),
                                     Variablen = TailVariablen,
                                     N is NT, !.
anzahlVariablen([H|T],Variablen,N):- var(H),
                                     anzahlVariablen(T,TailVariablen,NT),
                                     Variablen = [H|TailVariablen],
                                     N is NT + 1, !.
anzahlVariablen([_|T],Variablen,N):- anzahlVariablen(T,Variablen,N).

% test: anzahlVariablen([1,2,C,4,5,6,Z,U],Variablen,Anzahl).

% Sonderproblem: "member(X,[Y])" wird durch Unifikation wahr
% neues Praedikat fuer Variablenliste noetig:
memberVariable(X,[H|_]):- X == H, !.
memberVariable(X,[_|T]):- memberVariable(X,T).

% test: memberVariable(X,[3,5,6,F,H,i,O]).

flacheTermliste(C,[C]):- (atom(C); var(C)), !.
flacheTermliste(Term,Liste):- compound(Term), not(is_list(Term)),
                              Term =.. [Funktor|Anfangsliste],
                              flacheTermliste(Anfangsliste,Endliste),
                              append([Funktor],Endliste,Liste), !.
flacheTermliste([],[]).
flacheTermliste([H|T],Liste):- compound(H),
                               flacheTermliste(T,Tailliste),
                               flacheTermliste(H,Headliste),
                               append(Headliste,Tailliste,Liste), !.
flacheTermliste([H|T],Liste):- flacheTermliste(T,Tailliste),
                               append([H],Tailliste,Liste), !.

% test: flacheTermliste(wenn_dann(P,wenn_dann(E,D)),Liste).

verschiedeneVariablen(X,Y):- not(memberVariable(X,[Y])),
                             not(memberVariable(Y,[X])).