
%% Das Überprüfen auf Variabale muss in vbl, frei subst
%% vernünftig geregelt werden.
%% 
%% 
%% 

%% 
%% 
%%  
%% 
%% 



%                           Beweispruefer
%
%                             Juni 2005
%
% Das vorliegende Programm "Pruefer" ist in der Lage, aussagenlogische Beweistexte,
% die in dem Textsatzprogramm TeXmacs geschrieben sind, auf ihre Richtigkeit
% zu überprüfen. Die TeXmacs-Texte bestehen aus einer Folge von
% quantorenfreien Aussagen, in denen die Einführung einer Annahme durch
% das Wort "Sei" und die Folgerung aus einer Annahme durch "Also" notiert
% wird.
%
% Die Texte werden in der Datei ~/test.tm abgespeichert. Diese Datei wird durch das
% Programm "Pruefer" gelesen und auf die Beweisregeln überprüft. "Pruefer" ist ein
% Prolog-Programm, das unter dem verbreiteten SWI-Prolog läuft.
%
% "Pruefer" gliedert sich in drei Teile:
%
%  1. Implementation der Aussagenlogik; Aussagen sind Listen
%       von Tokens "(", ")", "neg" für die Negation, "wedge" für die 
%       Konjunktion, ..., "alpha", "beta", ... für die aussagenlogischen
%       Variablen.
%
%  2. Bearbeitung der Eingabe aus dem Programm TeXmacs; dabei sind 
%       Formatierungselemente zu entfernen und eine Liste von Aussagen
%       entsprechend dem obigen Format zu erzeugen.
%
%  3. Extraktion der jeweils gültigen Voraussetzungen im Beweistext ("Lesen").
% 
%  4. Überprüfung dieser Liste auf logische Korrektheit; die Liste wird
%       gelesen und es werden insbesondere die jeweils gueltigen 
%       Voraussetzungen extrahiert; der eingegebene Beweis ist korrekt, wenn
%       jede Beweiszeile aus den jeweiligen Voraussetzungen durch einen
%       logischen Schluss gebildet werden kann.


pruefen :-
    einlesen(Text),
    uebersetzen(Text,Text_intern),
    lesen(Text_intern,Zeiger,Voraussetzungen,Frei),
    beweis1(Text_intern,Zeiger,Voraussetzungen).


%      1. Formalisierung von Aussagen und Texten  
%
% Implementation der Aussagenlogik
% entsprechend der Vorlesung
% Logik und diskrete Strukturen
% im Sommersemester 2005

% Als aussagenlogische Variablen werden alle kleinen griechischen
% Buchstaben benutzt. Sie werden als Prolog-Atome implementiert.
% Die Schreibweisen entsprechen dem internen Format von TeXmacs.

% Die aussagenlogische Verknüpfungen Negation, Konjunktion (/\),
% Disjunktion (\/), Implikation (->) und Äquivalenz (<->):

neg. wedge. vee. rightarrow. leftrightarrow.

% Die Sprache der Aussagenlogik

% Zeichenreihen der Aussagenlogik werden
% als Listen von Atomen repräsentiert.
% Die Analyse der Zeichenreihen (Parsing) erfolgt
% aus Gründen der Effizienz
% mit Hilfe von Differenzlisten.

% Als prädikatenlogische Variablen vereinbaren wir alle kleinen lateinischen
% Buchstaben. Das Prädikat vari(X,Y,T) sagt aus, das die Liste X mit einer
% Variablen beginnt, Y ist der Rest der Liste. In T wird die gefundene
% Variable ausgegeben. Die kleinen lateinischen Buchstaben sollen Atome
% im Sinne von Prolog werden, daher werden sie alle als richtig "behauptet".

a. b. c. d. e. f. g. h. i. j. k. l. m. n. o. p. q. r. s. t. u. v. w.
x. y. z.

varsymb(V) :- member(V,[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z]).

vari([V|T],T,V) :- varsymb(V).

% Atomare Aussagen sind relationale atomare Aussagen der Arten 
% x=y, x<y, x<=y und x in y sowie aussagenlogische Variablen und Konstanten. 
% Das Prädikat atomare_aussage(X,Y,Z) sagt aus, dass die Liste X
% mit einer atomaren Aussage Z beginnt und der Rest von X gleich der Liste
% Y ist:

eq. less. leq. in.

% Relationen werden intern durch die folgenden atome dargestellt:

relint(R) :- member(R,[eq,less,leq,in]).

relation(['='|S],S,eq).
relation(['less'|S],S,less).
relation(['leqslant'|S],S,leq).
relation(['in'|S],S,in).
    

atomare_aussage(X,Y,[V1,R,V2]) :-
    vari(X,A,V1), relation(A,B,R),vari(B,Y,V2).

alpha. beta. gamma. delta. varepsilon. epsilon.
zeta. eta. theta. vartheta. iota. kappa. lambda.
mu. nu. xi. omicron. pi. varpi. rho. varrho. sigma.
varsigma. tau. upsilon. phi. varphi. chi. psi. omega.

% Die aussagenlogische Konstanten für wahr und falsch:

top. bot.


atomare_aussage([H|T],T,H)
    :- member(H,[alpha, beta, gamma,
		  delta, varepsilon, epsilon, zeta, eta,
		  theta, vartheta, iota, kappa, lambda,
		  mu, nu, xi, omicron, pi, varpi, rho,
		  varrho, sigma, varsigma, tau, upsilon,
		  phi, varphi, chi, psi, omega, top, bot]).

% Aussagen. Das Prädikat aussage(X,Y,T) sagt aus, dass die Liste X
% mit einer Aussage beginnt und der Rest von X gleich der Liste
% Y ist. Das Prädikat gibt weiterhin einen Strukturbaum T für die
% Aussage aus, der die weitere Verarbeitung effizienter macht.
% Für die Negation zum Beispiel gilt z.B.
%   aussage(['(', neg, phi,')', bla, bla],[bla,bla],[not,T]),
% wobei T der Strukturbaum für die Aussage phi ist.
%
% Wir führen Prolog-Atome für den Aufbau der Strukturbäume ein:

not. and. or. then. iff. let. thus. all. ex.

aussage(X,Y,T) :- atomare_aussage(X,Y,T).
% Negation
aussage(X,Y,[not,T]) :- X=[neg|U], aussage(U,Y,T).

% Konjunktion
aussage(X,Y,[T1,and,T2]) 
    :- X=['('|A], aussage(A,B,T1), B=[wedge|C], aussage(C,D,T2), D=[')'|Y].

% Disjunktion

aussage(X,Y,[T1,or,T2]) 
    :- X=['('|A], aussage(A,B,T1), B=[vee|C], aussage(C,D,T2), D=[')'|Y].

% Implikation
aussage(X,Y,[T1,then,T2]) 
    :- X=['('|A], aussage(A,B,T1), B=[rightarrow|C], aussage(C,D,T2), D=[')'|Y].

% Äquivalenz
aussage(X,Y,[T1,iff,T2])
    :- X=['('|A], aussage(A,B,T1), B=[leftrightarrow|C], aussage(C,D,T2), D=[')'|Y].

% Universelle Aussagen
aussage(X,Y,[all,V,A])
    :- X=['forall',V|U], aussage(U,Y,A).

% Existenzielle Aussagen
aussage(X,Y,[ex,V,A])
    :- X=['exists',V|U], aussage(U,Y,A).

% Für die Behandlung von Termen und Quantoren ist die Bestimmung der
% der Menge der Variablen und der freien Variablen in einer Aussage
% wichtig. Wir gehen von Aussagen im internen Format aus.

vbl([V1,R,V2],Z) :-
    varsymb(V1), relint(R),varsymb(V2), list_to_set([V1,V2],Z).

vbl(A,[])
    :- member(A,[alpha, beta, gamma,
		  delta, varepsilon, epsilon, zeta, eta,
		  theta, vartheta, iota, kappa, lambda,
		  mu, nu, xi, omicron, pi, varpi, rho,
		  varrho, sigma, varsigma, tau, upsilon,
		  phi, varphi, chi, psi, omega, top, bot]).

vbl([not,T],Z) :- vbl(T,Z).

vbl([T1,and,T2],Z) 
    :- vbl(T1,X), vbl(T2,Y), union(X,Y,Z).
