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

*To*: Xiao Han <moshimaru@xxxxxxxxx>*Subject*: Re: [PVS-Help] Ask for help on a proof*From*: Jerome <jerome@xxxxxxxxxxxxxx>*Date*: Tue, 20 May 2008 08:20:55 -0700*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <4548705a0805160325j184f8619t44e8269f60017cdf@mail.gmail.com>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-agent*: Mutt/1.4.1i

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.

- Prev by Date:
**Re: [PVS-Help] Non empty finite set induction** - Next by Date:
**Re: [PVS-Help] Ask for help on a proof** - Prev by thread:
**[PVS-Help] Ask for help on a proof** - Next by thread:
**Re: [PVS-Help] Ask for help on a proof** - Index(es):