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, Jordan