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

[PVS-Help] Proof By Contradition - How to do this in PVS?



Title: Proof By Contradition - How to do this in PVS?

I'm trying to reconstruct a manual proof that used proof by contradition, i.e assume the negation of your thesis and then derive a contradition.

It's not clear to me how to accomplish this in the PVS prover.  Any suggestions would be most welcome.

Thanks - Mark Janney