Quantification in Nqthm: a Recognizer and Some Constructive Implementations Matt Kaufmann Technical Report 81 August, 1992 Computational Logic Inc. 1717 W. 6th St. Suite 290 Austin, Texas 78703 (512) 322-9951 This research was supported in part by ONR Contract N00014-91-C-0130. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Office of Naval Research or the U.S. Government. ABSTRACT: We present an implementation of a recognizer for quantified notions in the Boyer-Moore Theorem Prover, Nqthm. That is, we provide a method for checking that a given function does indeed represent a quantified notion. We also present methods for generating constructively-presented functions that represent quantified notions, including definitions using only bounded quantifiers. 1. Introduction It is often the case that users of Nqthm [1, 2] want to be able to express first-order quantified notions in Nqthm, or in Pc-Nqthm [3, 4].(We assume familiary with Nqthm and Pc-Nqthm in this report.) Quantifiers can be useful in creating elegant specifications: from a specification standpoint it is sometimes more appropriate to assert that a certain value exists, than to specify that a particular ``witnessing'' function (Skolem function) serves to provide that value. In some cases, the quantifiers are in fact necessary both for the specification and the proof; see for example the discussion of Ramsey's theorem in [5]. In fact, Pc-Nqthm provides the DEFN-SK feature [5] as a direct implementation of first-order quantification, but not all Nqthm users want to use DEFN-SK for representing quantified notions. For example, both Nqthm and Pc-Nqthm users often prefer to use recursive functions to model bounded quantification, for at least two reasons. For one, they may prefer constructivity either on ``ethical'' grounds of parsimony or perhaps because they want to execute their forms. Second, it is often useful to take advantage of the prover's careful heuristics for dealing with recursive functions rather than its relatively weak heuristics for dealing with free variables. Nqthm users know that it is often quite possible to define constructive ``Skolem functions'' to witness ordinary (unbounded) first-order quantifiers. For example, Yuan Yu has informed us of the existence of an unbounded quantifier in his MC68020 work that is really equivalent to a bounded one. There are two goals in the present work. One goal is to implement a recognizer for quantified notions, i.e. some kind of predicate that can inform the user when he has implemented a quantified notion correctly. The other goal is to implement various utilities that generate quantified notions. We will deal with these two goals in the two respective sections that follow. Thus in the first section below we present a new macro CHECK-QUANT that tells us when we have correctly implemented a quantified notion. Here is a brief introduction by way of example. Consider the form (check-quant forall-p4 (i j y) (forall x (implies (and (numberp x) (not (lessp x i)) (lessp x j)) (p4 x i j y))) forall-p4-intro) Here, loosely speaking, this form returns true if and only if the system verifies that in the current theory, with the specific assistance of the event forall-p4-intro, it is the case that the existing function forall-p4 has the property that F i F j F y [(forall-p4 i j y) I F x (implies (and (numberp x) (not (lessp x i)) (lessp x j)) (p4 x i j y))] The second section presents two new tools for generating representations of quantified notions. First we present DEFN-SK-CONSTRUCTIVE, a macro similar to DEFN-SK except that it requires witnessing functions and then generates an appropriate CONSTRAIN event [6]. Then we present an implementation BDD-FORALL of bounded universal quantification. The first appendix is a transcript of a session using BDD-FORALL. The second appendix contains the Lisp code. 2. Recognizing quantified notions. In this section we address the following question: How do we know when we have correctly represented a quantified concept? This question is important, since there are occasions when Nqthm users want to present their work in terms of quantifiers but do not want to use quantifiers explicitly to do their work. We present a utility CHECK-QUANT that has been created to certify that a given function does indeed correctly represent a quantified notion in a given history. Let us be a bit more precise. Let @g[f] be a first-order formula with free variables included in the set {x1 ... xn}. Also, let f be a function symbol with argument list (x1 ... xn). The predicate CHECK-QUANT tells us when it is the case that @g[f] is logically equivalent to (f x1 ... xn) in the current history. More precisely, CHECK-QUANT is conservative in the same sense that the Nqthm prover is conservative: if it answers affirmatively then this logical equivalence holds, but if not then we simply don't know. We begin with an example illustrating the use of CHECK-QUANT as well as an associated utility CHECK-QUANT-HELP. The second subsection contains documentation and a proof of a specification of CHECK-QUANT. 2.1 A sample use of CHECK-QUANT Consider the following rather standard definition of the property that x is a list of natural numbers. (defn all-naturals (x) (if (listp x) (and (numberp (car x)) (all-naturals (cdr x))) t)) In this simple example it is obvious that (all-naturals x) is equivalent to the formula (forall a (implies (member a x) (numberp a))) Now if we were to define a notion based on this quantified formula, using DEFN-SK, we might write (defn-sk all-naturals-quant (x) (forall a (implies (member a x) (numberp a)))) This DEFN-SK event generates the Skolem axiom (AND (IMPLIES (IMPLIES (MEMBER (A X) X) (NUMBERP (A X))) (ALL-NATURALS-QUANT X)) (IMPLIES (NOT (IMPLIES (MEMBER A X) (NUMBERP A))) (NOT (ALL-NATURALS-QUANT X)))) However, rather than submit such a DEFN-SK event, suppose we prefer to use the original all-naturals function. Let us introduce a function that plays the role of the function A in the term above.(Ken Kunen suggested this trick to us some time ago.) Intuitively, this function does its best at finding a counterexample to the universally quantified formula: if any counterexample exists, then this function should find it. (defn bad-guy (x) (if (listp x) (if (not (numberp (car x))) (car x) (bad-guy (cdr x))) 0)) Now we can prove a version of the Skolem axiom displayed above. (prove-lemma all-naturals-is-correct () (and (implies (implies (member (bad-guy x) x) (numberp (bad-guy x))) (all-naturals x)) (implies (not (implies (member a x) (numberp a))) (not (all-naturals x))))) Finally, we can assert that we have indeed defined a quantified notion as claimed. The following form returns T if the equivalence of (all-naturals x) with the indicated quantified formula can be seen to be a theorem of the current theory, with the help of the lemma ALL-NATURALS-IS-CORRECT above. We will see below that this equivalence guarantees that the function all-naturals correctly represents the indicated quantified notion. >(check-quant all-naturals (x) (forall a (implies (member a x) (numberp a))) all-naturals-is-correct) T > Finally, let us mention a utility that can be helpful in conjunction with CHECK-QUANT, called CHECK-QUANT-HELP. Imagine that one want to represent the quantified notion discussed above, (forall a (implies (member a x) (numberp a))), but has not yet defined the ``Skolem function'' bad-guy. Then one could use CHECK-QUANT-HELP as follows: (check-quant-help all-naturals (x) (forall a (implies (member a x) (numberp a)))) The system responds as follows. The new function symbol with its argument list is (A-1 X). (AND (IMPLIES (IMPLIES (MEMBER (A-1 X) X) (NUMBERP (A-1 X))) (ALL-NATURALS X)) (IMPLIES (NOT (IMPLIES (MEMBER A X) (NUMBERP A))) (NOT (ALL-NATURALS X)))) We may then proceed to define bad-guy to have the property that a-1 has in the term above. Alternatively, CHECK-QUANT may take a final argument that is a functional substitution, whose domain should contain exactly the new function symbols reported by CHECK-QUANT-HELP. In this case, then, we could submit the following form. (check-quant all-naturals (x) (forall a (implies (member a x) (numberp a))) ((a-1 bad-guy))) The theorem prover then checks that the functional instance of the term printed above by CHECK-QUANT-HELP, using the functional substitution ((a-1 bad-guy)), is a theorem and returns T if and only if the proof succeeds. 2.2 Precise description of CHECK-QUANT and theoretical justification In this subsection we begin by describing the usage of CHECK-QUANT, including a criterion that we guarantee will be met when CHECK-QUANT returns T. Then we move to the realm of formal logic and present a precise notion of what it means for a function to represent a quantified notion. Finally, we connect up the CHECK-QUANT utility and our logical notion of represents by showing that when the CHECK-QUANT criterion is met, then our notion of represents holds for the given function symbol and formula. The usage of CHECK-QUANT is as follows. (check-quant function arguments formula previous-event-name) Here, function should be a function symbol in the current history, and arguments should be a list of distinct variables that includes all free variables of formula and whose length equals the arity of function. previous-event-name should be the name of a previous event (except, see below for an exception). If this form returns T then the following condition must be met (but not necessarily conversely); otherwise this form returns NIL. (See [6] for a discussion of functional instances and functional substitutions.) CHECK-QUANT CRITERION: A Skolemization of the equivalence (iff (function . arguments) formula) is a functional instance of the Nqthm term (technically, the FORMULA-OF) associated with previous-event-name. Finally, as a convenience we allow previous-event-name to be a functional substitution fs instead of an event name, as long as certain conditions are met. Let @g[y] be the Skolemization given by DEFN-SK of the formula (iff (function . arguments) formula) displayed above. Then the domain of fs must consist of the Skolem functions generated by DEFN-SK in producing @g[y], and its range should contain only symbols(Perhaps this latter restriction can be relaxed, but we haven't bothered to do so.). In addition, application of f to @g[y], i.e. @g[y] \ fs must be a theorem of the given history. (See [6] for more about functional substitutions.) For the rest of this section we will consider only the case above where previous-event-name is a previous event name, rather than a functional substitution. The proof of the theorem below in the other case follows easily from the theorem we prove, and is left to the reader. Let us now state just what it means for CHECK-QUANT to be a correct recognizer for first-order notions. Definition. Let @g[G] be a first-order theory (set of sentences), let @g[f] be a first-order sentence, let f be a function symbol not occurring in @g[f], and let x , ..., x be 1 n distinct variables including all the free variables of @g[f], where n is the arity of f. We say that f(x ,...,x ) represents 1 n @g[f] in @g[G] if @g[G] |- [f(x ,...,x ) I @g[f]]. 1 n An important consequence of this notion of represents, which we will not need here, is the following trivial corollary. It is simply a formal statement asserting that ``represents'' has the desired property, namely that the given first-order formula can be replaced by the corresponding function application. Proposition. Suppose that f(x ,...,x ) represents @g[f] in 1 n @g[G]. Then for any substitution s, @g[G] |- [f(s(x ),...,s(x )) 1 n I @g[f]/s] (where we define s(x) = x for all x not in the domain of s). -| For the rest of this paper, functional substitutions will always associate function symbols (rather than LAMBDA terms) with function symbols. Here is the theorem stating correctness of our approach. We think of the theory @g[G] below as being the set of theorems of the current history, and of P as being the formula associated with some existing event, i.e. of what we called previous-event-name above. In the theorem below, think of fs as substituting only for function symbols that do not occur in the current history, i.e. for the ones generated by the indicated Skolemization. Theorem. Suppose that f is a function symbol, x ,...,x is a 1 n list of distinct variables where n equals the arity of f, and @g[y] is a Skolemization of the following equivalence: (iff (f x ... x ) @g[f]) 1 n where @g[f] is a formula whose free variables all belong to {x 1 .. x }. Also let P be a theorem of @g[G], and suppose that fs is n a functional substitution such that @g[y]\fs is P, where the domain of fs consists of function symbols not occurring in @g[f], {f}, or @g[G]. Then f(x ,...,x ) represents @g[f] in @g[G]. 1 n Proof. We have to show that @g[G] |- [f(x ,...,x ) I @g[f]]. 1 n Now a basic property of Skolemization (see for example Lemma 2(2) of [7], or Proposition 1 in the second appendix of the technical report version of [5]) is that each Skolemization (actually its universal closure) implies the formula from which it comes. It is routine to check that in fact, this argument does not depend on the choice of Skolem function symbols. It is then clear then that @g[y]\fs may itself be viewed as a Skolemization (in this more general sense) of the equivalence displayed above. Therefore, by the above property of Skolemization, since @g[y]\fs is a theorem of @g[G], therefore so is the equivalence displayed above. Here is an alternate, model-theoretic argument. We know that it is logically valid that @g[y]' R equiv, where equiv is the equivalence displayed above and @g[y]' is the universal closure of @g[y]. But logical validity is preserved by functional substitutions in which the range is disjoint from the domain, for if the negation of a sentence A\fs has a model M, then the negation of A has a model: simply expand M to interpret the function symbols in the domain of fs by the interpretations in M of what fs maps them to. Therefore, it is also logically valid that (@g[y]' R equiv)\fs, i.e. that ((@g[y]\fs)' R equiv). -| 3. Generating quantified notions Recall that DEFN-SK [5] allows the user to introduce quantified notions into the Boyer-Moore paradigm. In the preceding section we introduced a recognizer for when one has correctly represented quantified notions, and in fact we believe that DEFN-SK always produces functions that represent desired quantified notions. For example, after the event (defn-sk all-naturals-quant (x) (forall a (implies (member a x) (numberp a)))) we obtain a result of T upon evaluation of the form (check-quant all-naturals-quant (x) (forall a (implies (member a x) (numberp a))) all-naturals-quant) However, we have already pointed out in the introduction that there are times when the user would prefer to avoid the DEFN-SK mechanism. In this section we present two tools for this purpose. The first, DEFN-SK-CONSTRUCTIVE, is quite general: it behaves just like DEFN-SK, except that it requires the user to provide existing ``witnessing functions'' (in the spirit of CONSTRAIN, cf. [6]) for each of the newly-introduced functions. The second, BDD-FORALL, is an implementation of bounded universal quantification by way of primitive recursive functions. This latter construct is somewhat similar in intent to the more sophisticated and far-reaching ideas for bounded quantification in [8], but is simpler and is based on the DEFN-SK-CONSTRUCTIVE mechanism mentioned above, which in turn is based on CONSTRAIN [6]. Thus, BDD-FORALL is likely to be easily portable to the Acl2 system [9] that is currently under development, unlike the implementation of bounded quantification in [8], which is based on the EVAL$ construct of Nqthm [2] that is not likely to be ported to Acl2. 3.1 DEFN-SK-CONSTRUCTIVE Suppose that one wants the elegance and rewrite rules provided by DEFN-SK but wishes to stay within the ``constructive'' world. For example, consider again the notion that every member of a given list is a natural number. Recall that we gave the following recursive definition of this notion, (defn all-naturals (x) (if (listp x) (and (numberp (car x)) (all-naturals (cdr x))) t)) and also the ``nonconstructive'' version that uses explicit quantification: (defn-sk all-naturals-quant (x) (forall a (implies (member a x) (numberp a)))) This event adds the ``Skolem'' axiom (AND (IMPLIES (IMPLIES (MEMBER (A X) X) (NUMBERP (A X))) (ALL-NATURALS-QUANT X)) (IMPLIES (NOT (IMPLIES (MEMBER A X) (NUMBERP A))) (NOT (ALL-NATURALS-QUANT X)))) which is then stored as two rewrite rules. We now present a similar mechanism for introducing a quantified notion, but one which does not rely on the nonconstructivity of DEFN-SK. Here is an auxiliary definition (repeated from the preceding section) followed by an example of the new ``event.'' (defn bad-guy (x) (if (listp x) (if (not (numberp (car x))) (car x) (bad-guy (cdr x))) 0)) (defn-sk-constructive all-naturals-quant (x) (forall a (implies (member a x) (numberp a))) ((all-naturals-quant all-naturals) (a bad-guy))) In this case the relevant event is called ALL-NATURALS-QUANT- INTRO, but the rewrite rules stored are the same ones stored for the DEFN-SK event above (except for their names). The ``witnessing alist'' ((all-naturals-quant all-naturals) (a bad-guy)) instructs the system to take the Skolem axiom created by DEFN-SK (see above), then functionally instantiate it with this functional substitution, and finally prove that instantiated term: (AND (IMPLIES (IMPLIES (MEMBER (bad-guy X) X) (NUMBERP (bad-guy X))) (all-naturals X)) (IMPLIES (NOT (IMPLIES (MEMBER A X) (NUMBERP A))) (NOT (all-naturals X)))) Fortunately, there is assistance in seeing the form required for the ``witnessing alist.'' One simply leaves off that argument and calls DEFN-SK-CONSTRUCTIVE-HELP instead of DEFN-SK-CONSTRUCTIVE. >(defn-sk-constructive-help all-naturals-quant (x) (forall a (implies (member a x) (numberp a)))) The Skolemized formula will be: (AND (IMPLIES (IMPLIES (MEMBER (A X) X) (NUMBERP (A X))) (ALL-NATURALS-QUANT X)) (IMPLIES (NOT (IMPLIES (MEMBER A X) (NUMBERP A))) (NOT (ALL-NATURALS-QUANT X)))). The witnessing function alist should have roughly the form: ((A ???) (ALL-NATURALS-QUANT ???)). T > Actually, a call to DEFN-SK-CONSTRUCTIVE simply generates a call to CONSTRAIN for the Skolem axiom that DEFN-SK would have generated, as illustrated by the response below that Lisp gives to a request to expand the DEFN-SK-CONSTRUCTIVE macro. >(macroexpand-1 '(defn-sk-constructive all-naturals-quant (x) (forall a (implies (member a x) (numberp a))) ((all-naturals-quant all-naturals) (a bad-guy)))) (CONSTRAIN ALL-NATURALS-QUANT-INTRO (REWRITE) (AND (IMPLIES (IMPLIES (MEMBER (A X) X) (NUMBERP (A X))) (ALL-NATURALS-QUANT X)) (IMPLIES (NOT (IMPLIES (MEMBER A X) (NUMBERP A))) (NOT (ALL-NATURALS-QUANT X)))) ((ALL-NATURALS-QUANT ALL-NATURALS) (A BAD-GUY))) T > The general form for DEFN-SK-CONSTRUCTIVE is as follows: (DEFN-SK-CONSTRUCTIVE function-name formal-parameters quantified-formula (... ( new old ) ...) i i &OPTIONAL hints) where hints are as in hints to PROVE-LEMMA and (... ( new old ) i i ...) is as in the corresponding argument to CONSTRAIN. Finally, we observe that this call to DEFN-SK-CONSTRUCTIVE does indeed give us a history in which (all-naturals-quant x) represents the indicated quantified formula, in the sense described in the preceding section. >(check-quant all-naturals-quant (x) (forall a (implies (member a x) (numberp a))) all-naturals-quant-intro) T > Although we believe that using DEFN-SK-CONSTRUCTIVE provides functions that represent quantified formulas, we encourage the user to use CHECK-QUANT as indicated above in order to gain such assurance. 3.2 BDD-FORALL The final utility we provide is one that generates appropriate events for defining notions with a single outermost universal quantifier. Of course it is then possible to allow arbitrary bounded quantifiers simply by introducing such notions in an inside-out manner. An example should suffice to illustrate the technique. Suppose we have already declared or defined a 4-place predicate p4, e.g. (dcl p4 (a b c d)) and wish to represent the following quantified notion forall-p4 (with free variables i, j, and y): For all natural numbers x such that i L x < j, (p4 x i j y) holds The following form is used to introduce a function forall-p4, with formal parameters i, j, and y, that defines this notion: (bdd-forall forall-p4 x i j (i j y) (p4 x i j y)) Note however that any term can serve the function of (p4 x i j y); that term need not be an application of a function symbol to variables. In Appendix A we show what events are actually generated by this form. The only event generated by a call of BDD-FORALL that really matters for subsequent events, however, is the final one. The final one is actually a DEFN-SK-CONSTRUCTIVE (see the preceding subsection), and the other events are present simply to assist in the acceptance of this final event. Here is what that final event looks like for the example above, though since the functional substitution and hints are generated by the system, there is really no need for the user to look at these. (DEFN-SK-CONSTRUCTIVE FORALL-P4 (I J Y) (FORALL X (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y))) ((X FORALL-P4-SK-MODEL) (FORALL-P4 FORALL-P4-MODEL)) ((USE (FORALL-P4-MODEL-NECC) (FORALL-P4-MODEL-SUFF)) (DISABLE-THEORY T) (ENABLE-THEORY GROUND-ZERO))) Following our own admonition from the preceding subsection, let us check that we have correctly represented the quantified notion in question. >(check-quant forall-p4 (i j y) (forall x (implies (and (numberp x) (not (lessp x i)) (lessp x j)) (p4 x i j y))) forall-p4-intro) T > It should be straightforward to define the analog of BDD-FORALL for the existential quantifier, as well as versions for primitive recursion over finite lists instead of over numbers. We simply have not yet done so. We may also wish to reimplement BDD-FORALL so that it is based entirely on DEFN events rather than on a CONSTRAIN event, so that the resulting function will be executable. Appendix A Transcript from an execution of a BDD-FORALL form This appendix serves not only to illustrate BDD-FORALL, but in fact it illustrates all of the notions introduced in this paper. The run below took place on a Sun 3/60 with 24 megabytes of main memory. client12:kaufmann[82]% pc-nqthm AKCL (Austin Kyoto Common Lisp) Version(1.602) Sun Sep 29 19:41:25 CDT 1991 Contains Enhancements by W. Schelter Nqthm, with functional instantiation. Initialized with (BOOT-STRAP NQTHM) on September 29, 1991 22:26:0. >(load "defn-sk-constructive.o") Loading defn-sk-constructive.o start address -T 594000 Finished loading defn-sk-constructive.o 14016 >(dcl p4 (x i j y)) [ 0.0 0.0 0.0 ] P4 >(bdd-forall forall-p4 x i j (i j y) ;; for all x with i <= x < j, (p4 x i j y) holds (p4 x i j y)) ^L (DEFN FORALL-P4-SK-MODEL-AUX (X I J Y) (IF (LESSP X J) (IF (NOT (P4 X I J Y)) X (FORALL-P4-SK-MODEL-AUX (ADD1 X) I J Y)) J) ((LESSP (DIFFERENCE (ADD1 J) X)))) Linear arithmetic establishes that the measure (DIFFERENCE (ADD1 J) X) decreases according to the well-founded relation LESSP in each recursive call. Hence, FORALL-P4-SK-MODEL-AUX is accepted under the principle of definition. Observe that: (OR (NUMBERP (FORALL-P4-SK-MODEL-AUX X I J Y)) (EQUAL (FORALL-P4-SK-MODEL-AUX X I J Y) X) (EQUAL (FORALL-P4-SK-MODEL-AUX X I J Y) J)) is a theorem. [ 0.1 0.0 0.1 ] FORALL-P4-SK-MODEL-AUX ^L (DEFN FORALL-P4-SK-MODEL (I J Y) (FORALL-P4-SK-MODEL-AUX (FIX I) I J Y)) From the definition we can conclude that: (OR (NUMBERP (FORALL-P4-SK-MODEL I J Y)) (EQUAL (FORALL-P4-SK-MODEL I J Y) J)) is a theorem. [ 0.1 0.0 0.0 ] FORALL-P4-SK-MODEL ^L (DEFN FORALL-P4-MODEL-AUX (X I J Y) (IF (LESSP X J) (IF (P4 X I J Y) (FORALL-P4-MODEL-AUX (ADD1 X) I J Y) F) T) ((LESSP (DIFFERENCE (ADD1 J) X)))) Linear arithmetic informs us that the measure (DIFFERENCE (ADD1 J) X) decreases according to the well-founded relation LESSP in each recursive call. Hence, FORALL-P4-MODEL-AUX is accepted under the principle of definition. Note that: (OR (FALSEP (FORALL-P4-MODEL-AUX X I J Y)) (TRUEP (FORALL-P4-MODEL-AUX X I J Y))) is a theorem. [ 0.1 0.0 0.1 ] FORALL-P4-MODEL-AUX ^L (DEFN FORALL-P4-MODEL (I J Y) (FORALL-P4-MODEL-AUX (FIX I) I J Y)) From the definition we can conclude that: (OR (FALSEP (FORALL-P4-MODEL I J Y)) (TRUEP (FORALL-P4-MODEL I J Y))) is a theorem. [ 0.1 0.0 0.0 ] FORALL-P4-MODEL ^L (PROVE-LEMMA FORALL-P4-MODEL-AUX-NECC NIL (IMPLIES (NOT (IMPLIES (AND (NUMBERP X) (NUMBERP X**) (NOT (LESSP X X**)) (LESSP X J)) (P4 X I J Y))) (NOT (FORALL-P4-MODEL-AUX X** I J Y)))) Name the conjecture *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LESSP X** J) (P4 X** I J Y) (p (ADD1 X**) I J Y X)) (p X** I J Y X)) (IMPLIES (AND (LESSP X** J) (NOT (P4 X** I J Y))) (p X** I J Y X)) (IMPLIES (NOT (LESSP X** J)) (p X** I J Y X))). Linear arithmetic can be used to show that the measure: (DIFFERENCE (ADD1 J) X**) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates four new conjectures: <<<... rest of proof omitted; simplification is all that's needed >>> That finishes the proof of *1. Q.E.D. [ 0.1 1.0 0.7 ] FORALL-P4-MODEL-AUX-NECC ^L (PROVE-LEMMA FORALL-P4-MODEL-NECC NIL (IMPLIES (NOT (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y))) (NOT (FORALL-P4-MODEL I J Y))) ((USE (FORALL-P4-MODEL-AUX-NECC (X** (FIX I)))))) This simplifies, opening up the functions FIX, NOT, AND, IMPLIES, LESSP, and FORALL-P4-MODEL, to: (IMPLIES (AND (NOT (NUMBERP I)) (LESSP X 0) (NUMBERP X) (LESSP X J) (NOT (P4 X I J Y))) (NOT (FORALL-P4-MODEL-AUX 0 I J Y))). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.1 0.8 0.1 ] FORALL-P4-MODEL-NECC ^L (PROVE-LEMMA FORALL-P4-MODEL-AUX-SUFF NIL (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LET ((X (FORALL-P4-SK-MODEL-AUX X I J Y))) (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y)))) (FORALL-P4-MODEL-AUX X I J Y)) ((INDUCT (FORALL-P4-MODEL-AUX X I J Y)))) This formula can be simplified, using the abbreviations IMPLIES, NOT, OR, and AND, to the following three new goals: <<<... rest of proof omitted; simplification is all that's needed >>> Q.E.D. [ 0.1 7.2 0.9 ] FORALL-P4-MODEL-AUX-SUFF ^L (PROVE-LEMMA FORALL-P4-MODEL-SUFF NIL (LET ((X (FORALL-P4-SK-MODEL I J Y))) (IMPLIES (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y)) (FORALL-P4-MODEL I J Y))) ((USE (FORALL-P4-MODEL-AUX-SUFF (X (FIX I)))))) This simplifies, unfolding the definitions of FIX, NOT, AND, IMPLIES, FORALL-P4-SK-MODEL, LESSP, and FORALL-P4-MODEL, to seven new conjectures: <<<... rest of proof omitted; simplification is all that's needed >>> Q.E.D. [ 0.1 4.4 0.5 ] FORALL-P4-MODEL-SUFF ^L (DEFN-SK-CONSTRUCTIVE FORALL-P4 (I J Y) (FORALL X (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y))) ((X FORALL-P4-SK-MODEL) (FORALL-P4 FORALL-P4-MODEL)) ((USE (FORALL-P4-MODEL-NECC) (FORALL-P4-MODEL-SUFF)) (DISABLE-THEORY T) (ENABLE-THEORY GROUND-ZERO))) WARNING: Note that FORALL-P4-INTRO contains the free variable X which will be chosen by instantiating the hypothesis: (NOT (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y))). We will verify the consistency and the conservative nature of this constraint by attempting to prove: (AND (IMPLIES (IMPLIES (AND (NUMBERP (FORALL-P4-SK-MODEL I J Y)) (NOT (LESSP (FORALL-P4-SK-MODEL I J Y) I)) (LESSP (FORALL-P4-SK-MODEL I J Y) J)) (P4 (FORALL-P4-SK-MODEL I J Y) I J Y)) (FORALL-P4-MODEL I J Y)) (IMPLIES (NOT (IMPLIES (AND (NUMBERP X) (NOT (LESSP X I)) (LESSP X J)) (P4 X I J Y))) (NOT (FORALL-P4-MODEL I J Y)))) This formula simplifies, unfolding the definitions of NOT, AND, IMPLIES, and LESSP, to: T. Q.E.D. [ 0.5 3.7 0.0 ] FORALL-P4-INTRO T >(check-quant forall-p4 (i j y) (forall x (implies (and (numberp x) (not (lessp x i)) (lessp x j)) (p4 x i j y))) forall-p4-intro) T > Appendix B The Common Lisp code (defun defn-sk-constructive-fn (name args body witness-alist hints defn-sk-hints) (let (skolemized-body new-functions-and-formals) (match! (chk-acceptable-defn-sk name args body defn-sk-hints) (list name args body defn-sk-hints skolemized-body new-functions-and-formals)) (nconc (list 'constrain (pack (list name '-intro)) '(rewrite) skolemized-body witness-alist) (if hints (list hints) nil)))) (defmacro defn-sk-constructive (name args body witness-alist &optional hints defn-sk-hints) (defn-sk-constructive-fn name args body witness-alist hints defn-sk-hints)) (defmacro defn-sk-constructive-help (name args body) (let (skolemized-body new-functions-and-formals) (match! (chk-acceptable-defn-sk name args body hints) (list name args body hints skolemized-body new-functions-and-formals)) (PRINEVAL (PQUOTE (PROGN CR CR |The| |Skolemized| |formula| |will| |be| |:|)) nil 0 PROVE-FILE) (PRINEVAL (PQUOTE (PROGN CR (!term skolemized-body (quote |.|)) CR |The| |witnessing| |function| |alist| |should| |have| |roughly| |the| |form| |:|)) `((skolemized-body . ,skolemized-body)) 0 PROVE-FILE) (PRINEVAL (PQUOTE (PROGN CR (!ppr x (quote |.|)) CR CR)) `((X . ,(iterate for fn-formals in new-functions-and-formals collect (list (car fn-formals) '???)))) 0 PROVE-FILE) t)) (defun defn-sk-nonconstructive-fn (name args body defn-sk-hints) (let (skolemized-body new-functions-and-formals) (match! (chk-acceptable-defn-sk name args body defn-sk-hints) (list name args body defn-sk-hints skolemized-body new-functions-and-formals)) `(let (undone-events) (do-events ',(iterate for fn-args in new-functions-and-formals with temp collect `(dcl ,(car fn-args) ,(cdr fn-args)) into temp finally (return (append temp `((add-axiom ,(pack (list name '-intro)) (rewrite) ,(untranslate skolemized-body)) (add-axiom ,(pack (list name '-boolean)) (rewrite) (or (truep (,name ,@args)) (falsep (,name ,@args)))))))))))) (defmacro defn-sk-nonconstructive (name args body &optional defn-sk-hints) (defn-sk-nonconstructive-fn name args body defn-sk-hints)) (defun functionally-one-way-unify-rec (pat term fns acc &aux pair) ;; Returns a functional substitution fs with domain contained in ;; fns, no member of which is a constructor, such that ;; pat \ (fs U acc) = term; or else returns 'fail. Here we're doing very ;; simple one-way unification -- no fancy higher-order stuff, ;; and every function symbol that's bound is bound to a symbol. ;; Let's say that the "free" function symbols are those in fns ;; which aren't bound in acc. ;; We assume that no function symbol of fns occurs in term. (cond ((variablep pat) (if (eq pat term) acc 'fail)) ((fquotep pat) (if (equal pat term) acc 'fail)) ((variablep term) 'fail) ((eq (ffn-symb pat) (fn-symb term)) ;; then by assumption, (ffn-symb pat) is not in fns, and hence ;; we'll never replace it (functionally-one-way-unify-lst (fargs pat) (sargs term) fns acc)) ((setq pair (assoc-eq (ffn-symb pat) acc)) (if (eq (cdr pair) (fn-symb term)) (functionally-one-way-unify-lst (fargs pat) (sargs term) fns acc) 'fail)) ((not (member-eq (ffn-symb pat) fns)) 'fail) ((= (arity (ffn-symb pat)) (arity (fn-symb term))) ;; otherwise we are allowed to bind the function symbol of pat (functionally-one-way-unify-lst (fargs pat) (sargs term) fns (cons (cons (ffn-symb pat) (fn-symb term)) acc))) (t 'fail))) (defun functionally-one-way-unify-lst (patlist termlist fns acc) (if patlist (let ((new-acc (functionally-one-way-unify-rec (car patlist) (car termlist) fns acc))) (if (eq new-acc 'fail) 'fail (functionally-one-way-unify-lst (cdr patlist) (cdr termlist) fns new-acc))) acc)) (defun functionally-one-way-unify (patlist termlist fns) (functionally-one-way-unify-rec patlist termlist fns nil)) (defun fnnamep-formula (fn x &aux (args (formula-args x)) (op (formula-op x))) (cond ((eq op 'term) (fnnamep fn args)) ((member-eq op '(forall exists)) (fnnamep-formula fn (cadr args))) (t (iterate for arg in args thereis (fnnamep-formula fn arg))))) (defun is-skolemization (term formula &optional translate-flg) ;; adapted from CHK-ACCEPTABLE-DEFN-SK (let ((translated-formula (if translate-flg (translate-to-formula formula) formula)) (untranslated-formula (if translate-flg formula (untranslate-formula formula)))) (when translate-flg (setq term (translate term))) (let ((x (skolemize translated-formula t)) (arity-alist arity-alist)) (iterate for pair in *new-functions-and-formals* do (setq arity-alist (cons (cons (car pair) (length (cdr pair))) arity-alist))) (setq unify-subst (functionally-one-way-unify x term (mapcar 'car *new-functions-and-formals*))) (if (eq unify-subst 'fail) (progn (PRINEVAL (PQUOTE (PROGN CR |The| |Skolemization| |of| CR (!ppr untranslated-formula nil) |is| CR (!term x nil) |,| |but| |the| |term| (!term term nil) |is| |not| |a| |functional| |instance| |of| |that| |term| |.| CR CR)) `((untranslated-formula . ,untranslated-formula) (x . ,x) (term . ,term)) 0 PROVE-FILE) nil) t)))) (defun check-quant-with-fs (name witness-alist) ;; This is adapted from Nqthm code for CHK-ACCEPTABLE-CONSTRAIN. ;; Remember, the basic idea is that to show that a quantified ;; notion is correctly represented, we need to show that a ;; functional instantiation of a Skolemization is a theorem. ;; I'm probably could allow lambda expressions, but I won't ;; at this time. ; It is important that the function symbols being witnessed, i.e., ; the new function symbols, not occur in the terms in the range of ; the substitution. This is insured by our not binding ARITY-ALIST ; until after the TRANSLATE on the range terms. (MATCH! (CHK-ACCEPTABLE-FUNCTIONAL-SUBSTITUTION WITNESS-ALIST T) (LIST WITNESS-ALIST)) (OR (NO-DUPLICATESP (CONS NAME (ITERATE FOR DOUBLET IN WITNESS-ALIST COLLECT (CAR DOUBLET)))) (ER SOFT NIL |it| |is| |illegal| |to| |use| |the| |name| |of| |a| |Skolem| |function| |for| |the| |name| |of| |the| |function| |that| |is| |representing| |the| |quantified| |notion| |,| |or| |to| |duplicate| |a| |function| |in| |the| |domain| |of| |the| |witnessing| |alist| |of| |the| |constraint| |.|)) (or (iterate for doublet in witness-alist always (symbolp (cadr doublet))) (er soft nil |We| |do| |not| |currently| |allow| |lambda| |expressions| |in| |the| |witnessing| |alist| |for| |CHECK-QUANT| |.|)) WITNESS-ALIST) (defun check-quant-fn (NAME ARGS BODY event-name-or-witness-alist hints &aux formula) ;; Checks that an existing notion NAME defines the notion in BODY ;; in the sense that (IFF (NAME . ARGS) BODY). (or (get name 'type-prescription-lst) (er soft (name) (!ppr name nil) |is| |not| |a| |function| |known| |in| |the| |current| |history| |.|)) (chk-arglist name args) (setq formula (translate-to-formula body)) (if (fnnamep-formula name formula) (progn (PRINEVAL (PQUOTE (PROGN CR |The| |function| |symbol| (!ppr name nil) |occurs| |in| |the| |formula| (!ppr body nil) |,| |and| |hence| (!ppr x nil) |is| |not| |what| |we| |call| |a| |representation| |of| |the| |indicated| |quantified| |notion| |.| CR CR)) `((name . ,name) (body . ,body) (x . (,name ,@args))) 0 PROVE-FILE) (return-from check-quant-fn nil))) ;; could probably omit the following (free-var-chk-formula name args formula) (cond ((symbolp event-name-or-witness-alist) (if (formula-of event-name-or-witness-alist) (is-skolemization (formula-of event-name-or-witness-alist) (make-defn-sk-formula name args formula)) (progn (PRINEVAL (PQUOTE (PROGN CR |The| |symbol| (!ppr event-name-or-witness-alist nil) |is| |not| |the| |name| |of| |an| |event| |with| |a| |formula| |.| CR CR)) `((event-name-or-witness-alist . ,event-name-or-witness-alist)) 0 PROVE-FILE) nil))) (t ;; Otherwise, we check that the result of functionally substituting ;; the witness-alist into the Skolemization is really a theorem, even ;; though it would in fact be legal to further substitute and get a ;; theorem then instead. (let ((term (skolemize (make-defn-sk-formula name args formula) t)) (arity-alist arity-alist)) (iterate for pair in *new-functions-and-formals* do (setq arity-alist (cons (cons (car pair) (length (cdr pair))) arity-alist))) (iterate for pair in event-name-or-witness-alist do (or (assoc-eq (car pair) *new-functions-and-formals*) (er soft ((fn (car pair))) |The| |function| |symbol| (!ppr fn nil) |appears| |in| |the| |domain| |of| |the| |witnessing| |alist| |but| |is| |not| |a| |Skolem| |function| |generated| |by| |the| |Skolemizer| |in| |the| |current| |context| |.|))) (iterate for pair in *new-functions-and-formals* do (or (assoc-eq (car pair) event-name-or-witness-alist) (er soft ((fn (car pair)) term) |The| |function| |symbol| (!ppr fn nil) |was| |generated| |as| |a| |Skolem| |function| |but| |does| |not| |appear| |in| |the| |witnessing| |alist| |that| |was| |supplied| |.| |The| |Skolemization| |is| |:| CR (!term term '|.|)))) (let ((term-to-prove (sublis-fn (iterate for doublet in (check-quant-with-fs name event-name-or-witness-alist) collect (cons (car doublet) (cadr doublet))) term))) (PRINEVAL (PQUOTE (PROGN CR |Our| |proof| |obligation| |is| |:| (!ppr term-to-prove '|.|) CR CR)) `((term-to-prove . ,term-to-prove)) 0 PROVE-FILE) ;; The following is adapted from the code for PROVE-LEMMA (LET ((IN-PROVE-LEMMA-FLG T) PROVE-ANS) (MATCH! (CHK-ACCEPTABLE-HINTS HINTS) (LIST HINTS)) (UNWIND-PROTECT (progn ;; Call translate first so that if arities is wrong, we ;; find out now. Kind of a shame, since PROVE calls translate ;; too, but that's OK. (or (error1-set (setq term-to-prove (translate (APPLY-HINTS HINTS TERM-to-prove)))) (er soft nil |Aborting| |,| |since| |our| |proof| |obligation| |is| |not| |well-formed| |.|)) (and (PROVE term-to-prove) t)) (PROGN (ITERATE FOR X IN HINT-VARIABLE-ALIST DO (SET (CADR X) (CADDDR X))) (SETQ LOCAL-DISABLEDP-HASH-FLAG NIL))))))))) (defmacro check-quant (&optional NAME ARGS BODY event-name hints) (if (or (null name) (null body) (null event-name)) (er soft nil CHECK-QUANT |has| |four| |required| |arguments| |.|) (if (and event-name (symbolp event-name) hints) (er soft (event-name hints) |Since| |a| |previous| |event| |name| |was| |specified| |,| |namely| (!ppr event-name nil) |,| |it| |is| |not| |sensible| |or| |legal| |to| |supply| |hints| |here| |.| |The| |final| |argument| (!ppr hints nil) |to| CHECK-QUANT |is| |thus| |illegal| |.|) `(check-quant-fn ',name ',args ',body ',event-name ',hints)))) (defun check-quant-help-fn (NAME ARGS BODY &aux formula) ;; Checks that an existing notion NAME defines the notion in BODY ;; in the sense that (IFF (NAME . ARGS) BODY). (or (arity name) (er soft (name) (!ppr name nil) |is| |not| |a| |function| |known| |in| |the| |current| |history| |.|)) (chk-arglist name args) (setq formula (translate-to-formula body)) ;; could probably omit the following (free-var-chk-formula name args formula) (let ((x (skolemize (make-defn-sk-formula name args formula) t))) (PRINEVAL (PQUOTE (PROGN CR |The| |new| |function| (plural? y (progn |symbols| |with| |their| |argument| |lists| |are|) (progn |symbol| |with| |its| |argument| |list| |is|)) (!ppr-list y (quote |.|)) CR CR)) `((y . ,*new-functions-and-formals*)) 0 PROVE-FILE) (untranslate x))) (defmacro check-quant-help (name args body) `(check-quant-help-fn ',name ',args ',body)) (defun bdd-forall-sk-model-aux (bdd-forall-sk-model-aux-name qvar upper args body) `(defn ,bdd-forall-sk-model-aux-name ,(cons qvar args) (if (lessp ,qvar ,upper) (if (not ,body) ,qvar (,bdd-forall-sk-model-aux-name (add1 ,qvar) ,@args)) ,upper) ((lessp (difference (add1 ,upper) ,qvar))))) (defun bdd-forall-sk-model (bdd-forall-sk-model-aux-name bdd-forall-sk-model-name lower args) `(defn ,bdd-forall-sk-model-name ,args (,bdd-forall-sk-model-aux-name (fix ,lower) ,@args))) (defun bdd-forall-model-aux (bdd-forall-model-aux-name qvar upper args body) `(defn ,bdd-forall-model-aux-name ,(cons qvar args) (if (lessp ,qvar ,upper) (if ,body (,bdd-forall-model-aux-name (add1 ,qvar) ,@args) f) t) ((lessp (difference (add1 ,upper) ,qvar))))) (defun bdd-forall-model (bdd-forall-model-aux-name bdd-forall-model-name lower args) `(defn ,bdd-forall-model-name ,args (,bdd-forall-model-aux-name (fix ,lower) ,@args))) (defun bdd-forall-model-aux-necc (bdd-forall-model-aux-necc-name bdd-forall-model-aux-name qvar qvar** upper args body) `(prove-lemma ,bdd-forall-model-aux-necc-name () (implies (not (implies (and (numberp ,qvar) (numberp ,qvar**) (not (lessp ,qvar ,qvar**)) (lessp ,qvar ,upper)) ,body)) (not (,bdd-forall-model-aux-name ,qvar** ,@args))))) (defun bdd-forall-model-necc (bdd-forall-model-necc-name bdd-forall-model-name bdd-forall-model-aux-necc-name qvar qvar** lower upper args body) `(prove-lemma ,bdd-forall-model-necc-name () (implies (not (implies (and (numberp ,qvar) (not (lessp ,qvar ,lower)) (lessp ,qvar ,upper)) ,body)) (not (,bdd-forall-model-name ,@args))) ((use (,bdd-forall-model-aux-necc-name (,qvar** (fix ,lower))))))) (defun bdd-forall-model-aux-suff (bdd-forall-model-aux-suff-name bdd-forall-sk-model-aux-name bdd-forall-model-aux-name qvar lower upper args body) `(prove-lemma ,bdd-forall-model-aux-suff-name () (implies (and (numberp ,qvar) (not (lessp ,qvar i)) (let ((,qvar (,bdd-forall-sk-model-aux-name ,qvar ,@args))) (implies (and (numberp ,qvar) (not (lessp ,qvar ,lower)) (lessp ,qvar ,upper)) ,body))) (,bdd-forall-model-aux-name ,qvar ,@args)) ((induct (,bdd-forall-model-aux-name ,qvar ,@args))))) (defun bdd-forall-model-suff (bdd-forall-model-aux-suff-name bdd-forall-model-suff-name bdd-forall-sk-model-name bdd-forall-model-name qvar lower upper args body) `(prove-lemma ,bdd-forall-model-suff-name () (let ((,qvar (,bdd-forall-sk-model-name ,@args))) (implies (implies (and (numberp ,qvar) (not (lessp ,qvar ,lower)) (lessp ,qvar ,upper)) ,body) (,bdd-forall-model-name ,@args))) ((use (,bdd-forall-model-aux-suff-name (,qvar (fix ,lower))))))) (defun bdd-forall-defn-sk-constructive (name bdd-forall-sk-model-name bdd-forall-model-necc-name bdd-forall-model-suff-name bdd-forall-model-name qvar lower upper args body) `(defn-sk-constructive ,name ,args (forall ,qvar (implies (and (numberp ,qvar) (not (lessp ,qvar ,lower)) (lessp ,qvar ,upper)) ,body)) ((,(make-new-skolem-fn-1 qvar 0 (list (cons name args))) ,bdd-forall-sk-model-name) (,name ,bdd-forall-model-name)) ((use (,bdd-forall-model-necc-name) (,bdd-forall-model-suff-name)) (disable-theory t) (enable-theory ground-zero)))) (defun bdd-forall-events (name qvar lower upper args body) ;; defines (name .args) to be ;; (forall qvar (implies (and (numberp qvar) ;; (not (lessp qvar lower)) ;; (lessp qvar upper)) ;; body)) (chk-new-name name t) (chk-arglist name args) (if (or (nvariablep qvar) (member-eq qvar args)) (er soft (qvar args) |The| |quantified| |variable| (!ppr qvar nil) |is| |supposed| |to| |be| |a| |variable| |that| |is| |not| |a| |member| |of| |the| |argument| |list| (!ppr args (quote |.|)))) ;; let's make sure these all translate before we even start (translate lower) (translate upper) (translate body) (let ((bdd-forall-sk-model-aux-name (pack (list name '-sk-model-aux))) (bdd-forall-sk-model-name (pack (list name '-sk-model))) (bdd-forall-model-aux-name (pack (list name '-model-aux))) (bdd-forall-model-name (pack (list name '-model))) (bdd-forall-model-aux-necc-name (pack (list name '-model-aux-necc))) (qvar** (pack (list qvar '**))) (bdd-forall-model-necc-name (pack (list name '-model-necc))) (bdd-forall-model-aux-suff-name (pack (list name '-model-aux-suff))) (bdd-forall-model-suff-name (pack (list name '-model-suff)))) (list (bdd-forall-sk-model-aux bdd-forall-sk-model-aux-name qvar upper args body) (bdd-forall-sk-model bdd-forall-sk-model-aux-name bdd-forall-sk-model-name lower args) (bdd-forall-model-aux bdd-forall-model-aux-name qvar upper args body) (bdd-forall-model bdd-forall-model-aux-name bdd-forall-model-name lower args) (bdd-forall-model-aux-necc bdd-forall-model-aux-necc-name bdd-forall-model-aux-name qvar qvar** upper args body) (bdd-forall-model-necc bdd-forall-model-necc-name bdd-forall-model-name bdd-forall-model-aux-necc-name qvar qvar** lower upper args body) (bdd-forall-model-aux-suff bdd-forall-model-aux-suff-name bdd-forall-sk-model-aux-name bdd-forall-model-aux-name qvar lower upper args body) (bdd-forall-model-suff bdd-forall-model-aux-suff-name bdd-forall-model-suff-name bdd-forall-sk-model-name bdd-forall-model-name qvar lower upper args body) (bdd-forall-defn-sk-constructive name bdd-forall-sk-model-name bdd-forall-model-necc-name bdd-forall-model-suff-name bdd-forall-model-name qvar lower upper args body)))) (defmacro bdd-forall (name qvar lower upper args body) `(do-events (bdd-forall-events ',name ',qvar ',lower ',upper ',args ',body))) REFERENCES 1. R. S. Boyer and J S. Moore, A Computational Logic, Academic Press, New York, 1979. 2. R. S. Boyer and J S. Moore, A Computational Logic Handbook, Academic Press, Boston, 1988. 3. Matt Kaufmann, ``A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover'', Technical Report 19, Computational Logic, Inc., May 1988. 4. M. Kaufmann, ``Addition of Free Variables to an Interactive Enchancement of the Boyer-Moore Theorem Prover'', Tech. report 42, Computational Logic, Inc., 1717 West Sixth Street, Suite 290 Austin, TX 78703, 1990. 5. Matt Kaufmann, ``An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification'', Journal of Automated Reasoning, (to appear), See also CLI Technical Report 43, May, 1989 for an expanded version 6. R.S. Boyer, D. Goldschlag, M. Kaufmann, J S. Moore, ``Functional Instantiation in First Order Logic'', Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7-26, Versions also published as CLI Technical Report 44 and in proceedings of the 1989 Workshop on Programming Logic, Programming Methodology Group, University of Goteborg, West Germany. 7. Matt Kaufmann, ``Skolemization Explained Simply'', Internal Note 27, Computational Logic, Inc., November 1987. 8. R. S. Boyer and J S. Moore, ``The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover'', Journal of Automated Reasoning, Vol. 4, No. 2, 1988, pp. 117-172. 9. R.S. Boyer, J S. Moore, ``A Theorem Prover for a Computational Logic'', Technical Report 54, Computational Logic, Inc., 1990, Published in proceedings of 10th International Conference on Automated Deduction, Kaiserslautern, West Germany, July 1990 Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . 1 2. Recognizing quantified notions. . . . . . . . . . . . 2 2.1. A sample use of CHECK-QUANT . . . . . . . . . . . 2 2.2. Precise description of CHECK-QUANT and theoretical justification . . . . . . . . . . . . 4 3. Generating quantified notions . . . . . . . . . . . . 7 3.1. DEFN-SK-CONSTRUCTIVE . . . . . . . . . . . . . . 7 3.2. BDD-FORALL . . . . . . . . . . . . . . . . . . . 10 Appendix A. Transcript from an execution of a BDD-FORALL form . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Appendix B. The Common Lisp code . . . . . . . . . . . . . . 18