----------------------- REVIEW 1 ---------------------
SUBMISSION: 32
TITLE: Recurrence-Driven Summations in Automated Deduction
AUTHORS: Visa Nummelin, Jasmin Blanchette and Sander R. Dahmen

----------- Overall evaluation -----------
SCORE: -2 (reject)
----- TEXT:
1. The paper is not readable in a way that allows understanding the scientific contributions.
It is poorly organized and main claims should be made in context of propositions or theorems.

2. The approach should be qualified relative to prior work on solving symbolic summations based on Karr's algorithm for closed form summations, http://ftp.gwdg.de/pub/misc/EMIS/journals/SLC/wpapers/s56schneider.pdf [Carsten Schneider, 2007]. 

3. The work is in a preliminary form with ideas on how to decompose disequalities with summations into inferences.


----------------------- REVIEW 2 ---------------------
SUBMISSION: 32
TITLE: Recurrence-Driven Summations in Automated Deduction
AUTHORS: Visa Nummelin, Jasmin Blanchette and Sander R. Dahmen

----------- Overall evaluation -----------
SCORE: 1 (weak accept)
----- TEXT:
The paper proposes a procedure to automatically prove equalities involving finite summations. The procedure works as an additional inference rule in the framework of superposition calculus within a higher-order theorem prover. It views the problem axioms as recurrences and derives new recurrences from existing ones, using techniques from holonomic sequences. In case of success, the derived recurrences serve as the inductive step of  an inductive proof, while the basic cases can be checked automatically by the prover. 

Strengths:
This paper is interesting because it presents new ideas to address the problem of proving equalities with finite summations. The techniques are built on solid theories from recurrence sequences and non-commutative polynomial algebra. Examples in the paper show that the method is promising and is able to handle some complex instances. For these reasons, I would like this paper to be accepted.

Weakness:
1. The paper does not have a Preliminaires section and assumes that readers are very familiar with automated deduction and recurrence sequences. No formal definitions are provided except in Sec 4. 

2. Sec 4 is difficult to read. As far as I understand, it encodes recurrence relations into operator polynomials, and uses elimination theory to compute new recurrences. The technical details are hard to check, but illustrative examples seem correct.

3. The procedure has not been implemented yet.


----------------------- REVIEW 3 ---------------------
SUBMISSION: 32
TITLE: Recurrence-Driven Summations in Automated Deduction
AUTHORS: Visa Nummelin, Jasmin Blanchette and Sander R. Dahmen

----------- Overall evaluation -----------
SCORE: -2 (reject)
----- TEXT:
Short Summary:

The paper introduces a method to integrate solving equivalences of recursively defined sequences in a saturation algorithm.

Very abstractly the idea is to perform an inductive proof on a set of recurrences in order to eliminate a literal t != 0 of some clause.

The process for doing this is split into multiple parts. 
In a first step (Section 3: Initialization) recurrences to use for the induction step are determined.

The next step (Section 4: Propagation) is the biggest part of the paper, aiming at proving the induction step.
The main idea of technique is to interpret homogenious linear recurrences as polynomials with so-called operators that transform sequences as indeterminantes.

An example is the recurrence  
```
    f(n1 + 2) = f(n1) + f(n1 + 1)
<-> f(n1 + 2) - f(n1 + 1) - f(n1) = 0 
```
which is associate is interpred as the polynomial  
```
S1^2  - S1 - 1
```
where the operator S1 which maps `f(n1) -> f(n1 + 1)`.

Procedures, called "Propagations", are introduced to prove equivalences of operator polynomials of complex sequence terms (e.g. `f(n + 7, m) + m g(n + 1, m)`), from recurrences of atomic sequence terms (e.g. `f(n,m)`).
The procedures use Gröbner basis computations in order to eliminate indeterminantes from polynomials, and thereby turn sets of polynomial equations into equivalent sets of equations "simpler" polynomials.

If the induction step is successfully proved, a set of induction base cases is selected and passed back to the saturation algorithm.


High Level Review:

The paper uses some very interesting ideas, which I find very inspiring, and of big potential for the use in automated reasoning in general and saturation algorithms i particular. 
Nevertheless the description of the method is very informal, and often imprecise, which leaves many questions about how to implement it open, and leaves me unable to verify whether the details of the method work out.
Further there are neither formal results on what is provable with this method, nor is there an experimental evaluation.

The paper lacks a Preliminaries section, which i see very necessary as the paper assumes a lot of mathematical knowledge that cannot be assumed to be known.
Further notation conventions, and frequently used definitions should be gathered there.
There is a lot of use of quite heavy mathematical language using many terms that are neither defined in the paper, nor is there a reference to where these terms are being defined, which makes the paper non-self-contained.
At the same time concepts and ideas introduced are introduced in a very informal language, which in combination with undefined terms, and mathematical concepts, leaves a lot of ambiguities, and makes definitions very hard to understand.

