2020-06-16 8:4:9 (GMT)
Dear colleagues,
Last week we have received an announcement that InriaForge will be shut down at the end of December 2020. In particular, that means that our matryoshka git repository will stop working.
We see two alternative platforms where the repository could move:
If you are a user of the matryoshka repo, please vote below for the option you prefer.
Once we have agreed on where to move, we’ll let you know when exactly we will switch.
While moving, we plan to shrink down the size of the repository by splitting off the “www” directory, which contains a lot of large PDFs in different versions, into a separate repo. We will keep the entire history of the matryoshka repo, but delete the history of the “www” directory. We will also move our repo for large data files “matryoshka_data”, but delete its history. If you have other suggestions, please let us know.
Cheers,
Alex & Jasmin
2020-06-16 8:6:24 (GMT)
2020-06-16 8:6:59 (GMT)
2020-06-16 10:37:32 (GMT)
Yes :slight_smile:
2020-06-16 10:37:35 (GMT)
----------------------- REVIEW 2 ---------------------
SUBMISSION: 2
TITLE: Boolean Reasoning in a Higher-Order Superposition Prover
AUTHORS: Petar Vukmirović and Visa Nummelin
----------- Overall evaluation -----------
SCORE: 1 (weak accept)
----- TEXT:
This paper studies several rules for Boolean reasoning in a higher-order superposition
theorem prover. In particular, the theorem prover Zipperposition is extended to support
these rules. In extensive experiments, the impact of the rules is evaluated. A comparison
to state-of-the-art tools indicate that the approach is competitive.
Overall the paper is well written (some minors are listed below), well motivated and
easy to follow. The contribution of this paper is more on the practical side and the
authors share a lot of experiences they made when implementing the rules for
Boolean reasoning. Hence, I think it would fit very well for PAAR and I recommend
acceptance.
Some typos and minors:
Page 1: superposition, calculus - remove comma
Page 1: This approach assumes a problem with formulas occurring as arguments
of symbols is translated to rst-order logic. - please check this sentence
Page 1: Bentkamp et al. - reference is missing
Page 4: THE version of Zipperposition preceding our modifications distinguished
Page 4: with one key distinction we do not perform - : is missing
Page 4: the double lines in the rules are not entirely clar (description of casesimp)
Page 5: if A clause has
Page 10: THE TPTP library
Page 10: instances of THE CASC theorem proving competition
Finally, it would be interesting to see the connection to QBF as, for example discussed
in [17]. Also the following paper seems to be related:
Martina Seidl, Florian Lonsing, Armin Biere:
qbf2epr: A Tool for Generating EPR Formulas from QBF. PAAR@IJCAR 2012: 139-148
----------------------- REVIEW 3 ---------------------
SUBMISSION: 2
TITLE: Boolean Reasoning in a Higher-Order Superposition Prover
AUTHORS: Petar Vukmirović and Visa Nummelin
----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
The paper deals with the topic of Boolean reasoning in the context of higher-order theorem proving.
This is the next stage in a program to develop a higher-order theorem proving technology
by extending the superposition calculus for first-order logic to first deal with lambdas
in the Boolean-free setting [5]. The paper partially compares to the work of Kotelnikov et al [18,19]
where the Boolean aspect is studied as an extension of first-order logic. The paper mostly
consist of a list of dedicated inference rules accompanied by explanations and examples.
The authors take a pragmatic approach, being primarily interested in practical efficiency,
leaving the completeness considerations behind as (currently) secondary. The rules have been
implemented in the Zipperposition prover and the paper ends with an experimental evaluation
on the higher-order part of the TPTP library.
The paper is well-written (see just a few comments below) and contains material the should be
of great interest to the developers of modern higher-order theorem provers. It's a good fit for PAAR.
I recommend accept.
*) Page 2 (2 Background) "A type $\tau,\upsilon$ is either a type variable ..." - why "$\tau,\upsilon$"?
*) Page 4 (3.2 Core Rules) "the result of clausification of the formula $\forall x. L1 \lor \ldots \lor Ln" - you lost the connection to C. Probably $C = L1 \lor \ldots \lor Ln$ ?
*) Page 5 (3.3 Higher-Order Considerations) "is the imitation of constant f : ... for variable z : ..." - The becomes a bit hard to follow. Are you sure it is "the" imitation and just an imitation? Also where does "z" come from here? A bit more detail here would be nice!
*) Page 6 "Andrews formulates this axiom as ..., where \epsilon ..." - \epsilon should return \alpha, shouldn't it?
*) This section 3.3 is needlessly packed. Separating the rules into paragraphs / subsubsections could help readablility
2020-06-16 10:39:50 (GMT)
aaaand this one
2020-06-16 10:39:52 (GMT)
----------------------- REVIEW 1 ---------------------
SUBMISSION: 2
TITLE: Boolean Reasoning in a Higher-Order Superposition Prover
AUTHORS: Petar Vukmirović and Visa Nummelin
----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
The submission "Boolean Reasoning in a Higher-Order Superposition Prover" describes the extension of a superposition-based calculus for so-called Boolean-free higher-order logic with (interpreted) Booleans (or Boolean reasoning). The work is situated in the context of the Zipperposition prover.
After motivating their work, and briefly highlighting the different problem dimensions, the authors present (partly practically motivated) calculus rules that capture Boolean reasoning within the superposition-based setting of Zipperposition. This includes the discussion of inference rules that originate from earlier work in a different context (e.g. first-order reasoning) and their adaption to the higher-order case. Specifically for higher-order reasoning, inference rules for handling predicate variables, extensionality principles and defined equalities are discussed. Subsequently, related approaches are discussed. Afterwards, the introduced approaches are demonstrated using examples, including the classical subjective cantor theorem. Finally, an implementation of the presented extension to Zipperposition is evaluated on the monomorphic THF-fragment of the TPTP problem library.
The overall presentation quality is convincing throughout the whole submission; the calculus extension is well-motivated and presented in an understandable and precise manner. In particular, the extension is tightly put in context with earlier work and related approaches -- to my mind, this submission not only succeeds in discussing the extensions of Zipperposition in a tangible manner, but also summarizes the relevant related work in high quality. The evaluation results suggest that the presented extensions are indeed valuable in practice.
The topic is hence clearly in scope of the PAAR workshop and highly interesting for system development in higher-order automated theorem proving. Moreover, I really enjoyed reading it.
I'm strongly in favor of accepting it.
2020-06-16 10:51:54 (GMT)
wrong thread but congratulation!
2020-06-16 11:3:28 (GMT)
Sorry :slight_smile:
2020-06-16 11:3:38 (GMT)
This was meant for Jasmin :slight_smile:
2020-06-16 13:36:37 (GMT)
Are you planning to have a separate repo for the www directory? or use something like git-lfs?
Shrinking the repo would be good in any case, I think the magic command is filter-branch (magic as in, it's also a weird incantation).
2020-06-16 13:45:33 (GMT)
We plan to split off the www directory into another repo because many people won't need it at all and it is quite big. I found a tool called git-filter-repo which I will use to do it. It's a bit easier to use than git filter-branch.
For Git LFS, everybody would have to install the Git LFS client, right? I don't think that would be a good idea.
2020-06-16 13:47:10 (GMT)
Our PDFs are like 300k. They're "medium" files but not large like video etc. A repository used by me and maybe Pascal will do the trick. We can purge it every 5 years if we want. :)
2020-06-16 13:47:48 (GMT)
The "problem" is just that we have sometimes 20 copies of the same paper on top of each other in the history.
2020-06-16 13:48:14 (GMT)
Deduplication is useful indeed. I think it's a simple solution that would work :+1: