LogicLab1DONE

validateGoalWithLastRow([ProofHead|[]], Goal) :-
    [_,Fact,_] = ProofHead,
    Goal = Fact,!.
validateGoalWithLastRow([_|ProofTail], Goal) :-
    validateGoalWithLastRow(ProofTail, Goal),!.

main :-
    open('invalid28.txt',read,Stream),
    read(Stream,Premises),
    read(Stream,Goal),
    read(Stream,Proof),
    close(Stream),
    validateGoalWithLastRow(Proof,Goal),
    validateProof(Premises,Goal,Proof,[],false),!.

validateProof(_,_,[],_,_).
validateProof(Premises,Goal,[[RowNr,Fact,assumption]|ProofTail],VerifiedRows,true) :-
    validateProof(Premises,Goal,ProofTail,[[RowNr,Fact]|VerifiedRows],false).
validateProof(Premises,Goal,[[RowNr,Fact,Rule]|ProofTail],VerifiedRows,false) :-
    examineRow([RowNr,Fact,Rule],Premises,Goal,VerifiedRows),
    validateProof(Premises,Goal,ProofTail,[[RowNr,Fact]|VerifiedRows],false).
validateProof(Premises,Goal,[ProofHead|ProofTail],VerifiedRows,false) :-
    validateProof(Premises,Goal,ProofHead,VerifiedRows,true),
    [[RowNr,Fact,assumption]|NewTail] = ProofHead,
    last(ProofHead,[RowNr2,Fact2,_]),
    NewVerifiedRows = [[RowNr, RowNr2, Fact, Fact2] | VerifiedRows],
    validateProof(Premises,Goal,ProofTail,NewVerifiedRows,false).

% [RowNr,Fact,premise] check if the fact is amongst our Premises.
examineRow([_,Fact,premise],Premises,_,_) :-
    member(Fact,Premises),!.

% [RowNr,Fact,impel(X,Y)] check if the elimination of implication is performed correctly
% accordingly to " p, p->q", remember that p needs to be stated first as X and p->q second as Y.
% Implication Elimination
examineRow([_,Fact,impel(X,Y)],_,_,VerifiedRows) :-
    member([X,Q], VerifiedRows),!,
    member([Y,imp(Q,Fact)],VerifiedRows),!.

%Copy(X).
examineRow([_,Fact,copy(X)],_,_,VerifiedRows) :-
    member([X,Fact], VerifiedRows).

%Implication Introduction
examineRow([_, imp(P,Q), impint(X,Y)],_,_,VerifiedRows) :-
    member([X,Y,P,Q],VerifiedRows).

%Contradiction check, check if Q is at row X and then check if neg(Q) is at row Y.
%Negation Elimination
examineRow([_, cont, negel(X,Y)],_,_,VerifiedRows) :-
    member([X,Q], VerifiedRows),
    member([Y,neg(Q)], VerifiedRows).

%OREL Or Elimination
examineRow([_, Whatever, orel(A,B,C,D,E)],_,_,VerifiedRows) :-
    member([A, or(Q,R)], VerifiedRows),
    member([B,C,Q,Whatever], VerifiedRows),
    member([D,E,R,Whatever], VerifiedRows).

%PBC
examineRow([_, Q, pbc(X,Y)],_,_,VerifiedRows) :-
    member([X,Y,neg(Q),cont], VerifiedRows).


/*fffffffffffffffffffffffffffffffffffffffffffff*/

%And Introduction
examineRow([_, and(P,Q), andint(X,Y)],_,_,VerifiedRows) :-
    member([X, P], VerifiedRows),
    member([Y, Q], VerifiedRows).

%And elimination 1
examineRow([_, P, andel1(X)],_,_,VerifiedRows) :-
    member([X, and(P,_)], VerifiedRows).

%And Elimination 2
examineRow([_, Q, andel2(X)],_,_,VerifiedRows) :-
    member([X, and(_,Q)], VerifiedRows).

%Or Introduction 1
examineRow([_, or(P,_), orint1(X)],_,_,VerifiedRows) :-
    member([X, P], VerifiedRows).

%Or introduction 2
examineRow([_, or(_,Q), orint2(X)],_,_,VerifiedRows) :-
    member([X, Q], VerifiedRows).

%LEM
examineRow([_, or(Q,neg(Q)), lem],_,_,_).

%MT
examineRow([_, neg(Q), mt(X,Y)],_,_,VerifiedRows) :-
    member([X, imp(Q,P)], VerifiedRows),
    member([Y, neg(P)], VerifiedRows).

%negation introduction
examineRow([_, neg(P), negint(X,Y)],_,_,VerifiedRows) :-
    member([X,Y,P,cont], VerifiedRows).

examineRow([_, _, contel(X)],_,_,VerifiedRows) :-
    member([X, cont], VerifiedRows).

examineRow([_, neg(neg(P)), negnegint(X)],_,_,VerifiedRows) :-
    member([X, P], VerifiedRows).

examineRow([_, P, negnegel(X)],_,_,VerifiedRows) :-
    member([X, neg(neg(P))], VerifiedRows).