Logical Algorithms
Natarajan Shankar (SRI International)
- Place: E2, Rm 392
- Time: 2-3:10pm, Wednesday, February 15, 2006
Abstract
In a logical algorithm, each individual computation step is an application of an inference rule. 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 talk is intended as an introduction to the use of inference systems for studying logical algorithms.