Sciweavers

LICS
2002
IEEE

Little Engines of Proof

13 years 8 months ago
Little Engines of Proof
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 s, 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 o...
Natarajan Shankar
Added 15 Jul 2010
Updated 15 Jul 2010
Type Conference
Year 2002
Where LICS
Authors Natarajan Shankar
Comments (0)