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

Re: Two trivial questions during proof..



Tae Ho,

a sequent of the form

   test1 :

   {-1}    TRUE
     |-------

requires you to proof FALSE from TRUE, i.e. a contradiction. This
indicates that either your ``theorem'' is not valid, or you made some
wrong decisions during the proof. 

In the case of theorem ``test1'' the latter applies: (GRIND) is not able
to find the right instantiations for ``y''. You can tell GRIND to use
all possible instantiations by adding the keyword argument :IF-MATCH
ALL. Thus,
(GRIND :IF-MATCH ALL) proves ``test1''.

Your second theorem ``test2'' is, however, NOT provable, since
``Julian'' doesn't occur in ``loveset''. If ``Julian'' is removed from
the type ``person'' the theorem ``test2'' can be proved by induction on
``x'' and using GRIND on every subgoal:

   (then (induct "x") (repeat (grind :if-match all)))


Greetings,

	- Holger


Tae Ho Kim wrote:
> 
> Hi. PVS users.
> 
> I'm sorry for asking the trivial questions.
> 
> I specified
> 'every boy loves some persons' (theorem test1)
> 'every person loves some persons or is loved by' (theorem test2)
> and I tried to prove it.
> 
> But I cannot advance after I met this proof node by (grind)
> 
> test1 :
> 
> {-1}    TRUE
>   |-------
> 
> How can I prove theorem test1 and test2.
> 
> lovetheory:THEORY
>   BEGIN
>   person: TYPE = {John, Tom, Alice, Mary, Julian}
>   boyset: setof[person] = { x: person |
>                  x = John or
>                  x = Tom }
>   boy: TYPE = (boyset)
>   love: TYPE = [person,person]
>   loveset : setof[love]  = {loverel:love |
>                loverel = (Tom, Alice) or
>                loverel = (John, Mary) or
>                loverel = (John, Alice) }
> 
>   test1: THEOREM FORALL (x:boy): EXISTS (y:person):
>                member((x,y),loveset)
> 
>   test2: THEOREM FORALL (x:person): EXISTS (y:person):
>                (member((x,y),loveset) OR member((y,x),loveset))
> 
> END lovetheory
> 
> --
> Kim, Tae-ho
> thkim@salmosa.kaist.ac.kr
> http://salmosa.kaist.ac.kr/~thkim

-- 
-----------------------------------------------------------------------
Holger Pfeifer                               Tel.: (+49) 731 / 502-4124
Abteilung KI                                  Fax: (+49) 731 / 502-4119
Universitšt Ulm
D-89069 Ulm                    e-mail: pfeifer@ki.informatik.uni-ulm.de
-----------------------------------------------------------------------