Inference Systems for Logical Algorithms

摘要

Logical algorithms are denned 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.