[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Kellom{ki Pertti <pk@cs.tut.fi>*Subject*: Re: Instantiation hints*From*: Sam Owre <owre@csl.sri.com>*Date*: Wed, 07 Feb 2001 12:42:47 -0800*cc*: pvs@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "Thu, 01 Feb 2001 08:33:10 +0200." <200102010633.IAA01103@arokyyhky.cs.tut.fi>*Sender*: pvs-owner@csl.sri.com

> Date: Thu, 1 Feb 2001 08:33:10 +0200 (EET) > From: Kellom{ki Pertti <pk@cs.tut.fi> > To: pvs@csl.sri.com > Subject: Instantiation hints > > I have to prove a number of theorems of the form > > (exists(a,b,c,...) : P(a,b,c,...)) => (exists(a,b,c,...) : Q(a,b,c,...)) > > where P=>Q is trivial once I get rid of the quantifications. The order > of the quantified variables may not be the same in the two > quantifications, but they have the same variables. > > Is there a way to tell PVS that it should instantiate "a" with "a!1", > "b" with "b!1" etc.? > -- > Pertti Hi Pertti, I decided to start writing a strategy that does this, mostly to illustrate how this could be done in PVS. It isn't robust, in that it will choose randomly if there are a number of skolem constants with the same prefix, e.g., a!1, a!2, ... This is because collect-skolem-constants gets the constants from a hash table. A better heuristic would probably use the larger suffixes, as they are the more recently introduced skolem constants. In addition, this strategy becomes a (SKIP) if any of the bound variable fail to match; you might want to use "_" as the value instead, so that it will do a partial instantiation instead - you could even put this on a flag. There are undoubtedly other ways that this could be improved. I'll let you make these adjustments since you know what you actually need. Regards, Sam Owre ---------Add to ~/pvs-strategies---------- (defstep inst-by-skolem-names (fnum) (let ((sformnum (find-sform (s-forms (current-goal *ps*)) fnum #'(lambda (sform) (if (negation? (formula sform)) (check-inst-quant (args1 (formula sform)) nil nil) (check-inst-quant (formula sform) nil T))))) (newterms (get-corresponding-skolem-constants sformnum)) (inst-cmd `(inst ,sformnum ,@newterms))) (if newterms inst-cmd (skip))) "Instantiates from available skolem constants with the 'same' name." "Instantiating from skolem constants") ;; Get the skolem constants corresponding to the bound variables in ;; formula sformnum (defun get-corresponding-skolem-constants (sformnum) (let* ((sforms (select-seq (s-forms (current-goal *ps*)) (list sformnum))) (sform (when sforms (car sforms))) (fmla (when sforms (formula sform))) (boundvars (when sforms (if (forall-expr? fmla) (bindings (args1 fmla)) (bindings fmla))))) (find-matching-skolem-names boundvars))) ;; Find a set of skolem constants with names matching the boundvars ;; If any boundvar fails to be matched, return nil. (defun find-matching-skolem-names (boundvars) (find-matching-skolem-names* boundvars (collect-skolem-constants) nil)) (defun find-matching-skolem-names* (boundvars skoconsts skolem-names) (if (null boundvars) (nreverse skolem-names) (let ((skoconst (find (id (car boundvars)) skoconsts :test #'matching-skolem-id :key #'id))) (when skoconst (find-matching-skolem-names* (cdr boundvars) skoconsts (cons (mk-name-expr (id skoconst) nil nil (mk-resolution skoconst (current-theory-name) (type skoconst))) skolem-names)))))) (defun matching-skolem-id (bound-id skolem-id) (or (eq bound-id skolem-id) (eq bound-id (sko-symbol-prefix skolem-id))))

**Follow-Ups**:**Re: Instantiation hints***From:*Kellomaki Pertti <pk@cs.tut.fi>

**References**:**Instantiation hints***From:*Kellom{ki Pertti <pk@cs.tut.fi>

- Prev by Date:
**Instantiations** - Next by Date:
**Re: Instantiation hints** - Prev by thread:
**Instantiation hints** - Next by thread:
**Re: Instantiation hints** - Index(es):