Message Boards Message Boards

Use FindEquationalProof on the following equation?

Posted 4 years ago

It failed, why?

FindEquationalProof[p + q == m, {x + p == z, x - q == y, z - y == m}]
POSTED BY: Math Logic
2 Replies
Posted 4 years ago

Got it! Appreciation!!

POSTED BY: Math Logic

FindEquationalProof does not know by default the rules of arithmetic, so you need to provide them as additional axioms. In this case only the (abelian) group of the addition operation is needed:

additiveGroup = AxiomaticTheory[{"AbelianGroupAxioms", "Multiplication" -> plus, "Identity" -> zero, "Inverse" -> minus}]

Then you can obtain a proof of your case with

FindEquationalProof[plus[p, q] == m, {additiveGroup, {plus[x, p] == z, plus[x, minus[q]] == y, plus[z, minus[y]] == m}}]
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract