/* file: ndprover.pro * author: Robert Keller * purpose: Generating a natural deduction proof from a tautology. * This provides an algorithmic version of the completeness * theorem for classical logic. * explanation: If an input propositional formula is a tautology, * a natural deduction proof is generated for it. * * Type test. after the Prolog prompt to run test cases, * or testTautology(Formula) to test a specific formula. */ % This predicate tests whether the Formula is a tautology. % If it is, it displays a natural deduction proof for it. % If not, the predicate itself fails. testTautology(Formula) :- resetCounter, nl, ( proveTautology(Formula, Proof) -> (write('Proof for tautology: '), write(Formula), write(':'), nl, nl, writeProof(Proof)) ; (write(Formula), write(' is not a tautology.')) ), nl. % proveTautology is the top-level prover. % If the first argument is a tautology, a natural deduction proof is generated. % If it is not, then the prover fails. proveTautology(Formula, Proof) :- extract(Formula, Atoms), proveAll(Atoms, Formula, Proof). % proveAll constructs the major sections of the proof and connects them. % Using the atoms in the original formula, a nested set of "boxes" is % effectively created. Each pair of boxes is preceded with a lem rule % (law-of-the-excluded-middle) on a single atom letter. Each box of % the pair opens with an assumption of that atom, or its negation. % After closing, the pair is followed by one application of or-elimination % to tie together the sub-derivations in the two boxes and the lem. proveAll(Atoms, Formula, Proof) :- reverse(Atoms, AtomsRev), % Atoms reversed for cosmetic reasons only proveAll(AtomsRev, [], Formula, Proof, _, _). % Auxiliary version of proveall, which takes an additional argument, % an accumulated Combo of atomic propositions and their negations. % It keeps splitting, until all atoms are accounted for. proveAll([], Combo, Formula, Proof, First, Last) :- prove(Formula, Combo, Proof, First, Last). proveAll([Atom | Atoms], Combo, Formula, Proofs, First, Last):- proveAll(Atoms, [step(S1, not(Atom)) | Combo], Formula, Proofs1, _F2, L1), proveAll(Atoms, [step(S2, Atom) | Combo], Formula, Proofs2, _F1, L2), append(Proofs1, [step(S1, not(Atom), assumption(or-elim))], Proofs1a), append(Proofs2, [step(S2, Atom, assumption(or-elim))], Proofs2a), Proofs = [step(Last, Formula, or-elim(First, S2-L2, S1-L1)), Proofs1a, Proofs2a, step(First, or(Atom, not(Atom)), lem)]. % Note above that proofs are stacked in reverse order, with the lem % usage last and the or-elim first. % prove constructs the proof for an arbitrary formula in the context of % assumptions of atoms or the negations, amounting to the imposition of % a valuation. prove(Formula, Literals, Proof) :- prove(Formula, Literals, Proof, First, First). prove(Formula, Literals, [], Step, Step) :- literal(Formula), evaluate(Formula, Literals, true), member(step(Step, Formula), Literals) -> true ; fail. prove(not(Formula), Literals, Proof, First, Last) :- evaluate(Formula, Literals, false), provenot(Formula, Literals, Proof, First, Last). prove(and(F, G), Literals, [step(Last, and(F, G), and-intro(L1, L2)) | Proof], First, Last) :- prove(F, Literals, Fproof, First, L1), prove(G, Literals, Gproof, _, L2), append(Fproof, Gproof, Proof). prove(or(F, G), Literals, [step(Last, or(F, G), or-intro(L1))| Proof], First, Last) :- prove(F, Literals, Proof, First, L1), !. prove(or(F, G), Literals, [step(Last, or(F, G), or-intro(L1)) | Proof], First, Last) :- prove(G, Literals, Proof, First, L1). prove(implies(F, G), Literals, [step(Last, implies(F, G), derived3(L1)) | Proof], First, Last) :- evaluate(F, Literals, false), !, provenot(F, Literals, Proof, First, L1). prove(implies(F, G), Literals, [step(Last, implies(F, G), implies-intro(L1)) | Proof], Last, Last) :- prove(G, Literals, Proof, _, L1). provenot(not(Formula), Literals, [], Step, Step) :- atom(Formula), member(step(Step, not(Formula)), Literals) -> true; fail. provenot(Formula, Literals, [], Step, Step) :- atom(Formula), member(step(Step, not(Formula)), Literals) -> true; fail. provenot(not(Formula), Literals, [step(Last, not(not(Formula)), not-not-intro(L)) | Proof], First, Last) :- prove(Formula, Literals, Proof, First, L). provenot(and(F, G), Literals, [step(Last, not(and(F, G)), derived1(L)) | Proof], First, Last) :- prove(not(F), Literals, Proof, First, L), !. provenot(and(F, G), Literals, [step(Last, not(and(F, G)), derived1(L)) | Proof], First, Last ) :- prove(not(G), Literals, Proof, First, L). provenot(or(F, G), Literals, [step(Last, not(or(F, G)), deMorgan(N)), step(N, and(not(F), not(G)), and-intro(L1, L2)) | Proof], First, Last) :- provenot(F, Literals, Fproof, First, L1), provenot(G, Literals, Gproof, _, L2), append(Gproof, Fproof, Proof). provenot(implies(F, G), Literals, Proof, First, Last) :- prove(F, Literals, Fproof, First, L1), prove(not(G), Literals, Gproof, _, L2), Tail = [step(Last, not(implies(F, G)), derived2(L1, L2)) ], append(Tail, Gproof, Tail2), append(Tail2, Fproof, Proof). % Determine whether a formula is a literal literal(Formula) :- atom(Formula), !. literal(not(Formula)) :- atom(Formula). % Evaluate a formula with respect to a valuation, as represented % by a list of literals (propositions and negations of propositions). % Evaluation is needed to determine which kind of proof to construct for % a formula, either one for the formulat itself or its negation. evaluate(Formula, Literals, Result) :- literal(Formula), !, (member(step(_, 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). % Truth tables for the basic operators, used in evaluation 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 ) :- !. % 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). % Standard membership utility member(A, [A | _]). member(A, [_ | L]) :- member(A, L). 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('| '). separator('--------------------'). % This is used to elminate empty boxes from the generated proof. emptyProof([]). emptyProof([A | X]) :- emptyProof(A), emptyProof(X). % output the proof, showing nesting, etc. writeProof(P) :- prefix(X), writeProof(P, X). writeProof(P, _Prefix) :- emptyProof(P), !. writeProof([First | Rest], Prefix) :- writeProof(Rest, Prefix), writeProof1(First, Prefix). writeProof1(First, _Prefix) :- emptyProof(First), !. writeProof1(First, Prefix) :- separator(Separator), ( First = step(Number, Formula, Rule) -> (write(Prefix), writeNumber(Number), write(': '), write(Formula), write(' ['), write(Rule), write(']'), nl) ; prefix(More), ( write(Prefix), write(Separator), nl, concat_atom([Prefix, More], NewPrefix), writeProof(First, NewPrefix), write(Prefix), write(Separator), nl ) ). writeNumber(Number) :- nonvar(Number), !, write(Number). writeNumber(Number) :- nextNumber(Number), write(Number). :- dynamic counter/1. counter(0). nextNumber(N1) :- retract(counter(N)), N1 is N + 1, assert(counter(N1)). resetCounter :- retract(counter(_)), assert(counter(0)). test :- testTautology(or(not(p), p)), testTautology(implies(implies(p, q), implies(not(q), not(p)))), testTautology(p), testTautology(not(p)), testTautology(and(p, q)), testTautology(implies(and(p, q), or(p, q))), testTautology(implies(and(p, not(q)), and(not(q), p))), testTautology(implies(or(p, q), and(p, q))), testTautology(not(and(p, not(p)))), testTautology(implies(p, p)), testTautology(implies(p, implies(not(p), p))), testTautology(implies(implies(p, implies(q, r)), implies(and(p, q), r))), testTautology(implies(not(and(p, q)), or(not(p), not(q)))), testTautology(implies(and(implies(e, and(implies(f, g), implies(g, f))), implies(and(implies(f, g), implies(g, f)), e)), and(implies(g, and(implies(f, e), implies(e, f))), implies(and(implies(f, e), implies(e, f)), g)))), testTautology(implies(and(p, not(q)), and(not(q), p))). % Read from file proveFromFile(X):- see(X), go, seen. go :- read(X), X \== end_of_file, !, testTautology(X), go. go.