/*
Autor: MB
Datum: MAY 2016
Entscheidungsverfahren fuer LP ausgehend von Wahrheitsbedingungen.
Analog zum entsprechenden Vorgehen in der Aussagenlogik (a.a.O.).
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.
*/

:- consult('Logikhilfspraedikate').

% vgl. zum Vorgehen die entsprechenden Bemerkungen beim aussagenlogischen Fall

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).

% 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).