2020-04-28 18:58:6 (GMT)
@Alex Steen @Michael Färber
As you might know, there is a bug in higher-order version of E that concerns some corner cases of HO rewriting
2020-04-28 18:58:45 (GMT)
Thus, if you use higher-order version of E (that is, Ehoh) you should use the one compiled from the branch ehoh_article
2020-05-01 7:47:42 (GMT)
Well, well, well, who's rearing his ugly head again? It's Mr. Skolem! :)
2020-05-01 7:49:24 (GMT)
Anyway, I know that these Skolem-related bugs are really a pain. Skolemisation is surprisingly hard to get right.
2020-05-01 7:50:22 (GMT)
Do you have an estimate about when your change might be integrated into E? Because I'm reluctant to use non-master branches in Satallax ...
2020-05-01 7:50:43 (GMT)
Thanks for informing us, by the way!
2020-05-01 12:7:38 (GMT)
We have to talk to E master @Stephan Schulz :slight_smile:
2020-05-01 12:8:10 (GMT)
But if you use master version of E right now, Satallax will be unsound :frown:
2020-05-01 12:14:55 (GMT)
Well, is there a not-to-radical mergable branch?I would tentatively plan to release E 2.5 after CASC, and I will feel more experimental then. But if it is only a minor change, we can do it anytime...
2020-05-01 12:17:35 (GMT)
It is a change that includes few new higher-order rules
2020-05-01 12:17:47 (GMT)
As well as a rule that does injectivity recognition.
2020-05-01 12:18:23 (GMT)
To be safe I would evaluate and test on the whole TPTP beforehand, but I am not sure if with the current StarExec sitaution it is doable
2020-05-01 12:18:39 (GMT)
Anyways, the branch is ehoh_article (made for the article version of Ehoh paper)