Paper #: 61
Title: Disproving False Conjectures
-------------------- review 770 --------------------
Overall evaluation: 2 (accept)
Referee's confidence: 3 (high)
This paper presents a technique for disproving a class of formulas in
first-order logic (FOL). These formulas arise in automatic proof in
various contexts such as verification of software specifications,
which is the context considered by the authors. An example of where
they arise is in a proof that requires induction, but is first
attempted without induction. In the approach given, a FOL formula is
translated to a fragment of second-order monadic logic which is
decidable. The translation is defined in such a way that if the
conjecture is proven false in monadic logic, then it is also false in
FOL. A proof of this soundness result is outlined. Knowing that a
conjecture is false can help make proof search more efficient by
cutting off the search for proofs of such conjectures.
This work is clearly motivated by practical applications in software
verification, and is an important first step in a bigger project, much
of which is outlined as future work in the conclusion.
The paper could be better motivated in the introduction. I suggest
moving some of the information at the beginning of section 3 and also
the motivating application using Maya to section 1.
On page 1, "the fragment of hereditary Harrop formulas" is ambiguous.
There needs to be a citation or an explanation of which fragment.
In figure 1, most notation is explained, but the empty list [] is
not. Why are lists used instead of sets as is usually used in such a
definition?
In example 1, an intuitive explanation of "left" and "right" is
needed. Also, "subtree" is not mentioned, but is used later.
The explanation just after definition 5 uses the notation
"x\in VC(P(t_1,ldots,t_n))" but this notation is not used above in the
9th case (or in any other case). I'm not sure what is meant.
I assume Lemma 1 can be made more specific by replacing "second-order
monadic" with "first-order monadic".
Typos and grammar errors:
-page 1, "He advocated to use the" should be "He advocated using".
-page 8, "The answer of this questions" should be "The answer to this
question" or "The answer to these questions".
-page 10, "trail and error" should be "trial and error".
-page 15, "planned into" should be "planned in".
-page 15, "will consists in" should be "will consist of"
-------------------- review 795 --------------------
Overall evaluation: 2 (accept)
Referee's confidence: 3 (high)
A nice, cleanly written paper showing an abstraction of first-order logic
to a decidable second-order logic such that non-provability is
preserved. The intended application of this abstract is as a
preprocessing phase in automated theorem provers in settings were large
numbers of subcases generated are likely to be unprovable.
The result is clean and the proof is well written. This is clearly in
the scope of LPAR.
It would have been nice to see some experimental validation of these
ideas, although including such a thing in this paper is probably
asking too much. One could clearly instrument an existing sub-goaling
theorem provers to have it print out lots of proposed subgoals.
Later, one can see how many of these would actually be rejected and at
what cost. Tight integration with a theorem prover first is not
necessary.
-------------------- review 802 --------------------
Overall evaluation: 2 (accept)
Referee's confidence: 4 (expert)
The paper describes an abstraction technique
for first-order logic whereby formulas are translated
into S0S, preserving provability. Hence, if the translated
formula is not provable in S0S, the original one is not provable
in PL1. Second-order quantifiers are used to approximate
replacement of equals by equals in equational FOL.
I liked the idea very much. It might give us a new
direction for using abstraction for filtering
proof search.
On the downside, I'm not sure how much is gained with this
technique. The examples are extremely simple. Modern
saturation technology---I have run the example in SPASS
automode---terminates on the examples, thus also showing
that they are not provable.
Perhaps the paper should discuss possible ways
of also providing certificates for non-provability.
With provers such as SPASS, to conclude that a conjecture
is not provable one relies on the completeness of the prover,
a property that is rather difficult to verify. With the
approach proposed in the paper, this problem might have a
better solution.
Also, for the non-equational part where the second-order quantifiers
are not needed, I think, abstraction into the monadic class might also
be possible. If so, what would be more precise?
Example 6: something seems wrong here, did you mean all x not (x