2020-03-26 13:22:59 (GMT)
2020-03-26 13:26:51 (GMT)
I donno. One week from now?
2020-03-26 13:26:54 (GMT)
It's a short paper.
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.)
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.
2020-03-26 14:29:55 (GMT)
I thought you might be interested indeed, @Sophie :slight_smile:
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.
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
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.
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.
2020-03-26 20:58:13 (GMT)
"Layered Clause Selection for Theory Reasoning" @Petar Vukmirovic I think it'd interest us both :)
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 :)
2020-04-02 15:59:17 (GMT)
Shall we try to get our hands on "Layed Clause Selection"?
2020-04-02 15:59:45 (GMT)
Oh it's on arXiv, nice.
2020-04-02 16:0:0 (GMT)
Are we only reading short papers?
2020-04-02 17:8:24 (GMT)
I don't know, but it sounds like a good idea, it takes less time
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
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. ;)
2020-04-02 17:27:20 (GMT)
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?
2020-04-02 17:36:9 (GMT)
Donno what you've read or not.
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
2020-04-02 17:37:28 (GMT)
About SMT.
2020-04-02 18:24:36 (GMT)
Would love to read that.
2020-04-02 18:41:26 (GMT)
too bad it doesn't qualify as a short paper... ^^
2020-04-02 19:33:18 (GMT)
I never read it either
2020-04-02 19:42:43 (GMT)
Shame on you. :)
2020-04-02 19:43:11 (GMT)
(I realize that's the kettle calling the pot black.)
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é
2020-04-03 7:49:36 (GMT)
Am I in the wrong Zulip topic? ;)
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.
2020-04-03 9:29:31 (GMT)
By abstracts you mean short papers and tool descriptions?
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.
2020-04-03 9:30:0 (GMT)
Or individually skip some.
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.
2020-04-03 9:30:38 (GMT)
I'm afraid restricting our scope to short papers would leave out 90% of interesting papers.
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. ;)
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
2020-04-03 17:35:13 (GMT)
Right. ;)
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?
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.
2020-04-04 12:10:51 (GMT)
Oh, you meant "abstracts" not "extended abstracts". I see. ;) (British humour...)
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?
2020-04-04 15:48:59 (GMT)
I'm fine with long papers as well, btw.
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
2020-04-04 17:11:50 (GMT)
This way we can make really good use of these bookclubs
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
2020-04-04 22:38:26 (GMT)
We should do some about intense implementation techniques for superposition provers to go the other way around :)
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).
2020-04-06 7:55:41 (GMT)
The SMT paper is a bit long, maybe we can find a shorter one? ^^
2020-04-06 7:58:57 (GMT)
Are you serious, or is this your attempt at cryptic humor? Or even better: is it both?
2020-04-06 8:0:10 (GMT)
It's my attempt. Let's read the SMT paper. :)
2020-04-06 8:40:49 (GMT)
Sure!
2020-04-07 15:23:56 (GMT)
Can I join the bookclub or are there already too many people?
2020-04-07 15:26:4 (GMT)
You are welcome! As far as I know, there is no member's list ^^
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. ;)
2020-04-07 15:26:45 (GMT)
Esp. that the upcoming paper (NOT) is quite long.
2020-04-07 15:26:51 (GMT)
But you've read it already, right?
2020-04-07 15:27:9 (GMT)
It would be great to have you around -- in general and for that paper in particular.
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
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
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
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?
2020-04-08 17:21:7 (GMT)
sounds good
2020-04-08 17:22:12 (GMT)
There's :upvote: and :downvote: actually (:upvote: and :downvote:!)
2020-04-08 17:31:34 (GMT)
And :octopus: of course.
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.
2020-04-09 12:17:35 (GMT)
Here are a few more suggestions:
2020-04-09 12:38:10 (GMT)
They're all in the same message. We cannot :upvote: or :downvote: them individually. :S
2020-04-09 12:51:28 (GMT)
2020-04-09 12:51:34 (GMT)
2020-04-09 12:51:43 (GMT)
2020-04-09 12:51:49 (GMT)
2020-04-09 12:52:12 (GMT)
Now we can vote (except me). :)
2020-04-09 12:52:34 (GMT)
Petar, could you vote for Labelled Clauses on my behalf? Thanks.
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.
2020-04-09 12:55:2 (GMT)
I personally would prefer
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.
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.
2020-04-09 13:24:41 (GMT)
and we risk burying nice but old proposals under more recent ones.
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.
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.
2020-04-09 17:34:49 (GMT)
You guys are using :octopus: all wrong! ;)
https://leanprover-community.github.io/archive/113488general/56578octopusemoji.html
2020-04-09 17:37:39 (GMT)
to me it means "conquer the world"
2020-04-09 17:38:11 (GMT)
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.
2020-04-21 17:34:12 (GMT)
That sounds interesting.