🚀 go-pugleaf

            Writing and Checking Proofs with PVS

            N. Shankar

            SRI Computer Science Lab

            Tuesday, March 31, 1992 at 2:30p.m. in AD-123

                                     COLLOQUIUM

                University at Albany - State University of New York

                            Computer Science Department

                                      ABSTRACT

                 PVS is a system for writing specifications and  constructing
            proofs.   It provides greater control in constructing proofs than
            an automatic theorem prover, and more theorem proving power  than
            a   low-level  proof  checker.   PVS  specifications  consist  of
            parameterized theories that are written in a  typed  higher-order
            logic  with  an  expressive  type system.  Proofs are constructed
            with a small collection of powerful inference steps that  include
            the  use  of  decision procedures and rewriting.  New patterns of
            inference steps can be added by  defining  proof  strategies.   A
            significant  aspect of PVS is the extent to which it exploits the
            synergy between the language constructs and the inference mechan-
            isms.   Theorem proving is employed in typechecking, and numerous
            features of the language, in turn, augment  the  theorem  proving
            capabilities.  PVS has so far been used to develop several proofs
            of nontrivial difficulty (e.g., the correctness of protocols  for
            Byzantine  agreement).   The talk will assume only a modest fami-
            liarity with logic and theorem proving, and will present an over-
            view of the design and use of PVS.