2
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ How do you mean "see"? As a graph or a list of steps? Can you be more specific about your main question? $\endgroup$ – flinty May 25 '20 at 12:55
  • $\begingroup$ If you do this you can see the steps Mathematica is taking both as a graph, and as a notebook of steps : proof = FindEquationalProof[A && B, {axioms, B && A}] proof["ProofGraph"] proof["ProofNotebook"] $\endgroup$ – flinty May 25 '20 at 12:59
  • $\begingroup$ Sorry, that was unclear. I've edited the question to hopefully make it clearer, but basically, "seeing" means getting a ProofObject as output instead of just a confirmation True. $\endgroup$ – Sami May 25 '20 at 16:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.