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

*To*: pvs-help@csl.sri.com*Subject*: Two trivial questions during proof..*From*: Tae Ho Kim <thkim@salmosa.kaist.ac.kr>*Date*: Wed, 27 Aug 1997 22:44:26 +0900 (KST)

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

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