The paper mentions that the work is strongly inspired by "Zeilberger, D.: A holonomic systems approach to special functions identities".
Obviously there are a lot of concepts introduced/defined by Zeilberger that are being used in this paper. 
Nevertheless it is not made clear to me which ideas from there are just slightly adjusted, and which ideas are really new ideas introduced in this paper, which also lets me unsure about the novelty of the techniques introduced in the paper in general.

The paper lists a lot of examples for the techniques introduced. 
In my eyes the examples should help to illustrate what the techniques introduced do in a simple easily understandable way.
Many of the examples given in the paper contain a lot of unnecessary information that have to be explained. 
This unnecessary information and the explanations thereof bloats the examples and makes it unclear which parts of the example are actually part of the procedures they are meant to illustrate. 
Therefore the examples do not help me understand the theory.


Low-level comments:

- Page 1: "These recurrences have almost the same form as multivariate holonomic sequences ..."
  The exact commonalities and differences are not described anywhere in the paper, which would be relevant in order to assess the originality of the content in the paper.

- Page 2: "procedure scales up to more sophisticated problems"
  There is no evidence for this in the paper, as there is no experimental or formal evaluation of the procedure.

- Page 2: "the procedure performs an induction on the generalized subterms ⃗s of t and u (Sect. 3)—these ⃗s may not be subterms of each other"
  This means that the method cannot generalize the term `g(a, f(a))` to `g(x,y)`, but only to `g(x,f(x))`. 
  Is this really the case, or is there a mistake in the definition? 
  In my eyes   ⃗s should be subterm-paths where none of them is the suffix of another one.

- Page 4: 
  The definition of which subterms are being generalized is not precise enough.
  Why is in the example none of the terms
    f(g(-1))
    g(a + 1)
    f(1, g(a + 1))
  generalized?
  Are only some sort of minimal subterms being generalized? 
  What about terms like g(a,b)? Do you generalize it to g(x, b), to g(a, x), or to g(x,y), or try all of the generalizations?

  The collection of bounds is described only very vaguely and informally, which makes it very hard to judge what exactly is going on:
  It is not clear which sort of literals are allowed be used as bounds.
  Intuitively I would expect literals s' >= t where s' is a generalization of s, and s'.
  But do you only allow for numerals t, or for arbitrary complex terms?
  But what about literals k s' >= t , for some numeral k?
  And what about the shapes of the clauses C1, ... Cl?  Do you only consider unit literals?
  Further I do not understand what the sentence "The free variables of ¬C are interpreted as constants, and they can also occur in ⃗s" is supposed to mean.


- Page 4 & 5:
  "Semantically, the recurrences we look for are multivariate heterogeneous linear finite-fixed-step equations with polynomial coefficients."
  It is not clear how to me to represent a non-homogenious equation as an operator polynomial.
  How would for example the recurrence `f(x + 1) = f(x) + 3` be represented? 
  In my eyes one would need an additional constant operator indeterminant `C_x` such that `(C_x f) n = x`.

- Page 5:
  "We could forbid them and work only with unit equations such as f ⃗a ⃗n = t. We could collect them and put them in the D component of the Summation rule’s conclusion. Or we could attempt to prove them when the initial recurrences are selected. In our ongoing implementation, we chose the first option."
  If I am not misunderstanding what is being said here this means that most of the examples that are being listed later are to be excluded, as most of the recurrences (e.g. the binomial coefficients) are usually only defined for natural numbers, hence all their recurrences would be of the form  `~(n >= 0) \/ f ⃗a ⃗n = t`.


- Page 5:
  "Sequences defined by recurrences with polynomial coefficients and finitely many base case values are holonomic."
  Is this a definition, or a necessary condition? 

  "They are closed under [..], which makes their equality decidable [21]."
  How does the decidability result in [21] differ from the procedures introduced in this paper?

- Page 7:
  "Due to the (non)commutation relations, polynomials can be written ..."
  It took me quite a while to figure out that the term "(non)commutation relations" (that is used thought the paper) refers to the formulas (1). 
  This should be made clear by an explicit definition of the term (non)commutation relations, as it is being used throughout the paper.

