2020-04-16 14:50:38 (GMT)
Let's list the current paper proposals for next time here, and use :upvote: :downvote: to indicate the ones we prefer.
2020-04-16 14:51:22 (GMT)
Ok. It'd also be nice to change the day (to wednesday or friday I guess) if y'all were ok with that, or time, or both :D.
2020-04-16 14:52:42 (GMT)
For me Wed is problematic. Thu earlier would be fine. Fri is not ideal since I might be traveling (once :cant_talk: is over).
2020-04-16 14:53:7 (GMT)
Thu one hour earlier would be fine with me
2020-04-16 14:54:42 (GMT)
2020-04-16 14:55:36 (GMT)
2020-04-16 14:56:59 (GMT)
I am just going bottom up through paper proposals. If someone could help, starting top down, it will be faster.
2020-04-16 14:57:49 (GMT)
Satallax: An Automatic Higher-Order Prover, by Brown
2020-04-16 14:58:14 (GMT)
2020-04-16 14:58:19 (GMT)
2020-04-16 14:58:43 (GMT)
2020-04-16 14:59:36 (GMT)
Backing Backtracking, which goes about the advantages of chronological backtracking
http://fmv.jku.at/papers/MoehleBiere-SAT19.pdf
2020-04-16 14:59:41 (GMT)
2020-04-16 15:0:30 (GMT)
2020-04-16 15:2:10 (GMT)
2020-04-16 15:4:41 (GMT)
Sophie said:
Backing Backtracking, which goes about the advantages of chronological backtracking
http://fmv.jku.at/papers/MoehleBiere-SAT19.pdf
we could even invite Sibylle Moehle if we go for that paper...
2020-04-16 15:5:45 (GMT)
The first rule of bookclub is you don't talk about bookclub. ;)
2020-04-16 15:6:5 (GMT)
I think everything that was on the general proposal is now in this new thread.
2020-04-16 15:9:29 (GMT)
The questions that remain are until when are new proposals welcome and when do we decide on the paper.
2020-04-16 15:12:20 (GMT)
@Jasmin Blanchette what is the :large_orange_diamond: supposed to mean?
2020-04-16 15:13:51 (GMT)
A reaction to me picking :red_triangle_up: as an extra strong :upvote:?
2020-04-16 15:17:0 (GMT)
Reaction: Try that at the Bundestag election. ;)
2020-04-16 15:17:7 (GMT)
Or whatever you have in Austria...
2020-04-16 15:17:43 (GMT)
We need to decide early so we can read the paper. I'm guessing nobody is going to read it in the next couple of days. Maybe we should make up our minds by Monday noon?
2020-04-16 15:21:23 (GMT)
The big diamond is an up arrow glued with a down arrow. Like "meh?" I'm open to other emoji for that. In one case, I say "meh?" because I've read the paper already. Maybe we need an emoji for that.
2020-04-16 15:24:37 (GMT)
":shrug: "
2020-04-16 15:27:45 (GMT)
:closed_book: for already read?
2020-04-16 17:54:27 (GMT)
Is the Voronkov paper the best reference for AVATAR? IIRC it is very vague
2020-04-16 18:21:9 (GMT)
@Haniel Barbosa Is there a better presentation? Perhaps in Simon's thesis? :)
2020-04-16 18:21:52 (GMT)
I don't know, it's why I asked xD
2020-04-16 18:55:44 (GMT)
I don't know of a better presentation; what's in my thesis is a much simpler version ("abatar", as dubbed by @Jasmin Blanchette ).
2020-04-16 18:55:50 (GMT)
There are 3 or 4 papers on Avatar with varying level of formality and details about the architecture
2020-04-17 9:39:31 (GMT)
https://www21.in.tum.de/~traytel/papers/incompleteness/incompleteness.pdf
2020-04-17 9:46:50 (GMT)
@Dmitriy Traytel you wanna vote for your paper?
2020-04-17 12:22:2 (GMT)
Nah, IIRC I might have already read it.
I don't know precisely what the scope of your bookclub is. A recent paper that is on my to read list is O'Hearn's "Incorrectness Logic" (POPL 2020).
2020-04-17 12:25:3 (GMT)
@Dmitriy Traytel then you can use the :closed_book: emoji for that: :closed_book:.
2020-04-17 12:25:44 (GMT)
2020-04-17 12:26:35 (GMT)
The scope is whatever people vote for. The only argument we've had so far was about the length of the papers, not their scope. ;)
2020-04-18 9:57:51 (GMT)
Sophie said:
- Julian Backes, Chad E. Brown: Analytic Tableaux for Higher-Order Logic with Choice
Not sure if we are allowed to campaign for papers, but on the assumption that we are can I encourage others to vote for this? I think that it is important for us in the higher-order community to study Satallax closely and see why it has been so successful for so long. Is it down to implementation, or does tableaux have a fundamental advantage over superposition/resolution when it comes to higher-order?
2020-04-18 14:18:55 (GMT)
I second Ahmed's championing :)
2020-04-18 14:19:58 (GMT)
I've been meaning to look more closely into Satallax for a while but never got to it
2020-04-19 5:39:31 (GMT)
or does tableaux have a fundamental advantage over superposition/resolution when it comes to higher-order?
2020-04-19 5:46:49 (GMT)
I am very skeptical here. Consider that Satallax uses a superposition prover, E, as a backend, that it was recently still beaten by Isabelle/Sledgehammer at the competition (except that Isabelle didn't produce proofs, a requirement) [1], that it performs rather poorly (and worse than Zipperposition) on Sledgehammer-generated benchmarks, and that it was highly optimized for the TPTP (including recognition of Church numeral problems, from what I'm told -- instead of relying on HO unification). Satallax's days are counted, I promise you. ;) It's still surprisingly good, though.
[1] I can't link to the CASC web site; it's full of broken links, e.g. http://www.tptp.org/CASC/26/WWWFiles/ResultsSummary.html
2020-04-19 9:24:40 (GMT)
@Michael Färber might also be interested in enlightening us on Satallax :slight_smile:
He is also a fan of what he calls non-Herband reasoning, right?
2020-04-20 8:38:4 (GMT)
I count seven votes for
and six votes for
(i.e. Satallax). Shall we make our lives easier and just elect AVATAR as the next paper and Satallax as the following one? The algorithm of copying over all proposals from one time to another is quadratic. My proposal would flatten the curve. ;)
2020-04-20 11:10:2 (GMT)
It's past noon (Paris time), and since nobody protested, I proclaim AVATAR the winner.