vbl([T1,or,T2],Z) 
    :- vbl(T1,X), vbl(T2,Y), union(X,Y,Z).
vbl([T1,then,T2],Z) 
    :- vbl(T1,X), vbl(T2,Y), union(X,Y,Z).
vbl([T1,iff,T2],Z) 
    :- vbl(T1,X), vbl(T2,Y), union(X,Y,Z).

vbl([all,V,A],Z)
    :- vbl(A,X), union(X,[V],Z).
vbl([ex,V,A],Z)
    :- vbl(A,X), union(X,[V],Z).

frei([V1,R,V2],Z) :- 
    varsymb(V1), relint(R), varsymb(V2), vbl([V1,R,V2],Z).

frei(A,[])
    :- member(A,[alpha, beta, gamma,
		  delta, varepsilon, epsilon, zeta, eta,
		  theta, vartheta, iota, kappa, lambda,
		  mu, nu, xi, omicron, pi, varpi, rho,
		  varrho, sigma, varsigma, tau, upsilon,
		  phi, varphi, chi, psi, omega, top, bot]).

frei([not,T],Z) :- frei(T,Z).

frei([T1,and,T2],Z) 
    :- frei(T1,X), frei(T2,Y), union(X,Y,Z).
frei([T1,or,T2],Z) 
    :- frei(T1,X), frei(T2,Y), union(X,Y,Z).
frei([T1,then,T2],Z) 
    :- frei(T1,X), frei(T2,Y), union(X,Y,Z).
frei([T1,iff,T2],Z) 
    :- frei(T1,X), frei(T2,Y), union(X,Y,Z).

frei([all,V,A],Z)
    :- frei(A,X), delete(X,V,Z).
frei([ex,V,A],Z)
    :- frei(A,X), delete(X,V,Z).

% Wir formalisieren jetzt, was eine legitime simultane Substitution einer Folge
% von Variablen durch andere Variable ist. Wir beginnen mit einer kleinen
% Formalisierung von Funktionen als Mengen geordneter Paare.

funct(F,X,Y) :- member([X,Y],F).
funct(F,X,X) :- defi(F,D), \+member(X,D).

restr([],A,[]).
restr([[X,Y]|T],A,[[X,Y]|R]) :- member(X,A), restr(T,A,R).
restr([[X,Y]|T],A,R) :- \+(member(X,A)), restr(T,A,R).

bild([],[]).
bild([[X,Y]|T],[Y|B]) :- bild(T,B).

defi([],[]).
defi([[X,Y]|T],[X|D]) :- defi(T,D).

 

subst([V1,R,V2],F,[W1,R,W2]) :-
    varsymb(V1), relint(R), varsymb(V2), funct(F,V1,W1), funct(F,V2,W2).

subst(A,F,A)
    :- member(A,[alpha, beta, gamma,
		  delta, varepsilon, epsilon, zeta, eta,
		  theta, vartheta, iota, kappa, lambda,
		  mu, nu, xi, omicron, pi, varpi, rho,
		  varrho, sigma, varsigma, tau, upsilon,
		  phi, varphi, chi, psi, omega, top, bot]).

subst([not,T],F,[not,U]) :- subst(T,F,U).

subst([T1,and,T2],F,[U1,and,U2]) 
    :- subst(T1,F,U1), subst(T2,F,U2).
subst([T1,or,T2],F,[U1,or,U2]) 
    :- subst(T1,F,U1), subst(T2,F,U2).
subst([T1,then,T2],F,[U1,then,U2]) 
    :- subst(T1,F,U1), subst(T2,F,U2).
subst([T1,iff,T2],F,[U1,iff,U2]) 
    :- subst(T1,F,U1), subst(T2,F,U2).

subst([all,V,A],F,[all,V,B])
    :- frei([all,V,A],Frei), restr(F,Frei,F1), bild(F1,Z), 
       \+member(V,Z), subst(A,F1,B).
subst([all,V,A],F,[all,W,B])
    :- frei([all,V,A],Frei), restr(F,Frei,F1), bild(F1,Z), vbl(A,Z1), 
       \+member(W,Z), \+member(W,Z1), union(F1,[[V,W]],F2), subst(A,F2,B).

