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). This would probably be easier with `Resolve`

, but the point here is to “see” the proof, instead of just getting a confirmation that it’s `True`

.