Jasmin Blanchette
2020-07-02 10:34:57 (GMT)
Anybody knows where the "Start of CASC" is? It's not streaming somehow.
Jasmin Blanchette
2020-07-02 10:35:5 (GMT)
It should have started 4 minutes ago.
Pascal Fontaine
2020-07-02 10:44:12 (GMT)
Just sent you a mail...
Jasmin Blanchette
2020-07-02 10:44:47 (GMT)
Thanks. That's confusing. The program clearly indicated it as part of Track A. :S
Simon Cruanes
2020-07-02 12:45:12 (GMT)
For reference, the race is on there: http://www.tptp.org/CASC/J10/WWWFiles/Racing.html
Pascal Fontaine
2020-07-02 12:53:53 (GMT)
Currently witnessing impressive performance of Zipperposition...
Petar Vukmirovic
2020-07-02 12:58:10 (GMT)
Thanks :slight_smile: the harder problems are only coming though :slight_smile:
Simon Cruanes
2020-07-02 12:58:32 (GMT)
take a screenshot while it's time!
Jasmin Blanchette
2020-07-02 13:11:25 (GMT)
Now is time to take a screenshot. ;)
Jasmin Blanchette
2020-07-02 13:12:11 (GMT)
Seriously, knowing how much Petar has been tuning Zip, unless Geoff has chosen the problems deliberately so that it loses, it should win with a decent margin over last year's Satallax.
Pascal Fontaine
2020-07-02 13:16:40 (GMT)
In 15 problems, you will have already won against Satallax 3.5 and Vampire. CVC4, Satallax 3.4 and Leo III are still potentially challenging.
Jasmin Blanchette
2020-07-02 13:17:58 (GMT)
"Potentially". There's only 3.4 that's challenging but it's starting to hit a wall as problems get harder.
Jasmin Blanchette
2020-07-02 13:18:23 (GMT)
The others were already failing to solve several easy problems. They won't be a match on the harder problems.
Petar Vukmirovic
2020-07-02 13:19:0 (GMT)
I think we are too easy to categorize something as hard or not :slight_smile:
Petar Vukmirovic
2020-07-02 13:19:37 (GMT)
You would be surprised how many "easy" looking problems are hard to solve with a particular method/prover
Jasmin Blanchette
2020-07-02 13:19:39 (GMT)
BTW Leo-II seems to be crippled. I'm betting its FO backend E is not installed properly.
Jasmin Blanchette
2020-07-02 13:20:15 (GMT)
For sure, but people who don't get the easy problem usually haven't tuned their prover against the TPTP library and as a result don't win.
Petar Vukmirovic
2020-07-02 13:20:57 (GMT)
I looked at a random proof output (http://www.tptp.org/CASC/J10/WWWFiles/Results/TEQ/LEO-II---1.7.0/LCL715%5E1) and it seems it called E successfuly on this one
Jasmin Blanchette
2020-07-02 13:22:1 (GMT)
Good thinking. It's amazingly weak then. It used not to be so dissimilar from Satallax.
Petar Vukmirovic
2020-07-02 13:23:4 (GMT)
Maybe there is another configuration issue?
Petar Vukmirovic
2020-07-02 13:24:39 (GMT)
DOes anyone have meeting ID for Zoom?
Jasmin Blanchette
2020-07-02 13:24:40 (GMT)
Problem selection is possibly part of the answer.
Petar Vukmirovic
2020-07-02 13:25:6 (GMT)
Geoff invited me over email, but I lost the ID somewhere in the sea of emails
Jasmin Blanchette
2020-07-02 13:25:57 (GMT)
To go to the CASC room?
Jasmin Blanchette
2020-07-02 13:26:18 (GMT)
If you're registered for IJCAR, there's a URL in the email with ZOOM INVITATION INSIDE in the title.
Simon Cruanes
2020-07-02 13:26:18 (GMT)
There's a CASC room? :surprise:
Jasmin Blanchette
2020-07-02 13:26:23 (GMT)
Of course. ;)
Jasmin Blanchette
2020-07-02 13:26:38 (GMT)
It's been going on since 12:30.
Jasmin Blanchette
2020-07-02 13:26:43 (GMT)
With all your favorite hackers.
Petar Vukmirovic
2020-07-02 13:27:20 (GMT)
ok ok thanks :slight_smile:
Pascal Fontaine
2020-07-02 13:28:22 (GMT)
Screenshot-at-2020-07-02-15-26-05.png
For historical reference
Haniel Barbosa
2020-07-02 13:38:58 (GMT)
I'm glad Leo-II participates so CVC4 does not look as bad :)
Simon Cruanes
2020-07-02 13:39:14 (GMT)
every category needs its muscadet!
Haniel Barbosa
2020-07-02 13:51:16 (GMT)
So what is the talk about having a SLH division again? That is something that I'd feel more motivated to improve for rather than THF...
Petar Vukmirovic
2020-07-02 13:52:11 (GMT)
I think it might be possible to improve CVC4 significantly since instantiation-based techniques can be quite good on THF
Haniel Barbosa
2020-07-02 13:53:42 (GMT)
ah, really? I did not know that had been observed.
Haniel Barbosa
2020-07-02 13:54:7 (GMT)
One thing that'd help CVC4 is doing more than lambda-free E-matching :)
Petar Vukmirovic
2020-07-02 13:54:23 (GMT)
actually I can help you there
Sophie Tourret
2020-07-02 13:54:34 (GMT)
Well, we're working on coming up with decent SMT instantiation techniques for higher-order but currently lambda-free :working_on_it:
Haniel Barbosa
2020-07-02 13:55:2 (GMT)
Sophie Tourret
2020-07-02 13:55:9 (GMT)
your help would be welcome!
Sophie Tourret
2020-07-02 13:55:34 (GMT)
(but maybe we should get the experimental results of the lambda-free version first...)
Petar Vukmirovic
2020-07-02 13:57:48 (GMT)
sorry I started typing
Petar Vukmirovic
2020-07-02 13:57:54 (GMT)
but then got interrupted :slight_smile:
Petar Vukmirovic
2020-07-02 13:58:4 (GMT)
there is a fragment of HO unification we discovered
Petar Vukmirovic
2020-07-02 13:58:14 (GMT)
and it is very powerful on matching
Simon Cruanes
2020-07-02 13:59:9 (GMT)
you mean, more than classic HO matching as implemented in some ITPs, right?
Sophie Tourret
2020-07-02 13:59:37 (GMT)
Are you going to talk about it in your FSCD talk?
Haniel Barbosa
2020-07-02 14:0:57 (GMT)
I think I remember this being mentioned somewhere.. do you have a link? It'd be quite interesting to try exploring that in an SMT solver
Sophie Tourret
2020-07-02 14:1:10 (GMT)
I think I already heard you talk about it last time I traveled to Amsterdam (long, long ago in a parallel dimension)
Petar Vukmirovic
2020-07-02 14:1:20 (GMT)
I will talk about that in 2 hours at FSCD
Petar Vukmirovic
2020-07-02 14:1:33 (GMT)
which is a shameless way to promote my talk as well
Sophie Tourret
2020-07-02 14:1:34 (GMT)
I thought so!
Petar Vukmirovic
2020-07-02 14:1:38 (GMT)
I will give you a link on our paper
Haniel Barbosa
2020-07-02 14:2:2 (GMT)
I'll make sure I don't miss it!
Petar Vukmirovic
2020-07-02 14:2:14 (GMT)
Sophie Tourret
2020-07-02 14:2:23 (GMT)
I already shamelessly advertised your talk yesterday at Ijcar because after Ahmed's talk there was a question about ho unification.
Petar Vukmirovic
2020-07-02 14:2:39 (GMT)
Thanks Sophie :slight_smile:
Petar Vukmirovic
2020-07-02 14:4:52 (GMT)
Jasmin Blanchette
2020-07-02 14:5:25 (GMT)
By which Petar means: You should actually read the whole paper. ;)
Haniel Barbosa
2020-07-02 14:6:30 (GMT)
Will do :)
Jasmin Blanchette
2020-07-02 14:23:23 (GMT)
And since it won the best young researcher paper award, you won't be wasting your time. ;)
Jasmin Blanchette
2020-07-02 14:23:34 (GMT)
(Spoiler alert.)
Simon Cruanes
2020-07-02 14:23:55 (GMT)
so proud of his students :)
Haniel Barbosa
2020-07-02 14:26:47 (GMT)
Awesome!
Sophie Tourret
2020-07-02 15:35:4 (GMT)
Anyone knows what HO unification à la Ziliani-Sozeau is?
Petar Vukmirovic
2020-07-02 15:35:25 (GMT)
Was wondering the same :slight_smile:
Petar Vukmirovic
2020-07-02 15:35:32 (GMT)
Who dares to ask the question? :slight_smile:
Simon Cruanes
2020-07-02 15:36:7 (GMT)
I imagine it's about the paper on the new Coq refiner unification algorithm
Jasmin Blanchette
2020-07-02 15:36:10 (GMT)
I'm guessing it's that:
https://www.irif.fr/~sozeau/research/publications/drafts/unification-jfp.pdf