subst([ex,V,A],F,[ex,V,B])
    :- frei([ex,V,A],Frei), restr(F,Frei,F1), bild(F1,Z), 
       \+member(V,Z), subst(A,F1,B).
subst([ex,V,A],F,[ex,W,B])
    :- frei([ex,V,A],Frei), restr(F,Frei,F1), bild(F1,Z), vbl(A,Z1), 
       \+member(W,Z), \+member(W,Z1), union(F1,[[V,W]],F2), subst(A,F2,B).


% Mathematische Texte 
% sind Listen von (Text-)Zeilen

% (Text-)Zeilen sind Aussagen, oder Aussagen die als
% Annahme oder Schlussfolgerung eingefuehrt werden, jeweils 
% gefolgt von einem Punkt (.).
 
zeile(X,Y,T) :- aussage(X,A,T), A=['.'|Y].
zeile(X,Y,[let,T]) :- X=['Sei'|A], aussage(A,B,T), B=['.'|Y].
zeile(X,Y,[thus,T]) :- X=['Also'|A], aussage(A,B,T), B=['.'|Y].

% Texte sind Listen von (Text-)Zeilen:

text([]).
text([H|T]) :- zeile(H,[]), text(T).



%
%          2. Einlesen von TeXmacs-Dateien
%


% Das Program "einlesen" liest die TeXmacs-Datei 'test.tm' und erzeugt hieraus
% einen Beweistext. Die Datei wird mit einem einfachen Tokenizer in Wörter
% und Satzzeichen zerlegt. Der formale Beweis steht im Format "emphasize".
% Alle Wörter außerhalb dieses Bereichs werden ignoriert. Die Wörter aus dem
% formalen Beweis werden im Sinne der obigen Syntaxdefinitionen bearbeitet und
% als Beweistext formatiert.
   
einlesen(Liste)  :-
    open('test.tm',read,In),
    liste(In,Liste1),
    close(In),
    clean1(Liste1,[_|Liste2]),
    clean2(Liste2,Liste3),
    append(Liste4,Liste3,Liste2),
    reverse(Liste4,Liste).


% Das Programm "liste" macht aus den akzeptierten Beweiszeilen eine Liste
% von Beweiszeilen.

liste(In,Liste) :-
    get0(In,Ch),
    (Ch= (-1) -> Liste = []
     ;
     sentence_tokens(In,Ch,Words),
     Liste = [Words|Liste1],
     liste(In,Liste1)).

% Dies ist ein üblicher Tokenizer, der mit einem "look-ahead" von einem Zeichen
% arbeitet.

sentence_tokens(In,Words) :-
    get0(In,Ch),
    sentence_tokens(In,Ch,Words).

sentence_tokens(In,Ch,Words) :-
    ( Ch= (-1) -> Words = []
    ; Ch=46 -> Words = ['.']
    ; alphabetic(Ch) ->
      get_letters(In,Ch,Ch1,Letters),
      atom_codes(Word, Letters),
      delete(Letters,47,Letters1),
      delete(Letters1,60,Letters2),
      delete(Letters2,92,Letters3),
      atom_codes(Word1,Letters3),
      (Word='<em' -> Words=[Word]
      ;Word='</em' -> Words=[Word]  
      ;Word='<with' -> Words=Words1, sentence_tokens(In,Ch1,Words1)
      ;Word=mode -> Words=Words1, sentence_tokens(In,Ch1,Words1)
      ;Word=math -> Words=Words1, sentence_tokens(In,Ch1,Words1)
      ;Letters3=[] -> Words=Words1, sentence_tokens(In,Ch1,Words1)
      ;Words=[Word1|Words1], sentence_tokens(In,Ch1,Words1))
    ; Ch=40 ->
      Words=['('|Words1],
      get0(In,Ch1),
      sentence_tokens(In,Ch1,Words1)
    ; Ch=41 ->
      Words=[')'|Words1],
      get0(In,Ch1),
      sentence_tokens(In,Ch1,Words1)
    ; Ch=61 ->
      Words=['='|Words1],
      get0(In,Ch1),
      sentence_tokens(In,Ch1,Words1)
    ; get0(In,Ch1),
      sentence_tokens(In,Ch1,Words)
    ).

