4
$\begingroup$

Mathematica 11.3.0 includes a new command FindEquationalProof having good prospects. Studying it, I consider a somewhat modified example from the help

grouptheory = {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], ForAll[a, g[a, e] == a], 
ForAll[a, g[a, inv[a]] == e], ForAll[a, g[a, a] == e]}

, where the assumption ForAll[a, g[a, a] == e] that each element of a group has order two is added. I try to prove that such group is Abelian by

proof = FindEquationalProof[ForAll[{a, b}, g[a, b] == g[b, a]],  grouptheory]

and succeed at this proof. Nice. Next, I visualize the obtained proof by

proof["ProofGraph"]

enter image description here

Unfortunately, neither vertices nor arcs are described, so I understand nothing. The documentation about FindEquationalProof does not shed light on...

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

I am not familiar with this functionality, but I noticed that hovering a node in the graph reveals its name as a tooltip. Each node is a statement. You can then cross reference them e.g. with proof["ProofNotebook"] or proof["ProofDataset"] to see what the statement is.

The visual symbol of nodes indicates the type of statement, e.g. green ones are the axioms that were input. Only three of the four axioms you gave here are actually used in this proof.

The arrows pointing to a node show which statements were directly used in its proof.

Solid (non-dashed) arrows appear to be used with substitution lemmas and show where the substitution comes from. It will be substituted into the branch coming from the dashed arrow.

Improve this answer
$\endgroup$
8
  • $\begingroup$ Thank you. Can you kindly elaborate your answer, explaining what the left green node at the top of the graph means? $\endgroup$
    – user64494
    Commented Nov 27, 2018 at 13:49
  • $\begingroup$ @user64494 I thought that would be clear after looking at their names. Green ones are all Axioms, orange triangles "Critical Pair Lemma", etc. I am simply guessing from reading the node names. As I said, I am not familiar with this functionality either. $\endgroup$
    – Szabolcs
    Commented Nov 27, 2018 at 13:51
  • $\begingroup$ There are four axioms. Which of them is noticed by the left green node at the top of the graph? The result of proof["ProofDataset"] says nothing about it for me. $\endgroup$
    – user64494
    Commented Nov 27, 2018 at 13:54
  • $\begingroup$ @user64494 I do not understand your comment. The axioms are clearly listed in both the dataset and the (easier to read) notebook for me under the same name as in the graph. I used M11.3. If your dataset does not contain them, please show a screenshot and indicate your Mathematica version (though I think M11.3 is the only released version with this functionality). $\endgroup$
    – Szabolcs
    Commented Nov 27, 2018 at 13:58
  • $\begingroup$ Can you kindly elaborate your statement "The axioms are clearly listed in both the dataset and the (easier to read) notebook for me under the same name as in the graph"? I repeat my open question "There are four axioms. Which of them is noticed by the left green node at the top of the graph? ". TIA. $\endgroup$
    – user64494
    Commented Nov 27, 2018 at 15:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.