Inference systems for logical algorithms

Abstract

Logical algorithms are defined in terms of individual computation steps that are based on logical inferences. We present a uniform framework for formalizing logical algorithms based on inference systems. We present inference systems for algorithms such as resolution, the Davis-Putnam-Logemann-Loveland procedure, equivalence and congruence closure, and satisfiability modulo theories. The paper is intended as an introduction to the use of inference systems for studying logical algorithms. © Springer-Verlag Berlin Heidelberg 2005.