Simon Cruanes
2020-03-26 13:22:59 (GMT)
IJCAR 2020
- iProver + superposition
- Solving bit-vectors with MCSAT: explanations from bits and pieces
Jasmin Blanchette
2020-03-26 13:26:51 (GMT)
I donno. One week from now?
Jasmin Blanchette
2020-03-26 13:26:54 (GMT)
It's a short paper.
Jasmin Blanchette
2020-03-26 13:27:31 (GMT)
I'm voting against MCSAT. The paper won't be interesting to those who don't know MCSAT. (I wouldn't object to the original MCSAT paper though.)
Sophie
2020-03-26 14:25:37 (GMT)
Hi, I would also be interested (at least in theory, I don't know if I will have the time). In the IJCAR list, the paper I am the most interested in is the one by @Haniel Barbosa : Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis (I could not review it because Haniel is an author but I would have liked to T_T ). I would also be happy reading the iprover paper.
Haniel Barbosa
2020-03-26 14:29:55 (GMT)
I thought you might be interested indeed, @Sophie :slight_smile:
Simon Cruanes
2020-03-26 14:37:47 (GMT)
Maybe for people more involved in Zipperposition/E: "Subsumption Demodulation in First-Order Theorem Proving" by the Vampire peeps.
Ahmed B
2020-03-26 18:2:51 (GMT)
How does this work. Someone picks a paper, reads it and then provides their understanding to others during a conference call? If so, I am interested and the paper I would like to read is:
A Comprehensive Framework for Saturation Theorem Proving
Jasmin Blanchette
2020-03-26 18:24:21 (GMT)
@Ahmed B right now the idea was we all read the same paper independently and meet again on some video chat room (Sophie knows a good address). But the concept is still young (1 day old) and evolving. ;) As for the paper you mentioned, we're planning to make it more friendly by the 18 April, so it's probably better to wait.
Ahmed B
2020-03-26 20:35:24 (GMT)
Jasmin Blanchette said:
Ahmed B right now the idea was we all read the same paper independently and meet again on some video chat room (Sophie knows a good address). But the concept is still young (1 day old) and evolving. ;) As for the paper you mentioned, we're planning to make it more friendly by the 18 April, so it's probably better to wait.
Ok, well if it is one paper, I am happy to go with the iProver one. Sounds intriguing.
Simon Cruanes
2020-03-26 20:58:13 (GMT)
"Layered Clause Selection for Theory Reasoning" @Petar Vukmirovic I think it'd interest us both :)
Petar Vukmirovic
2020-03-30 15:52:35 (GMT)
Simon Cruanes said:
"Layered Clause Selection for Theory Reasoning" Petar Vukmirovic I think it'd interest us both :)
Maybe next week :)
Jasmin Blanchette
2020-04-02 15:59:17 (GMT)
Shall we try to get our hands on "Layed Clause Selection"?
Jasmin Blanchette
2020-04-02 15:59:45 (GMT)
Oh it's on arXiv, nice.
Jasmin Blanchette
2020-04-02 16:0:0 (GMT)
Are we only reading short papers?
Simon Cruanes
2020-04-02 17:8:24 (GMT)
I don't know, but it sounds like a good idea, it takes less time
Petar Vukmirovic
2020-04-02 17:11:50 (GMT)
Maybe we can prefer short ones, but if there are longer papers that are interesting I think we should not avoid them
Jasmin Blanchette
2020-04-02 17:18:45 (GMT)
I see. At this book club, we don't read books but papers, because books are too long; but we don't read papers either but only short ones. ;)
Petar Vukmirovic
2020-04-02 17:27:20 (GMT)
Petar Vukmirovic
2020-04-02 17:28:22 (GMT)
Now I was wondering if there is any classical paper in any field of automated reasoning that we never had time to read/discuss but you think is important?
Jasmin Blanchette
2020-04-02 17:36:9 (GMT)
Donno what you've read or not.
Jasmin Blanchette
2020-04-02 17:37:19 (GMT)
I keep on citing the "NOT" paper but I've never read it:
https://dl.acm.org/doi/pdf/10.1145/1217856.1217859
Jasmin Blanchette
2020-04-02 17:37:28 (GMT)
About SMT.
Petar Vukmirovic
2020-04-02 18:24:36 (GMT)
Would love to read that.
Sophie
2020-04-02 18:41:26 (GMT)
too bad it doesn't qualify as a short paper... ^^
Haniel Barbosa
2020-04-02 19:33:18 (GMT)
I never read it either
Jasmin Blanchette
2020-04-02 19:42:43 (GMT)
Shame on you. :)
Jasmin Blanchette
2020-04-02 19:43:11 (GMT)
(I realize that's the kettle calling the pot black.)
Jasmin Blanchette
2020-04-03 7:47:48 (GMT)
Feedback from one of the authors to my email yesterday:
Dear Jasmin,
The sentence
If a conflict exists between two rules t → s and t → u (with t ≻ s ≻ u), ...
suggests that your ordering ≻ is total
This only applies if s and u are comparable (which is always true if e.g. we only use ground equalities in light normalisation, but not in the general case). If the two right-hand sides s and u are incomparable, we simply keep the old binding in the index.
What's unclear with Figure 1 is how the three main reasoning modules are combined. Are they run in parallel,
interleaved? Is the given clause algorithm of 2.2 shared among them (or at least among resolution and superposition)?
This is unfortunately unclear.
They are interleaved, and clauses can be shared between them, an example is the aforementioned global propositional subsumption, where all calculi can submit clauses to the (shared) SAT solver, which are then used to simplify ground and non-ground clauses in all calculi. The given clause loop is not shared. Each calculus runs its own independent saturation loop.
We were a bit puzzled by the sentence "We use a sound approximation of the entailment relation for this purpose,
where we only apply fast rules like unit propagation or place a limit on the number of backtracks"
This means that, for e.g. global subsumption or semantic detection of axioms via SMT, we use a sound but incomplete strategy to determine entailment, like restricting the number of backjumps in the SAT algorithm. We do not require completeness for these simplifications, so we're fine with using a weaker but much faster criterion. It would be impractical for example to use the complete SAT algorithm on every global subsumption check.
Hope this clarified some things. Thanks very much for the comments, we will take them into account for our final version.
Best regards,
André
Jasmin Blanchette
2020-04-03 7:49:36 (GMT)
Am I in the wrong Zulip topic? ;)
Ahmed B
2020-04-03 7:59:41 (GMT)
Jasmin Blanchette said:
I see. At this book club, we don't read books but papers, because books are too long; but we don't read papers either but only short ones. ;)
Maybe we should focus our attention on reading abstracts.
Jasmin Blanchette
2020-04-03 9:29:31 (GMT)
By abstracts you mean short papers and tool descriptions?
Jasmin Blanchette
2020-04-03 9:29:48 (GMT)
If the worry is that this will take too much time, we can always space out the meetings even further.
Jasmin Blanchette
2020-04-03 9:30:0 (GMT)
Or individually skip some.
Jasmin Blanchette
2020-04-03 9:30:14 (GMT)
But since reading papers is part of our job descriptions, I don't see this as a waste of time.
Jasmin Blanchette
2020-04-03 9:30:38 (GMT)
I'm afraid restricting our scope to short papers would leave out 90% of interesting papers.
Jasmin Blanchette
2020-04-03 9:31:12 (GMT)
And short papers are easier to read in 15 minutes if need be; no need for a "bookclub" to motivate me to read them. ;)
Haniel Barbosa
2020-04-03 17:34:33 (GMT)
I'd rather avoid short papers. Most of the discussion is actually speculation on what the authors might have said
Jasmin Blanchette
2020-04-03 17:35:13 (GMT)
Right. ;)
Jasmin Blanchette
2020-04-04 11:39:54 (GMT)
We're a bit in a deadlock. There are three people (Ahmed, Simon, Sophie) in favor of short papers and three people (Haniel, Petar, me) in favor of long papers. And we need to choose and read a paper in the next 12 days. Any ideas, anyone?
Ahmed B
2020-04-04 12:3:58 (GMT)
Jasmin Blanchette said:
We're a bit in a deadlock. There are three people (Ahmed, Simon, Sophie) in favor of short papers and three people (Haniel, Petar, me) in favor of long papers. And we need to choose and read a paper in the next 12 days. Any ideas, anyone?
You can remove me from the short paper list. My comment was supposed to be in jest. Clearly my sense of humour is not opaque.
In any case, I am happy to go with a long paper making the numbers 4 vs 2.
Jasmin Blanchette
2020-04-04 12:10:51 (GMT)
Oh, you meant "abstracts" not "extended abstracts". I see. ;) (British humour...)
Jasmin Blanchette
2020-04-04 12:12:10 (GMT)
Regardless, I think we can go for a long paper this time. There doesn't have to be a rule against short papers, but we had a short paper last time. There's one candidate so far (the "NOT" paper about SMT). Other proposals?
Simon Cruanes
2020-04-04 15:48:59 (GMT)
I'm fine with long papers as well, btw.
Petar Vukmirovic
2020-04-04 17:11:40 (GMT)
I would also like to stress that it might be good to read papers that some of us are clueless about but other people are are experts in
Petar Vukmirovic
2020-04-04 17:11:50 (GMT)
This way we can make really good use of these bookclubs
Petar Vukmirovic
2020-04-04 17:12:52 (GMT)
SMT paper is very good for this purpose since we have some people (notably Haniel) experts in SMT and some people (notably me) cluless about it
Haniel Barbosa
2020-04-04 22:38:26 (GMT)
We should do some about intense implementation techniques for superposition provers to go the other way around :)
Sophie
2020-04-06 6:28:26 (GMT)
My comment about short papers was also supposed to be a joke! ^^' At least, now I know I am not the only one with a cryptic sense of humor here.
I am perfectly fine with the SMT paper (although I believe I have read it already a few years ago, it won't hurt to take another look and discuss about it).
Jasmin Blanchette
2020-04-06 7:55:41 (GMT)
The SMT paper is a bit long, maybe we can find a shorter one? ^^
Sophie
2020-04-06 7:58:57 (GMT)
Are you serious, or is this your attempt at cryptic humor? Or even better: is it both?
Jasmin Blanchette
2020-04-06 8:0:10 (GMT)
It's my attempt. Let's read the SMT paper. :)
Sophie
2020-04-06 8:40:49 (GMT)
Sure!
Mathias Fleury
2020-04-07 15:23:56 (GMT)
Can I join the bookclub or are there already too many people?
Sophie
2020-04-07 15:26:4 (GMT)
You are welcome! As far as I know, there is no member's list ^^
Jasmin Blanchette
2020-04-07 15:26:36 (GMT)
We were 6 last time, which worked fine. I'm guessing we'll lose people faster than we'll gain them. ;)
Jasmin Blanchette
2020-04-07 15:26:45 (GMT)
Esp. that the upcoming paper (NOT) is quite long.
Jasmin Blanchette
2020-04-07 15:26:51 (GMT)
But you've read it already, right?
Jasmin Blanchette
2020-04-07 15:27:9 (GMT)
It would be great to have you around -- in general and for that paper in particular.
Mathias Fleury
2020-04-07 15:35:37 (GMT)
I have read it, but I learned a lot about SAT since, so rereading is a good idea
Jasmin Blanchette
2020-04-08 15:41:25 (GMT)
Another SAT paper, recently accepted at IJCAR, which Marijn Heule wants to advertize. It's full of nice pictures:
https://arxiv.org/pdf/1910.03740.pdf
Haniel Barbosa
2020-04-08 17:16:5 (GMT)
A SAT paper I've been wanting to read for a while is Backing Backtracking, which goes about the advantages of chronological backtracking
http://fmv.jku.at/papers/MoehleBiere-SAT19.pdf
Simon Cruanes
2020-04-08 17:17:11 (GMT)
given the authors it might be non trivial to read, but I'm interested.
Should we use the "reaction" emojis to vote? like up/down thumb?
Haniel Barbosa
2020-04-08 17:21:7 (GMT)
sounds good
Simon Cruanes
2020-04-08 17:22:12 (GMT)
There's :upvote: and :downvote: actually (:upvote: and :downvote:!)
Jasmin Blanchette
2020-04-08 17:31:34 (GMT)
And :octopus: of course.
Mathias Fleury
2020-04-08 17:34:0 (GMT)
I fear however that the paper is a bit far from the Matryoshka audience. I believe you need a good understanding of CDCL and watched literals to get the details.
Sophie
2020-04-09 12:17:35 (GMT)
Here are a few more suggestions:
- AVATAR: The Architecture for First-Order Theorem Provers, by Voronkov
- Labelled Clauses, by Lev-Ami, Weidenbach, Reps and Sagiv (somehow related to the Avatar architecture, possibly subsuming it, I have no idea whether it is suitable for the bookclub but Christoph mentioned it this morning and now I am curious)
- Satallax: An Automatic Higher-Order Prover, by Brown (the only publication I could find on Satallax, if there is a more recent one that gives a clear picture of the general current approach, I would also be interested)
- The Higher-Order Prover Leo-III, by Steen and Benzmüller
Jasmin Blanchette
2020-04-09 12:38:10 (GMT)
They're all in the same message. We cannot :upvote: or :downvote: them individually. :S
Jasmin Blanchette
2020-04-09 12:51:28 (GMT)
- AVATAR: The Architecture for First-Order Theorem Provers, by Voronkov
Jasmin Blanchette
2020-04-09 12:51:34 (GMT)
- Labelled Clauses, by Lev-Ami, Weidenbach, Reps and Sagiv (somehow related to the Avatar architecture, possibly subsuming it, I have no idea whether it is suitable for the bookclub but Christoph mentioned it this morning and now I am curious)
Jasmin Blanchette
2020-04-09 12:51:43 (GMT)
- Satallax: An Automatic Higher-Order Prover, by Brown (the only publication I could find on Satallax, if there is a more recent one that gives a clear picture of the general current approach, I would also be interested)
Jasmin Blanchette
2020-04-09 12:51:49 (GMT)
- The Higher-Order Prover Leo-III, by Steen and Benzmüller
Jasmin Blanchette
2020-04-09 12:52:12 (GMT)
Now we can vote (except me). :)
Jasmin Blanchette
2020-04-09 12:52:34 (GMT)
Petar, could you vote for Labelled Clauses on my behalf? Thanks.
Jasmin Blanchette
2020-04-09 12:54:51 (GMT)
Satallax hasn't evolved that much since 2012. The main change was the integration of FO ATPs (like Leo-II(I)) and more strategy/option tuning with machine learning.
Jasmin Blanchette
2020-04-09 12:55:2 (GMT)
I personally would prefer
- Julian Backes, Chad E. Brown: Analytic Tableaux for Higher-Order Logic with Choice
Jasmin Blanchette
2020-04-09 12:55:22 (GMT)
Which is one year older and perhaps too long for most people's taste, but there's also the IJCAR 2010 version.
Sophie
2020-04-09 13:23:52 (GMT)
I am not sure we should vote in this thread and right now. I suggest we wait until after the next bookclub metting and open a more specific thread (paper proposal 30/04/20, or something similar) where we gather all the current proposals and vote on them. Otherwise it will get messy from session to session.
Sophie
2020-04-09 13:24:41 (GMT)
and we risk burying nice but old proposals under more recent ones.
Sophie
2020-04-09 13:25:53 (GMT)
We could also do this live at the end of the meeting... I guess we have to experiment a bit to see what works.
Simon Cruanes
2020-04-09 13:27:11 (GMT)
Sophie said:
We could also do this live at the end of the meeting... I guess we have to experiment a bit to see what works.
I agree, we're still fumbling around.
The most important is that we do have the bookclub meetings, the rest will move into place progressively.
Jasmin Blanchette
2020-04-09 17:34:49 (GMT)
You guys are using :octopus: all wrong! ;)
https://leanprover-community.github.io/archive/113488general/56578octopusemoji.html
Simon Cruanes
2020-04-09 17:37:39 (GMT)
to me it means "conquer the world"
Simon Cruanes
2020-04-09 17:38:11 (GMT)
Michael Färber
2020-04-21 17:10:37 (GMT)
Jasmin Blanchette said:
- Satallax: An Automatic Higher-Order Prover, by Brown (the only publication I could find on Satallax, if there is a more recent one that gives a clear picture of the general current approach, I would also be interested)
A more recent and complete publication: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems, by Chad Brown
This paper is more theoretical than Brown's "Satallax" paper and a bit more practical than Backes/Brown's "Tableaux" paper.
Simon Cruanes
2020-04-21 17:34:12 (GMT)
That sounds interesting.