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

*To*: pvs-help@csl.sri.com*Subject*: ?s about the quant rule, etc.*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Mon, 13 Jul 1998 10:23:31 -0400 (EDT)*Cc*: aronsz@csee.wvu.edu

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

- Prev by Date:
**library for 'reals'** - Next by Date:
**? about the quant rule** - Prev by thread:
**Re: ? about the quant rule** - Next by thread:
**library for 'reals'** - Index(es):