Logic in Computer Science (LICS 2002)

Invited Talk: Little Engines of Proof (at LICS 2002)

Authors: Natarajan Shankar

Abstract

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.

BibTeX

  @InProceedings{Shankar-LittleEnginesofProo,
    author = 	 {Natarajan Shankar},
    title = 	 {Little Engines of Proof},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    pages =      {3--},
    location =   {Copenhagen, Denmark}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }