Out of curiosity, I'm trying to implement a natural deduction prover in Mathematica using FindEquationalProof. So far, I've implemented a few of the easier rules:
axioms = {
ForAll[{A, B}, Implies[A && B, A]] (* conjunction elim. *),
ForAll[{A, B}, Implies[A && B, B]] (* conjunction elim. *),
ForAll[{A, B}, Implies[A, A || B]] (* disjunction intro. *),
ForAll[{A, B}, Implies[B, A || B]] (* disjunction intro. *),
ForAll[A, Implies[!! A, A]] (* negation elim. *)
}
Using these axioms, FindEquationalProof can solve some basic problems, like
FindEquationalProof[A && B, {axioms, B && A}]
returns a 21-step proof. I can't really say whether the axioms work correctly or not, and I have even less idea how to implement inference rules where cancellation is allowed (like in proof by contradiction). How could these rules be implemented in Mathematica? To make the question more specific, how could one implement the introduction of implication rule? The problem here is the cancellation property, marked with square brackets [ and ]:
[A]
...
B
--------- --> I
A --> B
The cancellation property means that when introducing an implication, one is allowed to cancel some temporary assumption $A$.
As a side note, as this question shows, using Resolve might be easier, but the reason I want to use FindEquationalProof is that it returns a ProofObject. This allows seeing how the proof was constructed, either as a graph or a human-readable notebook. Resolve would simply return True, which is not helpful in this case.
proof = FindEquationalProof[A && B, {axioms, B && A}] proof["ProofGraph"] proof["ProofNotebook"]$\endgroup$ProofObjectas output instead of just a confirmationTrue. $\endgroup$