alphabetic(Ch) :-
    (Ch >= 0'a, Ch=< 0'z ->
     true
    ;
     Ch >= 0'A, Ch =< 0'Z ->
     true
    ;
     Ch = 60 -> true  % <
    ;
     Ch = 47 -> true  % >
%    ;
%     Ch = 92 -> true % backslash
    ).

get_letters(In,Ch0,Ch,Letters) :-
    ( alphabetic(Ch0) ->
        Letters = [Ch0|Letters1],
        get0(In,Ch1),
        get_letters(In,Ch1,Ch,Letters1)

      ; Ch=Ch0,
        Letters = []
      ).

% Einige Hilfsprogramme zum Säubern der Ausgabe von "liste".

clean1([],[]).
clean1([H|T],T1) :- (member('em',H) -> T1=[H|T]
		     ; clean1(T,T1)).

clean2([],[]).
clean2([H|T],T1) :- (H=['</em'] -> T1=[H|T]
		     ; clean2(T,T1)).
    


%
%      Übersetzen der Eingabe in das interne Format
%


uebersetzen([],[]).
uebersetzen([Zeile|Liste],[Zeile_intern|Liste_intern]) :-
       zeile(Zeile,[],Zeile_intern),
       uebersetzen(Liste,Liste_intern).
       

%              
%      Lesen des internen Textes im Hinblick auf die Argumentationsstruktur
%

% Entsprechend der Definition 5.1. 
% der Vorlesung wird rekursiv eine Folge von Zeigern,
% eine Folge von lokalen Voraussetzungen und die
% Menge der jeweils freien (oder schon belegten) Variablen definiert.
% Dies kann als "Lesen" des Textes aufgefasst werden.
% Die Zeiger werden in einer Liste von Zeigern zusammengefasst.
% Die Voraussetzungen werden in eine Liste geschrieben, deren 
% Elemente wiederum Listen von Aussagen sind, die momentan gelten.
% Die _Menge_ der jeweils zur Verfügung stehenden Aussagen
% wird also durch eine _Liste_ implementiert.

% Für die Universalisierung von Implikationen nach Schließen eines
% Rahmens wird eine Hilfsfunktion imp eingeführt, die Quantoren for
% eine gegebene Aussage schreibt.

univ(A,[],A).
univ(A,[X|Var],[all,X,B]) :- univ(A,Var,B).

lesen([],[],[],[]).
lesen([Z],[-1],[[]],[[]]).
lesen([Zl,[let,A]|Text],[Z1,Z2|Zeiger],[[A|V2],V2|Vss],[F1,F2|Fs]) :-
    length(Text,Z1),
    lesen([[let,A]|Text],[Z2|Zeiger],[V2|Vss],[F2|Fs]),
    frei(A,S), union(F2,S,F1).
lesen([Zl,[thus,B]|Text], [Z1,Z2|Zeiger],[[Univ|V],V2|Vss],[F1,F2|Fs]) :-
    lesen([[thus,B]|Text], [Z2|Zeiger], [V2|Vss],[F2|Fs]),
    length(Zeiger,Ln), K is Ln-1-Z2,
    nth0(K,Zeiger,Z1),
    nth0(K,Vss,V),
    nth0(K,Text,[let,top]),
    frei(B, Frei1),
    nth0(K,Fs,F1),
    subtract(Frei1,F1,Frei2),
    univ(B,Frei2,Univ).
lesen([Zl,[thus,B]|Text], [Z1,Z2|Zeiger],[[Univ|V],V2|Vss],[F1,F2|Fs]) :-
    lesen([[thus,B]|Text], [Z2|Zeiger], [V2|Vss],[F2|Fs]),
    length(Zeiger,Ln), K is Ln-1-Z2,
    nth0(K,Zeiger,Z1),
    nth0(K,Vss,V),
    nth0(K,Text,[let,A]),
    frei([A,then,B], Frei1),
    nth0(K,Fs,F1),
    subtract(Frei1,F1,Frei2),
    univ([A,then,B],Frei2,Univ).
