2020-10-14 17:4:36 (GMT)
Hi All,
First draft for the paper authored by @Alexander Bentkamp , @Jasmin Blanchette , @Simon Cruanes , @Sophie Tourret , @Visa and me is available at https://petarvukmirovic.github.io/home/
2020-10-14 17:5:31 (GMT)
The paper is about the latest HO techniques we implemented in Zip
2020-10-14 17:5:41 (GMT)
Your comments are welcome!
2020-10-14 17:8:38 (GMT)
Wow! Congrats!
2020-10-14 17:9:28 (GMT)
Will look at it in the coming weeks. The only tiny imperfection I saw was the usual inconsistent capitalization of headings. ;)
2020-10-23 7:52:45 (GMT)
Petar Vukmirovic said:
Hi All,
First draft for the paper authored by Alexander Bentkamp , Jasmin Blanchette , Simon Cruanes , Sophie Tourret , Visa and me is available at https://petarvukmirovic.github.io/home/
I am reading through the paper and will send you some feedback soon hopefully. One point that I am not clear on, is what happens if one of the premises of a non-empty stream is simplified. Can the stream be removed from Q?
2020-10-23 11:6:55 (GMT)
In principle, yes (see the Zipperposition Loop in the Saturation Framework paper). In practice, I believe Zip doesn't do orphan deletion currently.
2020-10-23 12:50:21 (GMT)
It does :smile:
2020-10-23 12:53:5 (GMT)
Also for streams?
2020-10-23 12:54:15 (GMT)
If so, maybe we should mention it in the paper?
2020-10-23 12:55:7 (GMT)
Ok, good idea, thanks :smile:
2020-10-23 13:34:9 (GMT)
Oh, so you have orphan deletion. Great!!
2020-10-23 13:36:36 (GMT)
But we should write something like 'a technique with the unfortunate name of "orphan deletion" '.
2020-10-23 13:36:43 (GMT)
It's really a bad name.
2020-10-23 13:38:2 (GMT)
Maybe our chance to give it a new name?
2020-10-23 13:39:59 (GMT)
Is orphan deletion really the standard name?
2020-10-23 13:40:15 (GMT)
I heard it for the first time ever from Stephan
2020-10-23 13:40:21 (GMT)
Maybe Vampires have a better name?
2020-10-23 13:43:4 (GMT)
As far as I am aware, Vampire doesn't do any orphan deletion.
2020-10-23 13:47:24 (GMT)
I googled a bit and the name seems to come from databases. There, they have a similar concept called "Cascade Delete" or "Cascading Removal". I actually think that cascade removal is closer to what we are doing than orphan removal is. So maybe we should use the name "Cascade removal" instead?
2020-10-23 14:2:37 (GMT)
wow
2020-10-23 14:2:40 (GMT)
that is a perfect name
2020-10-23 15:24:55 (GMT)
+1 for cascade removal, everywhere!
2020-10-23 15:38:39 (GMT)
trickle down removal
:upside_down:
2020-10-23 15:43:19 (GMT)
Somebody should ask Uwe. If he's on board, we've won. ;)
2020-10-23 15:55:8 (GMT)
We could also make sure that Konstantin (who writes about "orphan elimination") is on board.
2020-10-23 15:55:22 (GMT)
Oh, there's just a problem.
2020-10-23 15:55:33 (GMT)
Any discussion of orphan removal needs a concept of orphan.
2020-10-23 15:56:5 (GMT)
And the name is unfortunate today, not just due to real orphans, but because losing one's parent doesn't suffice to make you an orphan in real life.
2020-10-23 15:56:28 (GMT)
I withdraw my +1 until this issue has been resolved.
2020-10-23 15:56:54 (GMT)
See e.g. the beginning of Sect. 4.2 of Waldmann et al. for some example of text that would need to be updated.
2020-10-23 15:59:29 (GMT)
(Dammit, I'm citing Waldmann et al. again. Reviewer 2 will kill me.)
2020-10-23 16:9:5 (GMT)
In Sect. 4.2 you define an orphan, but then you use the word only in the context "orphan deletion". I think you could just as well define cascade removal directly:
"Cascade removal is the removal of a passive formula that was generated by an inference for which at
least one premise is no longer active."
2020-10-23 16:59:59 (GMT)
We still need the terminology in general IMO.
2020-10-23 17:0:9 (GMT)
Otherwise the new proposal won't subsume the old one.
2020-10-24 15:19:24 (GMT)
"isolated formula", "lonely formula" as replacements for "orphan"?
2020-10-24 15:25:2 (GMT)
Yes, this definitely goes into the right direction -- but smacks perhaps too much of covid resp. single? ;) Can we keep brainstorming?
2020-10-24 15:57:35 (GMT)
"decommissioned formula"?
2020-10-24 17:52:37 (GMT)
A bit of a mouthful. ;)
2020-10-24 18:32:42 (GMT)
"obsolete clause"?
2020-10-24 18:32:56 (GMT)
(or "formula", depending on the context)
2020-10-24 18:33:4 (GMT)
"disconnected"?
2020-10-24 18:33:43 (GMT)
"survivor (deletion)"?
2020-10-24 18:35:22 (GMT)
"outlasting"?
2020-10-24 19:50:40 (GMT)
I like "disconnected". A shorter version with similar nuances: "stranded"
2020-10-24 20:2:7 (GMT)
"Stranded" +1 :)
2020-10-24 20:2:43 (GMT)
You're a genius.
2020-10-25 0:20:38 (GMT)
So, we're abandoning all clauses that have been stranded? Petition to rename the prover "bountyposition" :p
2020-10-26 8:2:29 (GMT)
"backless"?
2020-10-26 8:3:22 (GMT)
Oxford Am. E. Dict. "adjective (of a woman's garment) cut low at the back:"? ;)
2020-10-26 8:4:11 (GMT)
2020-10-26 8:4:15 (GMT)
no, more like "with no backing"
2020-10-26 8:4:28 (GMT)
Yes but that's not in the dictionary.
2020-10-26 8:4:59 (GMT)
then "unbacked"
2020-10-26 8:5:14 (GMT)
Yes, that's much better. ;)
2020-10-26 8:5:37 (GMT)
It's also Simon-proof, I think. ;)
2020-10-26 8:5:53 (GMT)
Stranded clauses are clauses one would presumably want to save one day.
2020-10-26 8:17:35 (GMT)
If you don't like stranded: Sentinelese clauses, because you leave them alone? (https://en.wikipedia.org/wiki/Sentinelese)
2020-10-26 8:20:23 (GMT)
But you don't leave them alone, you delete them, so it would not improve much on orphan deletion. The main difference is that it is much less likely a Sentinelese will ever hear about this technique than an orphan.
2020-10-26 8:36:21 (GMT)
The problem with "unbacked" and other pure adjectives is that they are not nouns, so you have to always say "unbacked clause" where you could just use "orphan" before.
2020-10-26 9:1:19 (GMT)
Sophie has a valid point, but I suspect people speak seldomly enough about orphans that this would not be a big issue.
2020-10-26 9:1:33 (GMT)
It's still better than "pure literal clause elimination". ;)
2020-10-26 9:2:23 (GMT)
Still it would be nice to have a noun.
2020-10-26 9:8:15 (GMT)
What about "stray"? This has a similar meaning as orphan but also applies to objects. I also found "waif", but I didn't find the meaning for objects (https://www.merriam-webster.com/dictionary/waif) in other dictionaries, and this may be too literary a word anyway.
2020-10-26 9:9:37 (GMT)
Not sure "stray" is Simon-proof, because it makes one think of animals before objects.
2020-10-26 9:39:57 (GMT)
Stray is really cool. :)
2020-10-26 9:40:2 (GMT)
You are a genius too. :)
2020-10-26 9:40:10 (GMT)
(In addition to Ahmed.)
2020-10-26 9:40:24 (GMT)
A stray clause, stray clause elimination.
2020-10-26 9:40:27 (GMT)
(or formula)
2020-10-26 9:58:32 (GMT)
Do we still want to continue brainstorming, or are we ready for a vote?
2020-10-26 9:59:20 (GMT)
I'd propose to vote and suggest the winner to the broader community, first informally asking the people who use the word the most (e.g. Konstantin, Uwe), then perhaps in the AAR newsletter?
2020-10-26 9:59:36 (GMT)
Title "Let's kill orphans" ;)
2020-10-26 10:23:32 (GMT)
+1 for stray
2020-10-26 11:14:22 (GMT)
There
2020-10-26 11:14:42 (GMT)
's even "stray" and "strayer" as nouns, with the right meaning, for those who find "stray clause" too much of a mouthful. ;)
2020-10-26 11:14:48 (GMT)
+1 for stray and family
2020-10-27 14:7:10 (GMT)
GDPR'ed clauses
2020-10-27 15:55:24 (GMT)
Back to the paper draft: Why are the ORCIDs so incredibly ugly in this latex style? I am already considering not to put them in just because they look horrible.
2020-10-27 15:56:43 (GMT)
+1 on that... absolute garbage
2020-10-27 15:58:15 (GMT)
In the published paper, they are hidden under a nice icon.
2020-10-27 15:58:53 (GMT)
@Petar Vukmirovic or are you suggesting a new name for orphans: absolute garbage clauses?
2020-10-27 15:59:24 (GMT)
haha no, IMO the perfect name has been chosen
2020-10-27 16:0:51 (GMT)
Hey, "garbage" is not that bad. The process also resembles garbage collection a bit, doesn't it?
2020-10-27 16:1:36 (GMT)
hm.. not really, for something to be garbage collected all references to it need to disappear
2020-10-27 16:1:39 (GMT)
If such clauses are garbage, then are they composed of litter-all ?
2020-10-27 16:3:37 (GMT)
Petar Vukmirovic: hm.. not really, for something to be garbage collected all references to it need to disappear
Yeah, I was thinking of the parent-child relation as the analog of references, but it's a bit far-fetched I admit.
2020-10-27 16:3:53 (GMT)
Let's keep "stray" then :-)
2020-10-27 16:8:37 (GMT)
Sophie Tourret: In the published paper, they are hidden under a nice icon.
Oh, really? Can we somehow get the nice icons earlier than that? Or is this only done by Springer outside of Latex?
2020-10-27 16:12:8 (GMT)
Do you have an example of how it looks like after publication?
2020-10-27 16:35:16 (GMT)
Alexander Bentkamp said:
Do you have an example of how it looks like after publication?
2020-10-27 16:40:24 (GMT)
And for the code to have it even for submissions:
\def\orcid#1{\smash{\href{http://orcid.org/#1}{\protect\raisebox{-1.25pt}{\protect\includegraphics{../orcid.pdf}}}}}
...
\author{Mathias Fleury~\orcid{0000-0002-1705-3083}}
With orcid.pdf in the same folder.
2020-10-27 16:44:48 (GMT)
And it the final version, use \def\orcid#1{\orcidID{#1}}
2020-10-27 16:46:37 (GMT)
Beautiful. Thank you!
2020-10-27 17:1:58 (GMT)
Is @Mathias Fleury trying to add himself as a coauthor here? ;)
2020-10-27 17:2:21 (GMT)
Actually, as sole author! He wants to steal our paper!
2020-10-27 17:6:53 (GMT)
Too bad, Zulip does not have a :black_flag:☠️ emoji. Damn that one emoji: https://emojipedia.org/pirate-flag/, it is not printed correctly on my computer.