Talks & Seminars
Little Engines of Proof
Natarajan Shankar, SRI,Computer Science Laboratory
Date & Time: January 3, 2003 11:30
Venue: CSE Seminar Hall
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 over 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.
Speaker Profile:
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback