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

A question from KAIST

Dear pvs-help:

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.

Do you have any idea for this problem?

Please respond to me.

Thank you.

Best regards, Han Seong.