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