2020-04-24 8:47:53 (GMT)
I've just noticed that there is a small issue with the notion of eligibility in all our superposition papers. The definition of eligibility is:
A literal L is (strictly) eligible in C if it is selected in C or if there are no selected literals
in C and L is (strictly) maximal in C
The side condition on Sup says for example:
(t β t')π is strictly eligible in Dπ
But what we want is to test the selection before applying π and to test the maximality after applying π. Unless selection is stable under substitution, this definition is not entirely correct.
2020-04-24 8:57:38 (GMT)
Ouch. Ah well I'm not entirely surprised. When one looks at Knuth's errata -- and he's a very careful, precise person -- one realises that to err is human. Good thing we still have the journal publications ahead of us.
2020-04-24 8:58:53 (GMT)
@Ahmed B @Giles This might also concern your superposition with combinators paper.
2020-04-24 9:19:29 (GMT)
Alexander Bentkamp said:
Ahmed B Giles This might also concern your superposition with combinators paper.
Thanks, yes it does. Now that you point it out, it seems obvious.
2020-04-24 9:23:17 (GMT)
It looks like they haven't checked our IJCAR submission yet so we can still modify the camera-ready version on EasyChair.
2020-04-24 9:38:53 (GMT)
So I suppose our options are:
A literal L is (strictly) π-eligible in C if it is selected in C or if there are no selected literals
in C and Lπ is (strictly) maximal in Cπ
2020-04-24 9:42:50 (GMT)
Alexander Bentkamp said:
So I suppose our options are:
- remove the notion of eligibility
- improve the notion of eligibility, e.g.,
A literal L is (strictly) π-eligible in C if it is selected in C or if there are no selected literals
in C and Lπ is (strictly) maximal in Cπ
I am leaning towards removing the notion of eligibility. If this is done, I think that splitting superposition into separate positive and negative rules makes sense.
2020-04-24 9:43:3 (GMT)
Space might be an issue though.
2020-04-24 9:47:21 (GMT)
On our side, I hope we keep it -- or if we remove it, that we don't duplicate the rule.
2020-04-24 9:47:53 (GMT)
Maybe "eligible in w.r.t. "?
2020-04-24 9:49:18 (GMT)
Yes, I would also prefer to keep it. If you prefer "w.r.t.", that's fine with me.
2020-04-24 10:38:23 (GMT)
It sounds more English, that's all. ;)
2020-04-24 12:2:32 (GMT)
So I'll write "eligible w.r.t. the identity" for PosExt?
2020-04-24 12:5:40 (GMT)
Actually, "eligible w.r.t. the identity" would occur quite often in the ground proof, too. Maybe we should make the identity the default if nothing else is mentioned.
2020-04-24 12:15:12 (GMT)
Ohoh, another problem with "w.r.t.": I already use it to refer to the selection function used. Should I write "eligible w.r.t. π and sel"?
2020-04-24 12:15:55 (GMT)
I'm not married to "w.r.t." But your latest proposal sounds fine.
2020-04-24 12:16:3 (GMT)
We have it all the time in our saturation framework paper.
2020-04-24 12:16:34 (GMT)
It would be nice to have a convention to avoid saying "w.r.t. the identity".
2020-04-24 12:17:19 (GMT)
In the saturation paper sometimes we leave some dependencies implicit. When you're working at the ground level, I'm sure if you say "w.r.t. sel" alone that should be fine.
2020-04-24 12:17:49 (GMT)
(But then maybe swap and sel to put sel first.)
2020-04-24 12:18:19 (GMT)
((Forget my very last proposal..))
2020-04-24 12:19:9 (GMT)
E.g. "Red is a redundancy criterion w.r.t. and Inf.
2020-04-24 12:28:37 (GMT)
So I shouldn't write something like "A literal is eligible in C if it is eligible w.r.t. the identity substitution in C" after the def of "eligible w.r.t." to make the default explicit?
2020-04-24 12:54:27 (GMT)
Or better: "If $\sigma$ is the identity substitution, we leave it implicit."
2020-04-24 13:23:57 (GMT)
The latter is perfect in an article. In a conf version, I might live without if I ran out of space (which is always). ;)
2020-04-24 13:24:43 (GMT)
The situation is analogous to vs. . If you know your formula is a sentence (i.e. variable-free), you drop the , sometimes implicitly, sometimes with a kind warning of the type you suggest.
2020-04-24 15:13:29 (GMT)
Jasmin Blanchette said:
On our side, I hope we keep it -- or if we remove it, that we don't duplicate the rule.
On attempting to modify the paper, I realise that duplicating the rule quickly becomes pretty messy.
2020-04-24 15:47:19 (GMT)
@Ahmed B I am done with papers/2020-LMCS-lfhosup, if you want to see what I decided to do.
2020-04-24 15:47:56 (GMT)
(but it's basically what we've discussed above)
2020-04-25 8:55:16 (GMT)
Thanks, it looks clean.
@Alexander Bentkamp in the proof of Lemma 4.4, should there not be a "w.r.t to " of some sort in the non-ground level?
2020-04-25 9:56:9 (GMT)
No, Lemma 4.4 is only about ground clauses. That's the beauty of our new proof structure that we use since we employ the saturation framework by Waldmann et al. Non-ground clauses are only discussed in Section 4.3.
2020-04-26 6:41:59 (GMT)
@Ahmed B @Alexander Bentkamp Alex discovered that our IJCAR 2018 had a small completeness bug, regarding selection. Our journal manuscript has it fixed. Maybe this affects your IJCAR 2020 paper? Have Alex brought this up aleady?
2020-04-26 14:5:38 (GMT)
:question: That's what we discussed with Ahmed and Giles above already, right?
2020-04-26 16:44:50 (GMT)
Sorry. I mean the constraints on the selection function in intentional calculi.
2020-04-26 16:47:54 (GMT)
To quote a mid-March 2020 email of yours (Alex's): "In any case, I am pretty sure that this is an error in our IJCAR 2018 paper. How can we communicate this?"
2020-04-26 16:48:36 (GMT)
Ah, sorry, I had a wrong memory. It affected the purifying calculy only, not the intentional ones. Forget what I wrote.
2020-04-26 16:49:5 (GMT)
I was in a hurry to write the comment (given that the IJCAR 2020 camera ready deadline is officially passed...).
2020-04-26 17:37:37 (GMT)
Thanks for the message nevertheless. I am aware that we have been somewhat sloppy in our treatment of the selection function in the completeness proof. This is certainly something to bare in mind for a journal version.