- Page 8:
  "However, starting from encoded polynomials P⃗ • F⃗ , the standard Gröbner basis computation derives only polynomials of the same form R⃗ • F⃗ where no Rj contains any F⃗ component."
  I am not able to verify this claim without a pseudo-code for the Gröbner-basis computation algorithm. 
  I think there should be at least an appendix, or a reference to some resource that lets one verify this claim, as this is a crucial piece for the whole section to work out, and not at all obvious to see from what is explained in the paper. 

  "... by carrying excess terms along"
  It is not clear to me which terms are excess terms in the examples, and I was not able to understand the definition of excess terms given later.
  It would help a lot to understand the paper if they would be made explicit in the examples.

  Example 9. 
  This example is meant to illustrate propagation to addition. 
  The example as well contains the summation function, which is the replaced by an uninterpreted symbol that is then actually processed by the algorithm.
  The example would be a lot more understandable and illustrated propagation to addition just as well if using summation would be skipped and the uninterpreted symbol would be used straight away, as the step of introducing the uninterpreted symbol does not have to do anything with the procedure that is meant to be illustrated.

- Page 10:

  Example 11.
  This example again contains a lot of information that makes it hard to understand what is actually meant to be shown:
  What is the actual input to the procedure? 
  Why is the definition `binnom(n1,n2) = n1!/((n1 - n2)!n2!)`, when it's not being used in the rest of the example, but instead pascal's triangle recurrences are used?
  Further there is the recurrence `binom(n1,n2) = (n1/n2) * binom(n1-1, n2 - 1)` mentioned in the example and claimed that it is equivalent to the operator polynomial `(M2 + 1)S1S2 − M1 − 1`. 
  This equivalence is everything but trivial to me when it comes to automated reasoning as it is not mentioned in the paper how division should be translated into operator polynomials.

  It is mentioned in the example that "these" recurrences are being propagated to the substitution sigma. 
  I do not know which of the many recurrences mentioned before are meant by "these".

  The example should in my eyes just start with the exact terms propagation to substitution is being applied to and end with the result of the propagation. 
  All additional information makes the example quite confusing to me.


- Page 11:
  "[...] Em’s are part of excess terms built by applying operator polynomials and the substitution {n1 -> m} to f".
  Which operator polynomials do you mean here?

- Page 12:
  "... each sequence term with uninterpreted head."
  What does the term "uninterpreted head" mean?

  Definition 15.
  I did not manage to understand this definition:
  Sequence terms are never explicitly defined in the paper, but on page 5 their intuition is given.
  According to that intuition one cannot eliminate indeterminants from them, as they do not contain any. 
  So what I assume what is meant was "eliminating indeterminants from the defining operator polynomial of the sequence term".
  By looking at the rules I cannot see how the indeterminants Si are to be "erased".

  Also due to the fact that sequence terms are never formally introduced, I am not sure how to interpret the rewrite rule `{n -> bn + c} t ==> {n -> bn} t`. 
  Is a substitution formal object, i.e. a part of the syntax/bit of data (A)? Or is the substitution meant to be notation for the semantic operation of substituting subterms (B)?
  For example do you mean this rule to rewrite
  B) f(3n + 7) ==> f(3n) 
  or 
  A) {n -> 3n + 7}f(n) ==> {n -> 3n}f(n)
  If it is meant to be the (B), does this not cover the rule `sum_j^{c n + d} t ==> sum_j^{c n} t` without the need for explicitly introducing it?
  If it is meant to be the (A), it should be made explicit that these syntactic substitution object are different from the semantic notion of substitution introduced on Page 3.

  As i was not able to understand the definition of the spine and there were no example for spines given, i was not really able to understand the rest of the section in detail.
  i.e. It is not possible to verify how spines change when propagation is applied to a term, it is not clear which symbols spines will contain and therefore not possible to see whether the ordering is well-defined for them, and it is not possible to understand the definition of an excess term.

- Page 13:
  "[...] as invertibility of the multiplication maps associated with leading monomials’ coefficients."
  What are "multiplication maps"? 

- Page 13&14:

  Section 5: Induction

  It is not clear why the described base value sets should suffice in the case described by in the second paragraph. 
  The sentence that should explain this 
  "[...], suffice for the base cases, as a union of stacked hyperplanes that is infinite unless k ≤ 1, but corresponds to only sum_{j=1}^k b_j one variable substitutions [...]".
  is not understandable for me.

  The explanation why using the intersection of all the induction bases in the next paragraph is also not clear to me.

  Further, how are recurrences handled that have a leading polynomial that contains a multiplier?


- Page 14.

  Section 6: Examples
  There are claims of a few formulas to be solvable by the procedures described in the paper.
  As there are neither formal nor experimental results, I am not convinced that this claim really holds.

  In the example that is explained in details, the formula that the procedure is applied to in details contains division again.
  As division is not handled by the procedures described in this paper "mathematical intuition" (i.e. introducing the inverse of the factorial function, and finding a recursive definition for it) is required to proof the example.
  This does not help to support confidence in the method being suitable for a fully automatic theorem prover.


------------------------------------------------------
