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

Two trivial questions during proof..



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