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

Re: can you give me command to prove test??




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.