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

*To*: chao qin <Chao.Qin@loria.fr>*Subject*: Re: can you give me command to prove test??*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Sun, 06 Jul 2003 23:43:48 -0700*cc*: pvs-help@csl.sri.com*In-Reply-To*: Message from chao qin <Chao.Qin@loria.fr> of "Sat, 05 Jul 2003 17:32:26 +0200." <3F06EF8A.7050108@loria.fr>*Sender*: pvs-help-owner@csl.sri.com

Chao Qin: I've attached a proof. The typepred step is needed to expose the type constraint implicit in the type for b!1, and inst? instantiates the quantifier in the type predicate. The grind command does make use of type constraints as far as asserting them to the decision procedures, but it does not instantiate quantifiers in the constraints. This is why it fails. (grind) also fails when employed after the typepred because it needlessly expands is_finite and does a poor job of instantiating the resulting quantifiers. The more refined (grind :defs nil) does complete the proof, but inst? is a simpler alternative. -Shankar test : |------- {1} FORALL (a: set1, b: set2): subset?(b, a) Rule? (skosimp*) Repeatedly Skolemizing and flattening, this simplifies to: test : |------- {1} subset?(b!1, a!1) Rule? (typepred "b!1") Adding type constraints for b!1, this simplifies to: test : {-1} is_finite[T](b!1) {-2} FORALL (s: set1): subset?(b!1, s) |------- [1] subset?(b!1, a!1) Rule? (inst?) Found substitution: s: set1 gets a!1, Using template: subset?(b!1, s) Instantiating quantified variables, Q.E.D.

**References**:**can you give me command to prove test??***From:*chao qin <Chao.Qin@loria.fr>

- Prev by Date:
**can you give me command to prove test??** - Next by Date:
**pb with measure in a recursive function** - Prev by thread:
**can you give me command to prove test??** - Next by thread:
**Re: can you give me command to prove test??** - Index(es):