lesen([Zl1,A|Text], [Z2,Z2|Zeiger],[[A|V2],V2|Vss],[F1,F2|Fs]) :-
    lesen([[let,A]|Text], [Z2|Zeiger], [V2|Vss],[F2|Fs]),
    frei(A,S), union(F2,S,F1).


%
%    4. Beweis-Prüfung
%

% Ein formaler Beweis ist korrekt, wenn jede Behauptung aus 
% den momentan zur Verfügung stehenden Voraussetzungen mit Hilfe von Regeln
% erzeugt werden kann. Wir führen zunächst die Schlussregeln entsprechend
% dem Kapitel 5 der Vorlesung ein. 

% Eine Regel erlaubt aus der Menge der gerade zur Verfügung stehenden Voraussetzungen
% mit Hilfe syntaktischer Operationen formale Schlüsse. Die syntaktischen
% Operationen entsprechen der in 1. eingeführten Sprache.

% Kopieren einer Voraussetzung

schluss(X,Vss) :- member(X,Vss).

% und-Regeln

% und-Einfuehrung
schluss([F,and,G],Vss) :- 
    member(F,Vss), member(G,Vss).

% und-Elimination
schluss(A,Vss) :- 
    member([A,and,B],Vss).
schluss(B,Vss) :- 
    member([A,and,B],Vss).

% impliziert-Regel, impliziert-Elimination
schluss(B,Vss) :-
    member([A,then,B],Vss), member(A,Vss).

% aequivalent-Regeln
schluss([A,iff,B],Vss) :-
    member([[A,then,B],and,[B,then,A]],Vss).
schluss([[A,then,B],and,[B,then,A]],Vss) :-
    member([A,iff,B],Vss).

% Oder-Regeln

% Oder-Einfuehrung
schluss([A,or,B],Vss) :-
    member(A,Vss).
schluss([A,or,B],Vss) :-
    member(B,Vss).

% oder-Elimination, Fallunterscheidung
schluss(C,Vss) :-
    member([A,then,C],Vss),
    member([B,then,C],Vss),
    member([A,or,B],Vss).

% Konstanten-Regeln

% Top-Einfuehrung
schluss(top,Vss).

% Bottom-Elimination
schluss(A,Vss) :- member(bot,Vss).

% nicht-Regeln

% nicht A ist eine Abkuerzung fuer A impliziert falsch:
schluss([not,A],Vss) :-
    member([A,then,bot],Vss).
schluss([A,then,bot],Vss) :- 
    member([not,A],Vss).

% Widerspruchs-Regel
schluss(A,Vss) :- 
    member([[not,A],then,bot],Vss).

% All-Regel, All-Elimination, Instanzierung
schluss(A,Vss) :-
    member([all,X,B],Vss), frei(A,Frei), member(Y,Frei),
    subst(B,[[X,Y]],A).

% Gleichheits-Regeln

% Reflexivität
schluss([X,eq,X],Vss) :- varsymb(X).

% Symmetrie
schluss([X,eq,Y],Vss) :- member([Y,eq,X],Vss).

% Transitivität
schluss([X,eq,Z],Vss) :- member([X,eq,Y],Vss), member([Y,eq,Z],Vss).

% Substitutionsregel
schluss(A,Vss) :-
    member([X,eq,Y],Vss), member(B,Vss), subst(B,[[X,Y]],A).

% Beweise

beweis1([],[],[]).
beweis1([[let,A]|Text],[Z|Zeiger],[V|Vss]) :-
    beweis1(Text,Zeiger,Vss).
beweis1([[thus,A]|Text],[Z|Zeiger],[V|Vss]) :-
    schluss(A,V), beweis1(Text,Zeiger,Vss).
beweis1([A|Text],[Z|Zeiger],[V|Vss]) :-
    schluss(A,V), beweis1(Text,Zeiger,Vss).


beweis(Text) :- lesen(Text,Zeiger,Vss),beweis1(Text,Zeiger,Vss).

qed([T|Text]) :- 
    aussage(T), lesen([T|Text],[-1|Zeiger],Vss), beweis1([T|Text],[-1|Zeiger],Vss).

concat([],L,L).
concat([H|T],L,[H|L3]) :- concat(T,L,L3).

