Ahmed B
2020-03-28 13:49:15 (GMT)
Has the Matryoshka team decided on names for the various calculi you are working on? The following is from a comment by @Jasmin Blanchette on a draft of the combinatory superposition paper:
BTW although we don't use it explicitly in our paper,
the name we intend to use in the journal submission is "clausal higher-order
superposition" (and for its predecessor: "$\lambda$-free clausal higher-order
superposition"). We're going to submit the two articles in February and March.
Perhaps we can all agree on good, different names, e.g. "clausal combinatory
higher-order superposition". ("Clausal" is used as a synonym for
"Boolean-free".) More adjectives can of course be added, e.g. "polymorphic",
"intentional". Regardless, "lambda superposition" is also fine by me.
However, I noted that in @Petar Vukmirovic PAAR submission, he calls the calculus PFHOL, where "PF" stand for "predicate-free". Has there been a change in naming? It would be nice to fit the combinatory calculus into the overall naming scheme if possible.
Petar Vukmirovic
2020-03-28 13:58:59 (GMT)
The text of the paper has been changed to image.png
Petar Vukmirovic
2020-03-28 13:59:57 (GMT)
Jasmin has immediately reminded me that I should be consitent with the naming in Alex' paper
Jasmin Blanchette
2020-03-28 15:53:18 (GMT)
The new name is clausal \lambda-superposition.
Jasmin Blanchette
2020-03-28 15:53:34 (GMT)
As for the PAAR submission, I've already told Petar. ;)
Jasmin Blanchette
2020-03-28 15:54:0 (GMT)
For the previous calculus, clausal lambda-free superposition.
Jasmin Blanchette
2020-03-28 15:54:12 (GMT)
For the future calculus, \lambda-superposition.
Jasmin Blanchette
2020-03-28 15:54:47 (GMT)
You can write "lambda superposition" if you prefer (cf. \lambda-calculus vs. lambda calculus).
Jasmin Blanchette
2020-03-28 15:55:4 (GMT)
We use the new name in our recent JAR submission
Jasmin Blanchette
2020-03-28 15:55:13 (GMT)
and will use it in our forthcoming LMCS submission.
Jasmin Blanchette
2020-03-28 15:56:44 (GMT)
Ah, now I see Petar's answer. It didn't load at first!