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

Re: [PVS-Help] Ask for help on a proof



Thank you all, friends.  I have completed the proof by using (typepred "er") and (assert) command.  Your suggestion is of great help to me.

2008/5/21 Cesar Munoz <munoz@xxxxxxxxxx>:
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