FME+LICS+RTA invited talk: Little engines of proof
Monday July 22nd 08:55-09:55 in auditorium 1
The automated construction of mathematical proof is a basic activity in computing. Since the dawn of the field of automated reasoning, there have been two divergent schools of thought. One school, best represented by Alan Robinson's resolution method, is based on simple uniform proof search procedures guided by heuristics. The other school, pioneered by Hao Wang, argues for problem-specific combinations of decision and semi-decision procedures. While the former school has been dominant in the past, the latter approach has greater promise. In recent years, several high quality inference engines have been developed, including propositional satisfiability solvers, ground decision procedures for equality and arithmetic, quantifier elimination procedures for integers and reals, and abstraction methods for finitely approximating problems over infinite domains. We describe some of these "little engines of proof" and a few of the ways in which they can be combined. We focus in particular on the combination ground decision procedures and their use in automated verification. We conclude by arguing for a modern reinterpretation and reappraisal of Hao Wang's hitherto neglected ideas on inferential analysis.
About Natarajan Shankar
Dr. Natarajan Shankar has been a Staff Scientist at the SRI Computer Science Laboratory since 1989. He received his Ph.D. degree in computer science under the supervision of Robert Boyer and J Moore from the University of Texas at Austin in 1986. From 1986 to 1988, he served as a research associate at Stanford University.
Dr. Shankar's interests are in the study of formal methods for the specification and verification of hardware and software, in automated deduction, and in computational logic. In his dissertation, he employed the Boyer-Moore theorem prover to check proofs of various metamathematical theorems, including Gödel's incompleteness theorem and the Church-Rosser theorem. His book Metamathematics, Machines, and Gödel's Proof was published by Cambridge University Press in 1994. He has also contributed to the foundation of linear logic and to the theory of proof search in nonclassical logics.
Dr. Shankar co-developed the design and implementation of the PVS verification system and has written and lectured extensively on it. The PVS system is widely acknowledged as the leading computer-aided theorem proving system in widespread academic and industrial use for software and hardware verification.
Dr. Shankar has applied PVS extensively, to the verification of hardware, self-stabilization, and to distributed and real-time systems. He has explored the integration and use of BDDs and symbolic model checking in PVS and has examined the use of PVS as a semantic framework for embedding and combining different formalisms. He helped develop a combination of model-checking and theorem proving through the automatic construction of invariants and property preserving abstractions. Recently he defined and implemented an efficient evaluator for an executable fragment of PVS that employs safe destructive updates.
Dr. Shankar is currently leading the SAL (Symbolic Analysis Laboratory) project in collaboration with Professor David Dill of Stanford University. He is also participating in an initiative to develop www.QPQ.org, a peer-reviewed open source repository for deductive software components.