Franova et al. [6] have investigated the problem of patching faulty conjectures and proposed a method called PreS (predicate synthesis from formal specification). Their approach is based on the paradigm of predicate synthesis by proofs-as-programs. They explained their method by examples. No formal system is clearly defined and no system is described. Protzen proposed a method which allows to synthesize a corrective predicate during the proof attempt of a faulty conjecture. His approach is similar to ours, but uses rewriting rules and induction rules, he gives some correctness results and dealt with universally quantified formulas. Also Monroy et al. have introduced a method for correcting faulty conjec-tures. However, they only partially deal with the problem of correcting faults. For example, they cannot build a corrective predicate, only identify it as long as it is present in the working theory. More recently, Monroy proposed in [12] another method that consists of a collection of construction commands and is able to synthesize corrective predicates. His approach is also based on the proofs-as-programs paradigm and guarantees the correction and the termination. There is a similarity between his predicates and ours, but his predicates are refined incrementally during the proof process. Monroy poses the problem of automation of the process and suggests to use a proof planning approach. His technics deal with universally quantified formulas. We have presented a new method for patching faulty conjectures by synthesizing definite programs. The contribution of the paper is mainly the construction of corrective predicates by completing failed proof attempts. This method is original because it makes possible to correct formulas comprising of the existential quantifiers and it uses the powerful rules of folding. We proved the partial correctness of this method. We tested our method successfully on several examples borrowed from the literature, and we generally obtain some maximal predicates. The proposed method for patching faulty conjectures and extracting logic programs is implemented in the functional language OCaml (Objective Caml). So in our implementation, the user has to specify which rules to be applied. The full automation of the technique requires some proof strategies. We are investigating several ways. One is to implement some strategies in order to automate our system, a second track is to show that our method is useful in the domain of theorem proving, finally we intend to show that our method can be used to detect protocol attack.
展开▼
