PrologLab1

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

main :-
    open('valid05.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.
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.
examineRow([_, cont, negel(X,Y)],_,_,VerifiedRows) :-
    member([X,Q], VerifiedRows),
    member([Y,neg(Q)], VerifiedRows).

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

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