2020-03-31 18:58:16 (GMT)
@Simon Cruanes Is there any reason why positive simplify reflect does not try flipping the equations? (superposition.ml :: positive_simplify_reflect)
2020-03-31 18:59:35 (GMT)
Second thing is that instead of checking for equality, simplify reflect might want to check whether the generated substitution can be extended to contain rhs?
2020-03-31 19:1:7 (GMT)
And inspired by our literature for this week I wanted to try and implement some AC reasoning.
2020-03-31 19:1:29 (GMT)
I realized that more or less the same things that they descirbe are implemented in E
2020-03-31 19:5:23 (GMT)
There's already basic AC reasoning, check out AC.ml. It works for zipperposition's input format. (examples/ac.zf)
2020-03-31 19:6:53 (GMT)
As for positive simplify reflect, where exactly should it try flipping the equation? It relies on the index to do that, since s=t in the index should also have t=s there unless s>t is known.
But then, indeed, it should try both sides I guess, I must have overlooked that.
2020-03-31 19:19:48 (GMT)
the file AC.ml does not exist anymore it seems
2020-03-31 19:21:31 (GMT)
found it
2020-03-31 19:21:46 (GMT)
VSCode was not working properly
2020-03-31 19:23:17 (GMT)
it does more or less what E does, iirc. Detecting AC axioms would be very useful of course.
2020-03-31 19:24:31 (GMT)
yes I see now
2020-03-31 19:24:38 (GMT)
It does exactly what E does I checked
2020-03-31 19:24:54 (GMT)
What is also interesting is live checking of AC properties
2020-03-31 19:25:10 (GMT)
when asocciativity or commutativity is derived
2020-03-31 19:25:51 (GMT)
I will add this to the code tomorrow
2020-04-01 8:25:56 (GMT)
Simon, one possibility to avoid trying both orientations is to order equations left-to-right according to the order (E does that). Now if instantiation of an oriented equation is in the clause, then this instantiation must be oriented properly.