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

What is behind PVS?

Hi there,

I am wondering what the underlying engine that makes the logical
derivations in PVS is. Is it a prolog-like resolution or BDD or a
combination of these two or even something else? Is there a good
source (say paper, survey, book) of the "logic behind PVS"?

Thanks in advance,