Sharing project results

Stream: Equational

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

One thing I do think we might able to contribute is examples of implications/refutations that ATPs are unable to establish that we know to be true. This may be useful as either a test set for CASC, or alternatively as a test set in some online library such as the TPTP Problem Library. If others think that's a good idea, Geoff Sutcliffe organizes both of those so he can probably direct what's appropriate.

Now that the final formalizations are in, I thought I'd bring this up again. We have generated a database of results that could perhaps be useful for the ATP community. I noticed that Geoff Sutcliffe has an account on this Zulip, so unless anyone objects, I will start a thread here in the next few days tagging him to introduce some of the results from the project that may be of use, say for CASC or TPTP. In particular, I need to brush the dust off my toolchain and figure out how many of the implications vampire can't resolve in some small/reasonable amount of time, which ones they are, and find the breakdown of how many do/don't have finite counter-examples.

[Notification Bot]

A message was moved here from #Equational > What are the hardest positive implications for an ATP? by Vlad Tsyrklevich.