2020-06-29 7:12:41 (GMT)
This thread is to discuss about the talks presented in the 3rd session of PAAR 2020:
2020-06-29 9:49:3 (GMT)
All papers are available on the web page: http://paar2020.gforge.inria.fr/
2020-06-30 11:25:53 (GMT)
Session 3 will start in 5min!
2020-06-30 12:29:56 (GMT)
To capture the kind of relation mentioned by @Uwe Waldmann (that a predicate is a definition build using other predicate) I think it would help a lot that the features representing a symbol capture a common occurrence in a literal of several symbols.
2020-06-30 12:30:38 (GMT)
Some kind of graph linking various symbols maybe?
2020-06-30 12:32:46 (GMT)
It would be interesting to see if this emerged by itself from using GNN on the problem structure representation.
2020-06-30 12:37:24 (GMT)
Related to first talk: @Petar Vukmirovic it'd be lovely to get your slides somewhere, it was early and my brain takes a little while to boot (even though I know most of the content already).
I liked the charts a lot btw :slight_smile:
2020-06-30 12:39:18 (GMT)
We plan to upload the slides on the PAAR website.
2020-06-30 12:44:19 (GMT)
Here is the link to my presentation
https://docs.google.com/presentation/d/1I-NcjgNCHQcFrwA3OJ1_-6S3TfCJ1qo2X4i_9PlRP1E/edit?usp=sharing
2020-06-30 12:46:43 (GMT)
Thanks :slight_smile:
2020-06-30 12:47:2 (GMT)
Slide 34 is my favorite. It shows the nonlinear impact that solving two more problems can have. :)
2020-06-30 12:48:13 (GMT)
I don't follow your point @Jasmin Blanchette . Can you develop?
2020-06-30 12:54:13 (GMT)
I mean, what has slide 34 to do with what happens when you can solve two extra problems?
2020-06-30 12:56:15 (GMT)
The bars are clearly not proportional. A difference of 2 problems translates into a 20 or so pixel difference. Clearly, the bars were not measured properly...
2020-06-30 12:56:22 (GMT)
@Petar Vukmirovic regarding the unification modulo boolean, I understand that you remove terms occurring in both lists so it works modulo AC of and , because you don't necessarily know in advance what to unify with what. That's also why you sort by head+weight.
But would it make sense to use a kind of pre-unification (a first-order/lfHOL unification unifiability check) to do that instead? That'd be more robust I think. Doing this kind of check is already used in subsumption to prune impossible permutations early.
2020-06-30 12:56:57 (GMT)
Jasmin Blanchette said:
The bars are clearly not proportional. A difference of 2 problems translates into a 20 or so pixel difference. Clearly, the bars were not measured properly...
So you meant slide 35 and later then, not 34!
2020-06-30 12:57:4 (GMT)
Sorry, it was 35.
2020-06-30 12:57:20 (GMT)
Not 34! = 34 * 33 * 32 * ... * 1 indeed. ;)
2020-06-30 13:1:30 (GMT)
Simon Cruanes said:
Petar Vukmirovic regarding the unification modulo boolean, I understand that you remove terms occurring in both lists so it works modulo AC of and , because you don't necessarily know in advance what to unify with what. That's also why you sort by head+weight.
@Petar Vukmirovic Are you aware of cases where the unification fails because of the ordering or is this completely impossible?
2020-06-30 13:2:23 (GMT)
Simon Cruanes said:
Petar Vukmirovic regarding the unification modulo boolean, I understand that you remove terms occurring in both lists so it works modulo AC of and , because you don't necessarily know in advance what to unify with what. That's also why you sort by head+weight.
But would it make sense to use a kind of pre-unification (a first-order/lfHOL unification unifiability check) to do that instead? That'd be more robust I think. Doing this kind of check is already used in subsumption to prune impossible permutations early.
Well even if you decide to delay, you need to choose which disagreements you will create
2020-06-30 13:2:32 (GMT)
That is which pairs will be created
2020-06-30 13:2:47 (GMT)
In the example in the slides, seems to me that using a FO unifiability check would make it clear that p a and q a would not match, so clearly you need to commute.
2020-06-30 13:2:58 (GMT)
Oh I'm not talking about delaying.
2020-06-30 13:3:57 (GMT)
Ok, when I saw preunification, I thought of delaying like in Huet's preunification
2020-06-30 13:5:25 (GMT)
So what you mean is, some different filter applied rather than sorting?
2020-06-30 13:5:58 (GMT)
Sophie Tourret said:
Simon Cruanes said:
Petar Vukmirovic regarding the unification modulo boolean, I understand that you remove terms occurring in both lists so it works modulo AC of and , because you don't necessarily know in advance what to unify with what. That's also why you sort by head+weight.
Petar Vukmirovic Are you aware of cases where the unification fails because of the ordering or is this completely impossible?
It is for sure possible, that something like that will happen, but experience is that in practice this works well
2020-06-30 13:6:15 (GMT)
The reason is that you have huge common part that you remove by first algorithm step
2020-06-30 13:6:39 (GMT)
common ground part that is
2020-06-30 13:6:40 (GMT)
Yes that makes sense, but it seems very restrictive that it requires exact syntactic equality
2020-06-30 13:7:1 (GMT)
and the second part puts variables at the end roughly
2020-06-30 13:7:10 (GMT)
I was suggesting that if you have pairs of terms that are FO-unifiable (and don't pre-unify with anything else) you can still prune them early.
2020-06-30 13:7:31 (GMT)
or s/don't pre-unify/cannot unify/
2020-06-30 13:7:31 (GMT)
I see.. Yeah that is indeed another option
2020-06-30 13:22:45 (GMT)
Here is the github repo for tesc: https://github.com/skbaek/tesc related to the 4th talk of the session
2020-06-30 13:41:23 (GMT)
In his talk, Seulkee Baek said his motivation is working on a hamme for Lean. Anyone here knows what is the state of automation in Lean?
2020-06-30 13:43:18 (GMT)
I don't drink coffee in the evening.
2020-06-30 13:44:32 (GMT)
Very little, I played with Lean in the autumn.
2020-06-30 13:44:34 (GMT)
I guess Seul was probably talking about this: https://github.com/leanprover-community/mathlib/pull/1083
2020-06-30 13:45:12 (GMT)
@Gabriel Ebner has done some work toward implementing a Lean hammer, but it's not integrated into mathlib.
2020-06-30 13:49:45 (GMT)
(@Gabriel Ebner I think I need to subscribe you to this stream.)
2020-06-30 13:50:16 (GMT)
Work on a common proof format for ATPs would benefit a lot of ITPs, just look at how many hammers already exist :-)
2020-06-30 13:53:26 (GMT)
I think the challenge is not theoretical, but political.
2020-06-30 13:57:25 (GMT)
Totally. Still, the communities are small enough that format wars can't be afforded!
Afaik all the major ITPs have some form of sequent calculus, and it's very explicit in the way it handles assumptions, so I think it's a good design choice. The problem is to agree on a concrete format, and TESC could be it? But right now the power is in the hands of Geoff and the CASC competition organizers, since as we know the only way to force a proof format to be used is to mandate it for competitions :)
2020-06-30 13:58:14 (GMT)
Rob Lewis said:
Gabriel Ebner has done some work toward implementing a Lean hammer, but it's not integrated into mathlib.
Yes, there's a prototype for a hammer (see the slides here for experimental results). But the big issue is that Lean 3 is pretty slow for this kind of application (most of the problems time out before even calling the external prover). I plan to resume this work once Lean 4 is in a usable state.
2020-06-30 15:0:53 (GMT)
Simon Cruanes said:
But right now the power is in the hands of Geoff and the CASC competition organizers, since as we know the only way to force a proof format to be used is to mandate it for competitions :)
Us prover developers also have some power if Vampire, E, and Zipperposition could agree then that's a step forward...
2020-06-30 15:2:48 (GMT)
Let's not forget Leo3, satallax, the cop family… :wink:
2020-06-30 15:3:11 (GMT)
Now you are getting really ambitious!
2020-06-30 15:7:34 (GMT)
Well, if we take the current higher order provers, it's basically {E,Vampire,Zipperposition,Leo3,Satallax}, so that's a fun party already.
2020-06-30 15:10:23 (GMT)
Why are SMT solvers always forgotten? CVC4 can do HO as well, as can a veriT prototype.
2020-06-30 15:10:39 (GMT)
Oh my bad. Indeed.