Natural deduction with FindEquationalProof


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.