A quantitative approach to logical inference

摘要

Logical inference is of central importance in the information and decision sciences but presents a very hard computational problem. Since the traditional symbolic inference methods have had limited success on large knowledge bases, this papers investigates a quantitative approach. It surveys the application of integer programming methods to inference problems in propositional logic. It displays a number of remarkable parallels between logic and mathematics and shows that these can lead to fast inference methods, both quantitative and symbolic. In particular it explains why the logical concepts of resolution, extended resolution, input and unit refutation, the Davis-Putnam procedure, and drawing of inferences pertinent to a given topic are closely related to the mathematical concepts of cutting planes, Chvátal's method, elementary closure, branch and bound, and projection of a polytope, respectively. Much of the paper should be intelligible to persons with limited background in logic and mathematical programming, but recent mathematical results are stated precisely.