Event Detail

A formal system establishes a trinity between language, meaning, and inference. Many domains of thought can be captured using formal systems so that sound conclusions can be drawn through correct inferences. Philosophers have long speculated about machines that can distinguish sound arguments from flawed ones, and with modern computing, we can realize this dream to a significant extent. A research program to mechanize formal proof inevitably confronts a range of foundational and pragmatic choices. Should the foundations be classical or constructive, and should they be based on set theory, type theory, or category theory? What definitional principles should the language admit? How can formalizations be constructed from reusable modules? Should proofs be represented in a Hilbert calculus, natural deduction, or sequent calculus? Which inference steps in the proof calculus can and should be effectively mechanized in order to close the gap between informal arguments and their formal counterparts?

SRI’s Prototype Verification System (PVS) is an interactive proof assistant aimed at capturing the pragmatic features of mathematical expression and argumentation. The PVS language augments a simply typed higher-order logic with subtypes, dependent types, and algebraic datatypes. The PVS interactive proof checker integrates a number of decision procedures into the sequent calculus proof system. We examine the implications of these choices for the original goal of constructing mathematically sound arguments.