Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- validateGoalWithLastRow([ProofHead|[]], Goal) :-
- [_,Fact,_] = ProofHead,
- Goal = Fact,!.
- validateGoalWithLastRow([_|ProofTail], Goal) :-
- validateGoalWithLastRow(ProofTail, Goal),!.
- verify(InputFileName) :-
- see(InputFileName),
- read(Premises),
- read(Goal),
- read(Proof),
- seen,
- validateGoalWithLastRow(Proof,Goal),
- validateProof(Premises, Goal, Proof,[],false),!.
- validateProof(_,_,[],_,_).
- validateProof(Premises,Goal,[[RowNr,Fact,assumption]|ProofTail],VerifiedRows,true) :-
- integer(RowNr),
- validateProof(Premises,Goal,ProofTail,[[RowNr,Fact]|VerifiedRows],false).
- validateProof(Premises,Goal,[[RowNr,Fact,Rule]|ProofTail],VerifiedRows,false) :-
- integer(RowNr),
- 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).
Advertisement
Add Comment
Please, Sign In to add comment
