% :- ensure_loaded(library(strings)).

not(true, false).
not(false, true).

and(false, false,  false) :- !.
and(false, true,   false) :- !.
and(true,  false,  false) :- !.
and(true,  true,   true ) :- !.

or(false, false,  false) :- !.
or(false, true,   true ) :- !.
or(true,  false,  true ) :- !.
or(true,  true,   true ) :- !.

implies(false, false,  true ) :- !.
implies(false, true,   true ) :- !.
implies(true,  false,  false) :- !.
implies(true,  true,   true ) :- !.

literal(Formula) :- atom(Formula), !.
literal(not(Formula)) :- atom(Formula).

evaluate(Formula, Literals, Result) :-
    literal(Formula),
    !,
    (member(Formula, Literals) -> Result = true ; Result = false).

evaluate(not(Formula), Literals, Result) :-
    evaluate(Formula, Literals, Complement),
    !,
    not(Complement, Result).

evaluate(and(F, G), Literals, Result) :-
    !,
    evaluate(F, Literals, R1),
    evaluate(G, Literals, R2),
    and(R1, R2, Result).

evaluate(or(F, G), Literals, Result) :-
    !,
    evaluate(F, Literals, R1),
    evaluate(G, Literals, R2),
    or(R1, R2, Result).

evaluate(implies(F, G), Literals, Result) :-
    !,
    evaluate(F, Literals, R1),
    evaluate(G, Literals, R2),
    implies(R1, R2, Result).


% Extract atoms from formula

extract(Formula, Atoms) :- extract(Formula, [], Atoms).

extract(Formula, Accum, Atoms) :-
    atom(Formula),
    (member(Formula, Accum) -> Atoms = Accum ; Atoms = [Formula | Accum]).

extract(not(Formula), Accum, Atoms) :-
    extract(Formula, Accum, Atoms).

extract(and(F, G), Accum, Atoms) :-
    extract(F, Accum, More),
    extract(G, More, Atoms).

extract(or(F, G), Accum, Atoms) :-
    extract(F, Accum, More),
    extract(G, More, Atoms).

extract(implies(F, G), Accum, Atoms) :-
    extract(F, Accum, More),
    extract(G, More, Atoms).

proveTautology(Formula, Proof) :-
    extract(Formula, Atoms),
    reverse(Atoms, AtomsRev),
    proveAll(AtomsRev, [], Formula, Proof).

proveAll([], Combo, Formula, Proof) :-
    prove(Formula, Combo, Proof).

proveAll([Atom | Atoms], Combo, Formula, Proofs):-
    proveAll(Atoms, [not(Atom) | Combo], Formula, Proofs1),
    proveAll(Atoms, [    Atom  | Combo], Formula, Proofs2),
    append(Proofs1, [step(not(Atom), assumption)], Proofs1a),
    append(Proofs2, [step(    Atom,  assumption)], Proofs2a),
    Proofs = [step(Formula, or-elim), Proofs1a, Proofs2a, step(or(Atom, not(Atom)), lem)].
%    Proofs3 = [[Proofs1, step(Atom, assumption)], step(or(Atom, not(Atom)), lem)],
%    append([Proofs2, step(not(Atom), assumption)], Proofs3, Proofs).

combos(Atoms, Combos) :-
    combos(Atoms, [[]], Combos).

combos([], Combos, Combos).
combos([Atom | Atoms], CombosIn, CombosOut) :-
    combine(CombosIn, not(Atom), [], Accum),
    combine(CombosIn, Atom, Accum, Result),
    combos(Atoms, Result, CombosOut).

combine([], _Literal, Accum, Accum).

combine([Combo | Combos], Literal, Accum, NewCombos) :-
    combine(Combos, Literal, [[Literal | Combo] | Accum], NewCombos).

member(A, [A | _]).
member(A, [_ | L]) :- member(A, L).

prove(Formula, Literals, [step(Formula, premise)]) :-
    literal(Formula),
    evaluate(Formula, Literals, true),
    member(Formula, Literals) -> true ; fail.

prove(not(Formula), Literals, Proof) :-
    evaluate(Formula, Literals, false),
    provenot(Formula, Literals, Proof).

prove(and(F, G), Literals, [step(and(F, G), and-intro) | Proof]) :-
    prove(F, Literals, Fproof),
    prove(G, Literals, Gproof),
    append(Fproof, Gproof, Proof).

prove(or(F, G), Literals, [step(or(F, G), or-intro1)| Proof]) :-
    prove(F, Literals, Proof),
    !.

prove(or(F, G), Literals, [step(or(F, G), or-intro2) |  Proof]) :-
    prove(G, Literals, Proof).

prove(implies(F, G), Literals, [step(implies(F, G), implies-intro), [step(G, bottom-elim), step(bottom, not-elim), step(F, assumption)] | Proof]) :-
    evaluate(F, Literals, false),
    !,
    provenot(F, Literals, Proof).

prove(implies(F, G), Literals, [step(implies(F, G), implies-intro), Subproof]) :-
    prove(G, Literals, Proof),
    append(Proof, [step(F, assumption)], Subproof).

provenot(not(Formula), Literals, [step(not(Formula), premise)]) :-
    atom(Formula),
    evaluate(Formula, Literals, false).

provenot(Formula, Literals, [step(not(Formula), premise)]) :-
    atom(Formula),
    evaluate(Formula, Literals, false).

provenot(not(Formula), Literals, [step(not(not(Formula)), not-not-intro) | Proof]) :-
    prove(Formula, Literals, Proof).

provenot(and(F, G), Literals, [step(not(and(F, G)), deMorgan1), step(or(not(F), not(G)), or-intro1) | Proof]) :-
    prove(not(F), Literals, Proof),
    !.

provenot(and(F, G), Literals, [step(not(and(F, G)), deMorgan1), step(or(not(F), not(G)), or-intro2) | Proof] ) :-
    prove(not(G), Literals, Proof).

provenot(or(F, G), Literals, [step(not(or(F, G)), deMorgan2), step(and(not(F), not(G)), and-intro), Fproof, Gproof]) :-
    provenot(F, Literals, Fproof),
    provenot(G, Literals, Gproof).

provenot(implies(F, G), Literals, Proof) :-
    prove(F, Literals, Fproof),
    prove(not(G), Literals, Gproof),
    append(Fproof, Gproof, Rest),
    append([[step(not(implies(F, G)), not-intro), step(bottom, not-elim), step(G, implies-elim), step(implies(F, G), assumption)], step(and(F, not(G)), and-intro), Fproof, Gproof], Rest, Proof).


test(Number, Formula, Literals) :- 
    nl,
    write('Test '), write(Number),
    write(': Formula: '), write(Formula),
    write(', Literals: '), write(Literals),
    evaluate(Formula, Literals, Value),
    write(', Value: '), write(Value), nl,
    (  Value = true -> (prove(Formula, Literals, Result),
                       write('Proof: '), nl, writeProof(Result), nl)
     ; Value = false -> (provenot(Formula, Literals, Result),
                        write('Proof of negation: '), nl, writeProof(Result), nl)
     ; write('Value could not be determined'), nl).

prefix('| ').

writeProof(P) :- prefix(X), writeProof(P, X).

writeProof([], _Prefix).
writeProof([First | Rest], Prefix) :-
    writeProof(Rest, Prefix),
    writeProof1(First, Prefix).

writeProof1(First, Prefix) :-
    First = step(_, _) -> (write(Prefix), write(First), nl)
            ; prefix(More),
              concat_atom([Prefix, More], NewPrefix),
              writeProof(First, NewPrefix).

test :-
    test(01, a, [a])
  , test(02, a, [not(a)])
  , test(03, not(a), [a])
  , test(04, not(a), [not(a)])
  , test(05, implies(a, b), [not(a), not(b)])
  , test(06, implies(a, b), [not(a), b])
  , test(07, not(implies(a, b)), [a, not(b)])
  , test(08, implies(a, b), [a, b])
  , test(09, and(a, b), [a, b])
  , test(10, not(and(a, b)), [not(a), b])
  , test(11, not(and(a, b)), [a, not(b)])
  , test(12, not(and(a, b)), [not(a), not(b)])
  , test(13, not(or(a, b)), [not(a), not(b)])
  , test(14, or(a, b),      [not(a), b])
  , test(15, or(a, b),      [a, not(b)])
  , test(16, or(a, b),      [a, b])
  , test(17, implies(or(a, b), or(b, a)),      [not(a), not(b)])
  , test(18, implies(or(a, b), or(b, a)),      [not(a), b])
  , test(19, implies(or(a, b), or(b, a)),      [a, not(b)])
  , test(20, implies(or(a, b), or(b, a)),      [a, b])
  , test(21, implies(and(a, b), and(b, a)),      [not(a), not(b)])
  , test(22, implies(and(a, b), and(b, a)),      [not(a), b])
  , test(23, implies(and(a, b), and(b, a)),      [a, not(b)])
  , test(24, implies(and(a, b), and(b, a)),      [a, b])
  , test(25, implies(implies(a, b), or(not(a), b)), [not(a), not(b)])
  , test(26, implies(implies(a, b), or(not(a), b)), [not(a), b])
  , test(27, implies(implies(a, b), or(not(a), b)), [a, not(b)])
  , test(28, implies(implies(a, b), or(not(a), b)), [a, b])
  , test(29, implies(not(implies(a, b)), not(or(not(a), b))), [not(a), not(b)])
  , test(30, implies(not(implies(a, b)), not(or(not(a), b))), [not(a), b])
  , test(31, implies(not(implies(a, b)), not(or(not(a), b))), [a, not(b)])
  , test(32, implies(not(implies(a, b)), not(or(not(a), b))), [a, b])
  , test(33, implies(implies(p, q), not(and(p, not(q)))), [not(p), not(q)])
  , test(34, implies(implies(p, q), not(and(p, not(q)))), [not(p), q])
  , test(35, implies(implies(p, q), not(and(p, not(q)))), [p, not(q)])
  , test(36, implies(implies(p, q), not(and(p, not(q)))), [p, q])
  .

testTaut :- proveTautology(implies(implies(p, q), implies(not(q), not(p))), Proof), 
writeProof(Proof).