Generalized resolution and cutting planes

This paper illustrates how the application of integer programming to logic can reveal parallels between logic and mathematics and lead to new algorithms for inference in knowledge-based systems. If logical clauses (stating that at least one of a set of literals is true) are written as inequalities, then the resolvent of two clauses corresponds to a certain cutting plane in integer programming. By properly enlarging the class of cutting planes to cover clauses that state that at least a specified number of literals are true, we obtain a generalization of resolution that involves both cancellation-type and circulant-type sums. We show its completeness by proving that it generates all prime implications, generalizing an early result by Quine. This leads to a cutting-plane algorithm as well as a generalized resolution algorithm for checking whether a set of propositions, perhaps representing a knowledge base, logically implies a given proposition. The paper is intended to be readable by persons with either an operations research or an artificial intelligence background.