2020-02-27 22:42:32 (GMT)
@Alexander Bentkamp @Petar Vukmirovic : I'm trying renaming AppVarSup to VarSup but I'm not entirely happy yet. The thing is: We have two "app var" Sup rules: The expensive one DupSup and the cheap one (App)VarSup. In principle they should be called AppVarDupSup and AppVarSup or something, but that's too long and DupSup is too good to change. But still we need to think of the series
FluidSup > DupSup > (App)VarSup (and finally Sup over here)
where > means "subsumes". Any ideas?
2020-02-28 8:13:52 (GMT)
One idea is to call it FlexSup becuase it just does unification between two flex terms.
2020-02-28 9:10:16 (GMT)
Love it!! :)
2020-02-28 9:19:32 (GMT)
@Jasmin Blanchette about pragmatic mode
2020-02-28 9:21:14 (GMT)
I would not disable FlexSup from base, because that means we have to reevaluate everything
2020-02-28 9:22:23 (GMT)
However, like in Ehoh, I would create a competitive configuration that does not use FlexSup
2020-02-28 9:22:46 (GMT)
and a pragmatic version that uses very shallow unification and avatar for example
2020-02-28 9:36:30 (GMT)
OK for base.
How many new configs do you want to create now? Two?
2020-02-28 9:37:12 (GMT)
And what would they be called?
2020-02-28 9:46:4 (GMT)
Two.
2020-02-28 9:46:15 (GMT)
The first one would be competitive and the second one pragmatic
2020-02-28 9:46:56 (GMT)
The first one includes all the parameters that significantly helped base (that is probably only no FlexSup)
2020-02-28 9:47:25 (GMT)
and the second one is the same as the first one only with pragmatic mode of our unification algorithm with very shallow depth (to imitate LFHO sup as much as possible)
2020-02-28 9:47:48 (GMT)
and of course, as we agreed in the email the third one would be zip-core-portfolio
2020-02-28 9:50:35 (GMT)
Zip-core-portfolio is what I'd call Zip, right? Cf. Leo & Satallax.
2020-02-28 9:51:15 (GMT)
Is competitive = best for TPTP (or CASC) and pragmatic = best for SH still?
2020-02-28 9:52:18 (GMT)
We could think of clearer names, like \lambdaZip-competitive vs. \lambdaZip-hammer; or -miami vs. -cambridge. ;)
2020-02-28 9:52:55 (GMT)
Makes sense to me. It's a bit like hoboa.
2020-02-28 10:4:54 (GMT)
BTW Petar I added an @PETAR in the text. We need to document better which rules etc. are in -full. I hope
2020-02-28 10:5:55 (GMT)
\lambdaDemodExt is not one of them, because the rule is (AFAWK) incomplete. ;)
2020-02-28 10:6:31 (GMT)
BTW I'm now introducing a new naming distinction: \lambdaDemod is the 2-conclusion version of \lambdaDemodExt. The whole reason why I put Ext in the name is because of the presence of the third conclusion.
2020-02-28 10:6:53 (GMT)
Please reflect in the code when you have a chance so we don't go crazy (and similarly for the new FlexSup).
2020-02-28 10:12:37 (GMT)
Jasmin Blanchette said:
Is competitive = best for TPTP (or CASC) and pragmatic = best for SH still?
Since we have very small pool of TPTP problems, I am afraid that there will almost no difference between pragmatic and competitive
2020-02-28 10:16:32 (GMT)
Jasmin Blanchette said:
BTW I'm now introducing a new naming distinction: \lambdaDemod is the 2-conclusion version of \lambdaDemodExt. The whole reason why I put Ext in the name is because of the presence of the third conclusion.
LambdaDemodExt is not even implemented. LambdaDemod is implemented as an option in demodulation machinery of Zip, which just allows it go below lambdas. Implementing LambdaDemodExt would meen copying a lot of code since additional literal needs to be added, and I do not think it is worth it. LambdaDemod is off as all configurations are based on base
2020-02-28 10:23:7 (GMT)
Then let's just have pragmatic.
2020-02-28 10:23:45 (GMT)
I know about LambdaDemod impl. I'm just saying "if the code that does lambdaDemod calls it lambdaDemodExt, please rename your code".
2020-02-28 10:24:40 (GMT)
no no the option is called --lambda-demod
2020-02-28 10:25:2 (GMT)
Good. I've now officially added that name in the paper (lambdaDemod).
2020-02-28 10:25:32 (GMT)
OK.
So let's recapitulate what I need to add
2020-02-28 10:26:21 (GMT)
2020-02-28 10:26:28 (GMT)
About the names
2020-02-28 10:26:59 (GMT)
portfolio without backends is called Zip-core
portfolio with backends is Zip
2020-02-28 10:27:4 (GMT)
I like to work with names.
2020-02-28 10:27:21 (GMT)
Zip-core
Zip-pragmatic
2020-02-28 10:27:34 (GMT)
But I'm even proposing a new renaming: -core -> -uncoop.
2020-02-28 10:27:45 (GMT)
I call these versions "uncooperative".
2020-02-28 10:27:58 (GMT)
We talk about the "cooperative" architecture, after alll.
2020-02-28 10:28:24 (GMT)
We could even write Satallax-uncoop vs. Satallax-coop. That would be the clearest.
2020-02-28 10:28:51 (GMT)
And Zip-coop would be portfolio + coop.
2020-02-28 10:34:41 (GMT)
Please check the current state of Fig. 5 and let me know what you think.
2020-02-28 10:34:57 (GMT)
ok , checking back to you in 5
2020-02-28 10:35:41 (GMT)
Also, please define more precisely how -full is different from -base.
2020-02-28 10:36:5 (GMT)
"full implements the complete version of our calculus" is too vague. Which rules are removed? Which are added? Anything happens with unification?
2020-02-28 10:36:16 (GMT)
No hurry. ;)
2020-02-28 10:36:33 (GMT)
I'll be sitting on trains for the next 6 hours.
2020-02-28 10:38:20 (GMT)
ok I see.
2020-02-28 10:38:28 (GMT)
I like the table as it is now
2020-02-28 10:38:42 (GMT)
but as far as I understood you, we should remove -base from the table
2020-02-28 10:38:56 (GMT)
I think it is confusing to have it also next to pragmatic
2020-02-28 10:39:26 (GMT)
and we will use some space to explain both in the text which might not be the best use of space
2020-02-28 10:39:56 (GMT)
I will explain more about the configurations and also say that we run FO Ehoh or Vampire on FO problems and HO Ehoh or Vampire on HO problems
2020-02-28 13:26:36 (GMT)
Jasmin Blanchette:
@Petar Vukmirovic I'm thinking we should perhaps use a slightly different notation for features in the tables.
When I see a row "Base +Foo +Bar", I wonder if the last column is cummultative (Base+Foo+Bar) or not (Base+Foo).
How about "B+Foo" and "B+Bar", and of course "B-Baz"?
Just B. We'd call the base B.
I'm not sure; what do you think?
2020-02-28 13:28:54 (GMT)
I think that the text is quite clear because we have a cumulative effect for -NE,-PA which we denote by comma
2020-02-28 13:29:4 (GMT)
So I think it is quite clear as is
2020-02-28 13:29:31 (GMT)
And also we have +LS1 and +LS1024 so it is quite unlikely someone will think it is cumultaive
2020-02-28 13:47:26 (GMT)
OK.
2020-02-28 13:47:30 (GMT)
Thanks Alex.
2020-02-28 13:47:40 (GMT)
I'm still learing to use Zulip. ;)
2020-02-28 15:6:33 (GMT)
I'm a bit behind, but is Zipperposition useful for SH these days?
2020-02-28 15:21:18 (GMT)
I haven't yet build the three binaries. :S
2020-02-28 15:21:24 (GMT)
But the data looks awesome.
2020-02-28 15:21:48 (GMT)
In our paper, Zip is the winner, before Vampire, by a few problems.
2020-02-28 15:21:56 (GMT)
That's Zip portfolio + Ehoh.
2020-02-28 15:22:3 (GMT)
note that part of it is cooperation with Ehoh
that I plan to improve as soon as I have time (e.g. next week)
2020-02-28 15:23:15 (GMT)
Jasmin Blanchette said:
That's Zip portfolio + Ehoh.
sorry, the correct pronunciation is "Ehhhoooooooooooooohhhhh :wave: "
2020-02-28 15:28:16 (GMT)
Results without backends are also quite good:
On Sh-Lambda pure Zip solves 619, and when it is hooked with Ehoh it solves 710 problems
2020-02-28 15:29:43 (GMT)
@Jasmin Blanchette we have a problem
2020-02-28 15:31:0 (GMT)
What I previosly wrote was a portfolio for FO was actually without backends
because it was special FO portfolio mode of Zip
2020-02-28 15:31:14 (GMT)
I will run ho portfolio now and update the res
2020-02-28 15:32:0 (GMT)
Petar Vukmirovic said:
Results without backends are also quite good:
On Sh-Lambda pure Zip solves 619, and when it is hooked with Ehoh it solves 710 problems
I like the idea of using pure Zipperposition for SH, in practice :). E is also going to be called in parallel anyway?
2020-04-09 8:34:28 (GMT)
This morning I modernized some of the notations in our -Sup journal submission.
2020-04-09 8:34:49 (GMT)
I'm now avoiding floor and ceiling notations also for the term order.
2020-04-09 8:35:12 (GMT)
My next goal is to define a meta-quasiorder, next to the metaorder we also have.
2020-04-09 8:35:23 (GMT)
I guess with the proofs this should add one page.
2020-04-09 8:36:11 (GMT)
The difference between the meta-quasiorder and the reflexive closure of the metaorder would be that the former could orient X b >~ X a and stuff like that.
2020-04-09 8:37:0 (GMT)
Formally, "stuff like that" means where
2020-04-09 8:38:11 (GMT)
for each , either or and the two terms are not of function type (or type variable).
2020-04-09 8:39:18 (GMT)
I think I convinced Petar to implement it, once we have a proper textual description.
2020-04-09 8:40:16 (GMT)
Anyway, since the calculus is now (after Alex's change shortly before the submission) parameterized by a pair of (quasi)orders , it makes total sense to provide a pair of meta(-quasi)orders as well.
2020-04-09 8:41:9 (GMT)
Petar and I are curious to see how many problems we'll gain. I'm guessing we'll go from 1600 or so proved problems to 1603 or so -- plus 3.