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

?s about the quant rule, etc.



I have one specific question right now about the quant rule; then I
have a more general question...

More general first:  I am new to PVS.  I've been raised using Natural
Deduction systems in logic (like Kalish & Montague's box & cancel
style).  I'm finding it hard to shift over to the sequent calculus
used in PVS.  Is there anyone out there who could give some help
specific to this predicament, someone who's familiar with both styles?
And maybe there's a good reference--a textbook, or PVS document--that
would be helpful?

The specific question has arisen in a proof I'm trying to construct.
I need to prove two sets (two unions) are identical, so I invoked
extensionality for sets.  Then I wanted to instantiate the axiom for
the two unions that I want to prove identical.  I introduced names,
'a' and 'b' for the two union expressions with

(name "a" "union(foo)")

(name "b" "union(bar)")

This worked fine.  I then wanted instantiate putting "a" and "b" in
for the two set variables in the set extensionality axiom.  So I used

(quant -3 ("a" "b"))

As far as I can tell this is the precise syntax required for the rule,
but I get an "ill-formed rule/strategy" message with no change...

Can anyone tell me what's wrong here?  THanks in advance for any help
on either question.

Mark Aronszajn