Untitled

verify(InputFileName) :- see(InputFileName),
read(Prems), read(Goal), read(Proof),
seen,
valid_proof(Prems, Goal, Proof).

valid_proof(Prems, G, Proof) :- findlast(Proof, _, [_|[G|_]]), check_rules(Prems, Proof, Proof, 1).

findlast([X], [], X).
findlast([H | T], [H | N], X) :- findlast(T, N, X).

check_rules(_, [[]], _, _).
check_rules(_, [], _, _).
check_rules(Prems, [[H|H1]|T2], Proof, Count) :- get_rule(Proof, Count, [R|_]), (R == premise, get_prop(Proof, Count, Prop), check_premise(Prop, Prems) ;
                                              R == assumption, check_assumption(Proof, Count) ;
                                              R = copy(_), get_pred_of_prop(R, [_|[Num|_]]), copy(Num, Count, Proof) ;
                                              R = andint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), andint(A, B, Count, Proof) ;
                                              R = andel1(_), get_pred_of_prop(R, [_|[Num|_]]), andel1(Num, Count, Proof) ;
                                              R = andel2(_), get_pred_of_prop(R, [_|[Num|_]]), andel2(Num, Count, Proof) ;
                                              R = orint1(_), get_pred_of_prop(R, [_|[Num|_]]), orint1(Num, Count, Proof) ;
                                              R = orint2(_), get_pred_of_prop(R, [_|[Num|_]]), orint2(Num, Count, Proof) ;
                                              R = orel(_, _, _, _, _), get_pred_of_prop(R, [_|[X|[A|[B|[C|[D|_]]]]]]), orel(X, A, B, C, D, Count, Proof) ;
                                              R = impint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), impint(A, B, Count, Proof) ;
                                              R = impel(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), impel(A, B, Count, Proof) ;
                                              R = negint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), negint(A, B, Count, Proof) ;
                                              R = negel(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), negel(A, B, Count, Proof) ;
                                              R = contel(_), get_pred_of_prop(R, [_|[Num|_]]), contel(Num, Count, Proof) ;
                                              R = negnegint(_), get_pred_of_prop(R, [_|[Num|_]]), negnegint(Num, Count, Proof) ;
                                              R = negnegel(_), get_pred_of_prop(R, [_|[Num|_]]), negnegel(Num, Count, Proof) ;
                                              R = mt(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), mt(A, B, Count, Proof) ;
                                              R = pbc(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), pbc(A, B, Count, Proof) ;
                                              R == lem, lem(Count, Proof)), !,
                                              C1 is Count + 1,
    										  ((list_empty(H1) ; get_list_head(H1, H2), not(is_list(H2))), check_rules(Prems, T2, Proof, C1) ;
                                              nested_list(H), get_tail(H, T), check_rules(Prems, [[T|H1]|T2], Proof, C1) ;
                                              get_list_head(H1, H2), is_list(H2), check_rules(Prems, [H1|T2], Proof, C1)).

list_empty([]).
nested_list(A) :- A = [[_]|_] ; A = [_|[_]].
get_tail([_|T], T).

check_assumption(Proof, Num) :- row_depth(Proof, Num, Depth), is_list(Depth), findlast(Depth, [_|_], 1).

check_premise(Result, H) :- Result == H.
check_premise(Result, [H|T]) :- Result == H ; check_premise(Result, T).


find_row([[[[H|T]|_]|_]|_], H, [H|T]).
find_row([[[H|T]|_]|_], H, [H|T]).
find_row([[H|T]|_], H, [H|T]).
find_row([[[Hf|Tf]|T2]|[[H|T3]|T4]], Num, Result) :- less_than(H, Num), find_row([[H|T3]|T4], Num, Result) ; find_row([[Hf|Tf]|T2], Num, Result).
find_row([[_|[T1|_]]|T2], Num, Result) :- (not(is_list(T1)), find_row(T2, Num, Result) ; find_row([T1|T2], Num, Result)).

less_than(H, Num) :- is_list(H), get_list_head(H, P), less_than(P, Num) ; not(is_list(H)), H =< Num.

get_list_head([H|_], H).

depth(X, [X|_], [C], C).
depth(X, [H|_], [C|D], C) :- depth(X, H, D, 1).
depth(X, [_|T], D, C) :- C1 is C+1, depth(X, T, D, C1).

row_depth(Proof, Row, Depth) :- find_row(Proof, Row, FullRow), depth(FullRow, Proof, Depth, 1).

find_row_and_depth(Proof, Num, Row, Depth) :- find_row(Proof, Num, Row), row_depth(Row, Proof, Depth).

get_prop(Proof, Num, Prop) :- find_row(Proof, Num, [_|[Prop|_]]).

get_rule(Proof, Num, Rule) :- find_row(Proof, Num, [_|[_|Rule]]).

get_pred_of_prop(L, List) :- L =.. List.

lesser_depth([_], _).
lesser_depth([Ha|Ta], [Hb|Tb]) :- Ha is Hb, lesser_depth(Ta, Tb).

valid_depth(Proof, RowA, RowB) :- row_depth(Proof, RowA, DepthA), row_depth(Proof, RowB, DepthB),
                            lesser_depth(DepthA, DepthB).
valid_depth_box(Proof, DepthBox, RowB) :- row_depth(Proof, RowB, DepthB),
                            lesser_depth(DepthBox, DepthB).

check_box(Proof, Start, End, R) :- Start =< End, get_rule(Proof, Start, [Rule|_]), Rule == assumption,  row_depth(Proof, Start, [Hs|Ts]), row_depth(Proof, End, [He|Te]), findlast([Hs|Ts], Rs, _), findlast([He|Te], Re, _), Rs = Re, C1 is End+1, row_depth(Proof, C1, [H|T]), findlast([H|T], Rc, _), not(Rc = Re), findlast([Hs|Ts], R, _).

copy(A, B, Proof) :-
    A < B,
    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    PropA==PropB, valid_depth(Proof, A, B).

andint(A, B, C, Proof) :-
    A < C,
    B < C,
    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    get_prop(Proof, C, PropC),

    and(PropA, PropB) = PropC,
    valid_depth(Proof, A, C), valid_depth(Proof, B, C).

andel1(A, B, Proof) :-
    A < B,

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),

    get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),

    PredLeftA = PropB,
    valid_depth(Proof, A, B).

andel2(A, B, Proof) :-
    A < B,

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),

    get_pred_of_prop(PropA, [_ | [_ | [PredRightA | _]]]),

    PredRightA = PropB,
    valid_depth(Proof, A, B).

orint1(A, B, Proof) :-
    A < B,

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),

    get_pred_of_prop(PropB, [_ | [PredLeftB | _]]),

    PredLeftB = PropA,
    valid_depth(Proof, A, B).

orint2(A, B, Proof) :-
    A < B,

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),

    get_pred_of_prop(PropB, [_ | [_ | [PredRightB | _]]]),

    PredRightB = PropA,
    valid_depth(Proof, A, B).

orel(X, A, B, C, D, E, Proof) :-
    A < B,
    C < D,
    B < E,
    D < E,
    X < E,

    check_box(Proof, A, B, Il1),
    valid_depth_box(Proof, Il1, E),

    check_box(Proof, C, D, Il2),
    valid_depth_box(Proof, Il2, E),

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    get_prop(Proof, C, PropC),
    get_prop(Proof, D, PropD),
    get_prop(Proof, X, PropX),

    PropB = PropD,
    (PropX = or(PropA, PropC) ; PropX = or(PropC, PropA)).

impint(A, B, C, Proof) :-
    A =< B,
    B < C,

    check_box(Proof, A, B, Indexlist),
    valid_depth_box(Proof, Indexlist, C),

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    get_prop(Proof, C, PropC),

    get_pred_of_prop(PropC, [_ | [PredLeftC | [PredRightC | _]]]),

    PropA = PredLeftC,
    PropB = PredRightC.

impel(A, B, C, Proof) :-
    A < C,
    B < C,

    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    get_prop(Proof, C, PropC),

    ((get_pred_of_prop(PropB, [_ | [PredLeftB | [PredRightB | _]]]),
    PropA = PredLeftB,
    PropC = PredRightB) ;
    (get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),
    PropB = PredLeftA,
    PropC = PredRightA)),

    valid_depth(Proof, A, C), valid_depth(Proof, B, C).

negint(A, B, C, Proof) :-
      A < B,
      A < C,
      B < C,

      check_box(Proof, A, B, Indexlist),
      valid_depth_box(Proof, Indexlist, C),

      get_prop(Proof, A, PropA),
      get_prop(Proof, B, PropB),
      get_prop(Proof, C, PropC),

      get_pred_of_prop(PropC, [_ | [PredLeftC | _]]),

      PropA = PredLeftC,
      PropB = cont.

negel(A, B, C, Proof) :-
      A < C,
      B < C,

      get_prop(Proof, A, PropA),
      get_prop(Proof, B, PropB),
      get_prop(Proof, C, PropC),

      ((PropB = neg(_), get_pred_of_prop(PropB, [_ | [PredLeftB | _]]),
      PropA = PredLeftB) ;
      (PropA = neg(_), get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),
      PropB = PredLeftA)),

      PropC = cont,
      valid_depth(Proof, A, C), valid_depth(Proof, B, C).

contel(A, B, Proof) :-
      A < B,

      get_prop(Proof, A, PropA),

      PropA = cont,
      valid_depth(Proof, A, B).

negnegint(A, B, Proof) :-
      A < B,

      get_prop(Proof, A, PropA),
      get_prop(Proof, B, PropB),

      get_pred_of_prop(PropB, [_|[PredLeftB|_]]),
      get_pred_of_prop(PredLeftB, [_|[PredLeftBB|_]]),

      PropA = PredLeftBB,
      valid_depth(Proof, A, B).

negnegel(A, B, Proof) :-
      A < B,

      get_prop(Proof, A, PropA),
      get_prop(Proof, B, PropB),

      get_pred_of_prop(PropA, [_|[PredLeftA|_]]),
      get_pred_of_prop(PredLeftA, [_|[PredLeftAA|_]]),

      PropB = PredLeftAA.

mt(A, B, C, Proof) :-
      A < C,
      B < C,

      get_prop(Proof, A, PropA),
      get_prop(Proof, B, PropB),
      get_prop(Proof, C, PropC),

      get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),

      neg(PredLeftA) = PropC,
      neg(PredRightA) = PropB,
      valid_depth(Proof, A, C), valid_depth(Proof, B, C).

pbc(A, B, C, Proof) :-
      A < B,
      B < C,

      check_box(Proof, A, B, Indexlist),
      valid_depth_box(Proof, Indexlist, C),

      get_prop(Proof, A, PropA),
      get_prop(Proof, B, PropB),
      get_prop(Proof, C, PropC),

      (PropC = neg(PropA) ;
      get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),
      PropC = PredLeftA),
      PropB == cont.

lem(A, Proof) :-

    get_prop(Proof, A, PropA),

    get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),

    (neg(PredLeftA) = PredRightA ; PredLeftA = neg(PredRightA)),
    (PropA = or(PredLeftA, PredRightA) ; PropA = or(PredRightA, PredLeftA)).