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

*To*: Tae Ho Kim <thkim@salmosa.kaist.ac.kr>*Subject*: Re: Two trivial questions during proof..*From*: Holger Pfeifer <pfeifer@ares.informatik.uni-ulm.de>*Date*: Wed, 27 Aug 1997 16:25:03 +0200*Cc*: pvs-help@csl.sri.com*Organization*: Universität Ulm, Abteilung Künstliche Intelligenz*References*: <199708271344.WAA03488@hydra.kaist.ac.kr>*Sender*: pfeifer@ares.informatik.uni-ulm.de

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 -----------------------------------------------------------------------

**References**:**Two trivial questions during proof..***From:*Tae Ho Kim <thkim@salmosa.kaist.ac.kr>

- Prev by Date:
**Two trivial questions during proof..** - Next by Date:
**Instantiating datatypes with subtype of nat** - Prev by thread:
**Two trivial questions during proof..** - Next by thread:
**Questions on conversion/coercion.** - Index(es):