2020-04-14 11:25:26 (GMT)
I'd like to open a discussion whether or not we should use the saturation framework for our work on FOL with Booleans. It was great to use for lambda-free superposition and for lambda-superposition, but @Visa thinks that it's overkill for FOL with Booleans. Any opinions?
2020-04-14 11:56:24 (GMT)
Not an expert, for sure. But I like the framework and authors (see how I am objective here) claim that it helps lifting
2020-04-14 11:56:31 (GMT)
What are the arguments against?
2020-04-14 12:2:17 (GMT)
Against: If you just do the standard (static to dynamic) lifting, it is more usual (and enough) to refer to B&G.
For: Using the framework, you could get completeness results up to the Zipper loop, which I assume will be the support of the implem anyway.
For: (but not super objective, as I am an author of the framework) B&G was proven to contain a few mistakes in its formalism when Anders formalized RP. Since our framework has been formalized in parallel to being developed, it should be free of minor but result-breaking inconsistencies.
2020-04-14 12:3:54 (GMT)
Against: Our redundancy criterion needs to respect some extra conditions (that allow to lift results to provers) compared to B&G.
2020-04-14 12:6:4 (GMT)
Sophie, you forgot the biggest for (IMO): B&G don't cover subsumption. So with B&G you get dynamic completeness of a "prover process" that cannot do subsumption.
2020-04-14 12:8:4 (GMT)
I didn't forget it :mischievous: . It is just stated in a less explicit fashion since this is what allows the lifting to prover architectures (my first "for").
2020-04-14 12:10:54 (GMT)
but thanks for making it clearer :wink:
2020-04-14 13:39:40 (GMT)
Are you talking about papers, or the handbook's chapter? Cause this one does have subsumption, I think?
2020-04-14 13:45:26 (GMT)
They prove completeness with subsumption in the handbook, but not in general, only for their concrete calculus.
2020-04-14 13:47:44 (GMT)
In particular, B&G's redundancy criterion doesn't support subsumption (strict or not).
2020-04-14 13:48:39 (GMT)
Another reason in my mind to use a framework is that there are quite a few papers out there that prove static completeness of a calculus w.r.t. a redundancy criterion, but they never prove that the redundancy criterion actually is a redundancy criterion.
2020-04-14 13:49:30 (GMT)
If it turns out that isn't a redundancy criterion, the whole calculus is effectively incomplete in practice.
2020-04-14 13:50:2 (GMT)
I.e. going from static to dynamic isn't fully automatic -- you need a well-behaved . And if it's not, you've really wasted your time proving static completeness.
2020-04-14 13:51:6 (GMT)
Looking back at our IJCAR 2018 and CADE 2019 papers, the fact that we never prove a redundancy criterion is a bit shameful (but typical), and even more so that we never even mention that this is a pending proof obligation.
2020-04-14 13:53:54 (GMT)
it's somewhat amazing to me that the metatheory of superposition is now alive and kicking again, thanks to y'all and some other formalization efforts!
2020-04-14 13:54:53 (GMT)
Yeah, it's very retro!
2020-04-14 16:38:48 (GMT)
One good argument against the framework (at least for the ground to nonground part) are the skolems that we introduce. The arguments of the skolems depend on the free variables in the clause, which we don't know on the ground level. Therefore, we would have to use the intersection-mechanism to pass on this information to the ground layer.
2020-04-14 17:3:50 (GMT)
Alexander Bentkamp said:
One good argument against the framework (at least for the ground to nonground part) are the skolems that we introduce. The arguments of the skolems depend on the free variables in the clause, which we don't know on the ground level. Therefore, we would have to use the intersection-mechanism to pass on this information to the ground layer.
Ok this sounds tricky...