Logical inference and polyhedral projection

Abstract

We explore connections between polyhedral projection and inference in propositional logic. We formulate the problem of drawing all inferences that contain a restricted set of atoms (i.e., all inferences that pertain to a given question) as a logical projection problem. We show that polyhedral projection partially solves this problem and in particular derives precisely those inferences that can be obtained by a certain form of unit resolution. We prove that this unit resolution algorithm is exponential in the number of atoms in the restricted set but is polynomial in the problem size when this number of fixed. We also survey a number of new satisfiability algorithms that have been suggested by the polyhedral interpretation of propositional logic.