Simon Cruanes
2021-01-08 15:32:30 (GMT)
among other things, this talk about automation seems interesting. I imagine @Jasmin Blanchette knows this PhD student, it's the same university, correct?
Gabriel Ebner
2021-01-08 15:41:4 (GMT)
I imagine Jasmin Blanchette knows his PhD student, [...]
You have typed one "t" too many. :smile:
Jasmin Blanchette
2021-01-08 16:23:43 (GMT)
Reminds me of the sign in Munich that says "Plakattieren verboten".
Simon Cruanes
2021-01-08 16:28:55 (GMT)
Heh, I didn't check, but I suspected so :grinning:
Simon Cruanes
2021-01-08 17:32:53 (GMT)
ah well, :wave: @Jannis Limperg
Jannis Limperg
2021-01-08 18:12:31 (GMT)
Hi! I'm surprised and delighted someone found the talk interesting. (Also, I forgot I was on this Zulip.)
Simon Cruanes
2021-01-08 18:13:19 (GMT)
well if there are people interested in the intersection of ITP and ATP, I think there's a chance they're here :stuck_out_tongue:
Jannis Limperg
2021-01-08 18:18:20 (GMT)
Fair. The thing I talked about is currently extremely naive. If anyone has ideas/literature on what a modern auto for a dependently-typed ITP should look like, I'm all ears. So far I've been looking into Isabelle, ACL2, SMT, auto2 and sauto for inspiration.
Simon Cruanes
2021-01-08 18:18:52 (GMT)
I was going to suggest auto2 indeed.
Jannis Limperg
2021-01-08 18:28:15 (GMT)
This seems to come up a lot. What is it that you like about it? I understand the methodology is very different from the established systems -- saturation + e-matching vs mostly backwards search + simplification.
Simon Cruanes
2021-01-08 18:30:1 (GMT)
Well, having E-matching means it can apply rewrite rules (simp rules?) in a more robust way. Saturation means all branches are explored in a more fair way, rather than with backtracking where the first branch picked in a choice is inherently favored.
Jannis Limperg
2021-01-08 18:36:20 (GMT)
I see. Would a best-first backtracking search, where one could switch between, say, the branches corresponding to a disjunction based on which branch currently looks better, provide similar fairness?
Simon Cruanes
2021-01-08 18:48:47 (GMT)
Possibly. I'm also historically partial to encoding this kind of backtracking into SAT in such a way that true boolean literals indicate the current branch. @Guillaume Bury did something like that in archsat. But that's more a thing I like and not general wisdom.
Jannis Limperg
2021-01-08 19:2:35 (GMT)
All right, thanks!