SUBMISSION: 624
TITLE: Recurrence-Driven Summations in Automated Deduction


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

----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
Summary:

 In this paper, the authors present an algorithmic approach to
 deduce proofs of finite summations. They use the theory of
 holonomic sequences, which is a well-established theory. The
 advantage of their approach is that their algorithm can be
 directly embedded into higher-order theorem provers. Their approach
 automates the induction step with the base cases being handled
 by the theorem prover.

 Their procedure consists of the following three steps:
 (a) Initialization, (b) Selection, and (c) Induction.

 Evaluation:
 The paper is extremely well-written in most aspects. They have
 described in adequate detail all the terminology used in the
 paper. The work itself is both practical and extremely deep.
 Their inferential steps are detailed and easy to follow. The
 work itself is applicable to several domains. An extensive
 study of the literature has been performed. Several examples
 have been provided to illustrate the concepts.

  Without a doubt, this paper must be included in the proceedings.



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

----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
Summary

A method to prove equations including a rich set of operators over
commutative monoids/rings (addition, multiplication, multiplication
with integers, summation) is presented. The method is inspired by the
theory of holonomic sequences, and here adapted to the setting of
higher-order ATP, and extended to handle uninterpreted functions and
infinite sets of base cases. The approach has three main steps: (1)
recurrence equations are derived for the basic terms occurring in the
equation to be proving, and in assumptions that can be
used. Recurrence equations contain operators for index shifts and for
multiplying terms with indexes. (2) The selected recurrences are
propagated to derive recurrences for compound terms. Propagation
happens, primarily, through a non-commutative variant of Buchberger's
algorithm for computing Gröbner bases. (3) Induction is performed on
non-trivial recurrences after propagation.

Comments

Content-wise, this is a very strong submission, presenting various
ideas how the gap between computer algebra methods (holonomic
sequences, Gröbner bases, etc.) and ATP can be bridged. Although no
systematic evaluation is carried out, the paper discusses several
challenging examples that the procedure can prove automatically, and
which are far beyond the state of the art in ATP. (It is not clear
which of the examples could be solved by existing computer algebra
systems.) As there is currently very little available in terms of
support for summation and recurrences in automated theorem provers,
the work can be considered groundbreaking. The paper should be
extremely interesting for an ATP audience working on the integration
of theory solvers into first/higher-order reasoners.

In the current form, the paper is not very easy to read, however,
there is simply too much material and too little space. As a result,
the paper can only be understood with a lot of prior knowledge (e.g.,
about Buchberger's algorithm and recurrence equations); the paper is
very incomplete in terms of the more basic definitions, and not at all
self-contained. The paper is also in many places rather prosaic and
not very precisely written (also see below); some parts read more like
an experience report than a rigorous research paper. Somewhat
ironically, part of the issue is the presentation style combining
higher-order logic semantics with algebra. The work would probably be
more accessible by separating the purely algebraic perspective
(deriving recurrences of sequence terms, and in which way the
presented method extends the existing approaches) from the integration
into ATP. Altogether, it is not clear how the presentation problem can
be addressed.

The work is open-ended, and more like a collection of ideas, thoughts
on strategies and heuristics, than a single procedure. A negative
effect of this setting is that very little is said (or can be said?)
about completeness of the method for particular forms of equations.

Page 3: "We accept conditional proofs of this goal." unclear

Page 3: "and some extra conditions E" vague

Page 5: since Def 3 is essential for understanding the rest of the
paper, it should be made more precise, and maybe some examples be
provided



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

----------- Overall evaluation -----------
SCORE: 1 (weak accept)
----- TEXT:
Overview
======
The authors present a procedure that automatically proves
equations about finite summations. They mention that the method 
proposed is inspired by [19], a paper in which multivariate 
holonomic sequences are studied. Indeed, two steps of the 
procedure, Propagation and Inductions are supposed to apply 
holonomic-style techniques almost as a black box.

The intention of the authors is to implement the procedure within 
a higher-order automatic theorem prover - it is mentioned that 
an implementation in the Zipperposition prover is under way.

Evaluation
=======
The paper is in the scope of FroCoS. 
I think that the results are interesting, but I found the paper 
difficult to read. 
It would be good if the authors could describe clearer  the 
syntax of the terms/atoms they consider and if they could include 
more examples at the beginning of the paper to support the intuition
and explain the notation (otherwise e.g. the example on page 3 line 11
from the bottom is difficult to parse). 

Since the results are non-trivial and interesting I suggest acceptance.

However, I think that the presentation should be improved to make 
the paper more readable. 


Detailed comments
=============

page 2, Section 2 
Perhaps the notion of terms or subterms you use could be defined 
before giving the summation rule. In particular, what are the 
subterms of a term of the form k \sum_{i = 1}^n t' + t'' ?

page 3, Section 3
I am not sure that I understand the explanation in the paragraph 
``Term generalization'': The description of the heuristic you 
define seems to be self-referential. Is this right? 

page 5: Please explain, for instance by giving an example, why 
you need polynomials over non-commutative rings for modeling 
the problems you consider.
