A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23:47-77, 1997.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....indeed, can be considered extensions of OBJ3. There is also exciting new work in term rewriting [11] which is the basis for implementing systems like OBJ3, Maude and CafeOBJ) for example in France around Prof. Jean Pierre Jouannoud, on induction and termination proofs [5] including the spike [4] and CiME systems. The issues discussed in this paper seem to be of increasing importance for computer science, and I think we can look forward to continuing progress. ....

Adel Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47--77, 1997.

....versions of OBJ. There is also exciting new work in term rewriting [16] which is the basis for implementing systems like OBJ3, Maude and CafeOBJ) for example in France around Jean Pierre Jouannoud and Adel Bouhoula, on induction and termination proofs [9] including the spike and CiME systems [8], and some new work on proving behavioral properties with a similar technology [3] The issues discussed in this paper seem to be of increasing importance for computer science, and I think we can look forward to continuing progress. ....

Adel Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47--77, 1997.

No context found.

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47--77, 1997.

No context found.

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47--77, 1997.

....by Goguen et al. 12] Cover sets and cover context sets are fundamental for the correctness of our method. However, they cannot help us to disprove the non observationally valid clauses. For this purpose, we introduce a new notion of critical context sets and we use test sets as de ned in [8]. In the following, we re ne cover context sets so that not only we can prove behavioural properties but we can also disprove the non valid ones. We need rst to introduce the following notions: A context c is quasi ground reducible if for all ground substitution such that dom( var(c) c ....

....of test sets and test substitutions for conditional speci cations is decidable if the axioms are suciently complete and the constructors are speci ed by a set of unconditional equations (see [23,21] Unfortunately, no algorithm exists for the general case of conditional speci cations. However, in [8], a procedure is described for computing test sets when the axioms are suciently complete over an arbitrary speci cation of constructors. 6.2 Computation of critical contexts Let us rst introduce the following lemma which gives us a useful characterization of critical context sets: Lemma 6.9 ....

[Article contains additional citation context not shown here]

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47-77, 1997.

....to free sorts. The validity of such clauses in the initial model is obtained by applying the (non trivial) decision procedure due to Comon and Delor [12] Termination of the transformation process may be achieved if necessary by incorporating appropriate lemmas at step 4. Our method shares with [4] the property of being refutationally complete. This advantage over other methods should not be underestimated: practice shows that code is usually buggy, and therefore many theorems expected to hold do not. The generation of a counterexample can be built in the inference mechanism, hence ....

....0 y = false if y : Neg, whose proof is carried out in section 5. Note the dissymmetry in our completeness proof, which reflects the dissymmetry of the constructor sort structure. 5 Inductive proofs In this section, we develop a goal directed inductive theorem proving procedure in the lines of [7,4]. The inference system builds inductive proofs by instantiating induction variables of a goal by terms in a test set, and then simplifying the obtained instances by appropriate simplification rules, therefore producing new subgoals. 5.1 Simplification Rules We start describing the two kinds of ....

A. Bouhoula. Automated Theorem Proving by Test Set Induction. Journal of Symbolic Computation, 23(1):47--77, 1997.

....to free sorts. The validity of such clauses in the initial model is obtained by applying the (non trivial) decision procedure due to Comon and Delor [9] Termination of the transformation process may be achieved if necessary by incorporating appropriate lemmas at step 4. Our method shares with [4, 2] the property of being refutationally complete. This advantage over other methods should not be underestimated: practice shows that code is usually buggy, and therefore many theorems expected to hold do not. The generation of a counterexample can be built in the inference mechanism, hence avoiding ....

....: Int if y : Neg, which is indeed a simple logical consequence of the subsort declarations, and a non trivial part 0 y = false if y : Neg, whose proof is carried out in section 5. 5 Inductive proofs In this section, we develop a goal directed inductive theorem proving procedure in the lines of [4, 2]. The inference system builds inductive proofs by instantiating induction variables of a goal by terms in a test set, and then simpli P P S INT Neg Nat 0 Int Zero Pos BOOL P S S,P 0 S,P S e S e e e e Figure 4. Kaplan s normal form automaton fying the obtained instances by appropriate ....

A. Bouhoula. Automated Theorem Proving by Test Set Induction. To appear in Journal of Symbolic Computation, 1997.

....are strongly irreducible by R. Cover sets and cover context sets are fundamental for the correctness of our method. However, they cannot help us to disprove the non observationally valid clauses. For this purpose, we introduce a new notion of critical context sets and we use test sets defined in [7]. Definition 4 (test set, test substitution) A test set is a cover set which has the following additional properties: i) the instance of a ground reducible term by a test substitution matches a left hand side of R. ii) if the instance of a positive clause C pos by a test substitution oe is ....

....test sets and test substitutions for conditional specifications is decidable if the axioms are sufficiently complete and the constructors are specified by a set of unconditional equations (see [12] Unfortunately, no algorithm exists for the general case of conditional specifications. However, in [7], a procedure is described for computing test sets when the axioms are sufficiently complete over an arbitrary specification of constructors. 5.2 Computation of critical contexts Let us first introduce the following lemmawhich gives us a useful characterization of critical context sets: Lemma ....

[Article contains additional citation context not shown here]

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47--77, 1997.

....goal (or subgoal) with test terms, and then simplifying the obtained instances, therefore producing new subgoals. I(R) applies to pairs (E ; H) where E is the set of current conjectures and H is the set of inductive hypotheses. Soundness and completeness proofs of our inference system follow [1], showing that a minimal counterexample clause is preserved along a fair derivation when one exists. Finite success is obtained when the set of conjectures to be proved is exhausted. Infinite success is obtained when the procedure diverges, assuming fairness. When this happens, the thing to do is ....

Adel Bouhoula. Automated Theorem Proving by Test Set Induction. Journal of Symbolic Computation, to appear.

No context found.

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23:47-77, 1997.

No context found.

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23:4777, 1997.

No context found.

A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):4777, January 1997.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.