[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
A question from KAIST
I have a question about a proof with PVS.
Reading a paper on PVS proof, I found that using TABLE makes it easy to prove IF-THEN rules.
But, I am very interested in proving IF-THEN-ELSE rules themselves.
I have tried it, but no TCC's are generated. So, I can not check for completeness or consistency, etc.
Do you have any idea for this problem?
Please respond to me.
Best regards, Han Seong.