Skip to main content
Mathematica

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

10
  • $\begingroup$ I would recommend starting from just two basic axioms and gradually introducing the others to find the bad ones: Naxioms = { ForAll[{x, y}, plus[x, y] == plus[y, x]], ForAll[x, plus[x, zero] == x] }; works. $\endgroup$ Commented Nov 18, 2020 at 16:56
  • 2
    $\begingroup$ The problem appears to be that Mathematica doesn't think that the first 4 axioms are proper equations. You can check like this (I found this internal function via tracing) Language`EquationalProofDump`isEquationQ /@ Naxioms returns {False, False, False, False, True, True, True, True} $\endgroup$ Commented Nov 18, 2020 at 17:03
  • 2
    $\begingroup$ I'm not sure, it seems to be quite fussy about what it thinks is a valid equation: see here: pastebin.com/LsrdCt3P Something must go wrong internally - I suspect FindEquationalProof is kind of broken for a lot of use cases like yours, unless there are subtle semantics of ForAll that I'm not aware of. $\endgroup$ Commented Nov 18, 2020 at 17:32
  • 1
    $\begingroup$ I'm not certain enough to give a full answer as I've only used this feature a few times (and I've always had difficulty with anything non-trivial and not in the docs). Also there's probably no hope for the induction axiom as it's a second order axiom, and it appears FindEquationalProof seems to suit first-order logic only. For example you cannot do second-order problems quantified over propositions like: FindEquationalProof[Exists[X, X[0]], {P[0], Q[0]}] expecting to get P[0] or Q[0] unifying X with P or Q. You may want to try Prolog, TLA+, z3, Lean theorem prover, perhaps. $\endgroup$ Commented Nov 18, 2020 at 17:49
  • 2
    $\begingroup$ @user64494 by the way, I have a feeling Mathematica might be using this theorem prover: webwaldmeister.waldmeister.org for proof finding in some places, because 'waldmeister' appears in the traces as Language`EquationalProofDump`waldmeister. Also check here: mpi-inf.mpg.de/departments/automation-of-logic/software/… ...Stephen Wolfram has employed our system to carry out investigations in the area of singleton axiom systems for Boolean algebra... . So it wouldn't surprise me if that's being used as part of FindEquationalProof. $\endgroup$ Commented Nov 18, 2020 at 23:53