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

I would like to know the simpler way to prove.



Hi. PVS users.  

I would like to know the simple command without instantiation. 

I proved THEOREM group1check,  group3check, group2check with (inst ) 

command. But, I would like to know the automatic way to prove these 

theorem. How can I do it?  


 
love : THEORY

BEGIN
 
persontype : TYPE = {g1_p1, g1_p2,  g2_p2, g2_p3, 
  g2_p4, g3_p1, g3_p2} 

group1set : setof[persontype] = {x : persontype |
  x =  g1_p1 OR  x = g1_p2} 
group1type : TYPE = (group1set) 

group3set : setof[persontype] = {x : persontype | 
  x =  g3_p1 OR x = g3_p2} 
group3type : TYPE = (group3set) 

group2set : setof[persontype] = {x : persontype |  
  x = g2_p2 OR x = g2_p4 OR x = g2_p3} 
group2type : TYPE = (group2set) 

love : TYPE = [persontype, persontype] 
loveset : setof[love]= { ele : love |  
  ele = (g1_p1, g2_p2) OR ele = (g1_p2, g2_p4) OR  
  ele = (g2_p2, g2_p3) OR ele = (g2_p2, g2_p4) OR 
  ele = (g2_p4, g2_p3) OR ele = (g2_p4, g3_p2) OR
  ele = (g2_p3, g3_p1) } 
lovetype :  TYPE = (loveset) 

group1check: THEOREM FORALL (a1 : group1type):  
  EXISTS (a2 : group2type): member((a1,a2),loveset) 
%(grind :if-match nil)(inst 1 "g2_p2")(inst 1 "g2_p4")

group3check: THEOREM FORALL (a1 : group3type):  
  EXISTS (a2 : group2type): member((a2,a1),loveset) 
%(grind :if-match nil)(inst 1 "g2_p3")(inst 1 "g2_p4")

group2check: THEOREM FORALL (a1: group2type): 
  EXISTS (a2 : persontype): EXISTS (a3:persontype): 
  member((a2,a1), loveset) AND 
  member((a1,a3), loveset)
%(grind :if-match nil)(inst 1 "g1_p1" "g2_p3")(assert)(inst 1 "g1_p2" "g2_p3")(assert) (inst 1 "g2_p2" "g3_p1")(assert)


END love 
 

-- 
Kim, Tae-ho
thkim@salmosa.kaist.ac.kr
http://salmosa.kaist.ac.kr/~thkim