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

*To*: Jerome <jerome@xxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Ask for help on a proof*From*: Cesar Munoz <munoz@xxxxxxxxxx>*Date*: Tue, 20 May 2008 15:43:57 -0400*Cc*: pvs-help@xxxxxxxxxxx, Xiao Han <moshimaru@xxxxxxxxx>*In-reply-to*: <20080520152055.GB8966@cs.caltech.edu>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <4548705a0805160325j184f8619t44e8269f60017cdf@mail.gmail.com> <20080520152055.GB8966@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Thunderbird 1.5.0.14ubu (X11/20080505)

Actually, you don't have to declare the axioms. In your original specification, you have to issue the command (typepred "er") to get the reflexive, symmetric, and transitive properties for "er". Notice that those properties are declared in the type of "er". Cesar Jerome wrote: > If you can take the reflexive, symmetric, and transitive properties as > axioms, you should declare them as such (after your predicate > declarations): > > reflexive: AXIOM reflexive?(R) > symmetric: AXIOM symmetric?(R) > transitive: AXIOM transitive?(R) > > This way, in your proof, you can use them as in (LEMMA ...) and/or > (REWRITE ...) rules. For example: > > Rule? (LEMMA "symmetric") > ... > Rule? (INST?) > ... > > jerome > > On Fri, May 16, 2008 at 06:25:56PM +0800, Xiao Han wrote: >> Hi there, >> I am new to PVS. I am working on an assignment about using PVS to prove >> a theorem. >> Equivalence relations satisfy the following axioms: reflexive, symmetric >> and transitive. Here equivalence relations are denoted by ???. >> The theorem is >> >> forall x and y, ¬x???y ??? (forall z, x???z???¬y???z ) >> >> I wrote the specification as follows: >> >> relations[t: TYPE] : THEORY >> BEGIN >> x, y, z: VAR t >> R : VAR PRED[[t,t]] >> >> reflexive?(R): bool = (FORALL x: R(x, x)) >> symmetric?(R): bool = (FORALL x, y:R(x, y) IMPLIES R(y, x)) >> transitive?(R): bool = >> (FORALL x, y, z: R(x, y) AND R(y, z) IMPLIES R(x, z)) >> >> equivalent_relation?(R): bool = >> reflexive?(R) AND symmetric?(R) AND transitive?(R) >> er: (equivalent_relation?[[t,t]]) >> >> TODO: CONJECTURE ( FORALL (x: t), (y: t): NOT er(x, y) IMPLIES ( FORALL >> (z: t): er(x, z) IMPLIES er(y, z) ) ) >> END relations >> >> After using (grind) I got >> >> TODO : >> >> |------- >> {1} (FORALL (x: t), (y: t): >> NOT er(x, y) IMPLIES >> (FORALL (z: t): er(x, z) IMPLIES NOT er(y, z))) >> >> Rule? (grind) >> Trying repeated skolemization, instantiation, and if-lifting, >> this simplifies to: >> TODO : >> >> {-1} er(x!1, z!1) >> {-2} er(y!1, z!1) >> |------- >> {1} er(x!1, y!1) >> >> Rule? >> >> I should use the symmetric axiom to continue the proof but I do not know >> how: >> >> Rule? (use "symmetric?") >> Using lemma symmetric?, >> this simplifies to: >> TODO : >> >> {-1} symmetric? = (LAMBDA (R): (FORALL x, y: R(x, y) IMPLIES R(y, x))) >> [-2] er(x!1, z!1) >> [-3] er(y!1, z!1) >> |------- >> [1] er(x!1, y!1) >> >> Is it correct to use a lemma? If so, what to do next? >> >> Many thanks. > > -- Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@xxxxxxxxxx National Institute of Aerospace mailto:Cesar.A.Munoz@xxxxxxxx 100 Exploration Way Room 214 http://research.nianet.org/~munoz Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988 GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6 1A18 6000 89F5 C114 E6C4

- Prev by Date:
**Re: [PVS-Help] Ask for help on a proof** - Next by Date:
**[PVS-Help] simple state machine with access list** - Prev by thread:
**Re: [PVS-Help] Ask for help on a proof** - Next by thread:
**Re: [PVS-Help] Ask for help on a proof** - Index(es):