Optimization Methods for Logical Inference

by Chandru, Vijay; Hooker, John

• ISBN13: 9780471570356
• ISBN10: 0471570354
• Edition: 1st
• Format: Hardcover
• Copyright: 1999-03-30
• Publisher: Wiley-Interscience

Summary

Merging logic and mathematics in deductive inference-an innovative, cutting-edge approach. Optimization methods for logical inference? Absolutely, say Vijay Chandru and John Hooker, two major contributors to this rapidly expanding field. And even though "solving logical inference problems with optimization methods may seem a bit like eating sauerkraut with chopsticks. . . it is the mathematical structure of a problem that determines whether an optimization model can help solve it, not the context in which the problem occurs." Presenting powerful, proven optimization techniques for logic inference problems, Chandru and Hooker show how optimization models can be used not only to solve problems in artificial intelligence and mathematical programming, but also have tremendous application in complex systems in general. They survey most of the recent research from the past decade in logic/optimization interfaces, incorporate some of their own results, and emphasize the types of logic most receptive to optimization methods-propositional logic, first order predicate logic, probabilistic and related logics, logics that combine evidence such as Dempster-Shafer theory, rule systems with confidence factors, and constraint logic programming systems. Requiring no background in logic and clearly explaining all topics from the ground up, Optimization Methods for Logical Inference is an invaluable guide for scientists and students in diverse fields, including operations research, computer science, artificial intelligence, decision support systems, and engineering.

Author Biography

VIJAY CHANDRU is a professor in the Computer Science and Automation Department at the Indian Institute of Science in Bangalore, India.<br> <br> . HOOKER is a professor in the Graduate School of Industrial Administration at Carnegie Mellon University.

Table of Contents

Preface	xiii
Introduction	1	(10)
Logic and Mathematics: The Twain Shall Meet	3	(3)
Inference Methods for Logic Models	6	(1)
Logic Modeling Meets Mathematical Modeling	7	(1)
The Difficulty of Inference	8	(3)
Propositional Logic: Special Cases	11	(86)
Basic Concepts of Propositional Logic	13	(10)
Formulas	13	(3)
Normal Forms	16	(6)
Rules	22	(1)
Integer Programming Models	23	(8)
Optimization and Inference	25	(2)
The Linear Programming Relaxation	27	(4)
Horn Polytopes	31	(10)
Horn Resolution	31	(3)
The Integer Least Element of a Horn Polytope	34	(3)
Dual Integrality of Horn Polytopes	37	(4)
Quadratic and Renamable Horn Systems	41	(14)
Satisfiability of Quadratic Systems	42	(2)
The Median Characteristic of Quadratic Systems	44	(1)
Recognizing Renamable Horn Systems	45	(8)
Q-Horn Propositions	53	(2)
Nested Clause Systems	55	(8)
Nested Propositions: Definition and Recognition	55	(3)
Maximum Satisfiability of Nested Clause Systems	58	(3)
Extended Nested Clause Systems	61	(2)
Extended Horn Systems	63	(13)
The Rounding Theorem	65	(4)
Satisfiability of Extended Horn Systems	69	(1)
Verifying Renamable Extended Horn Systems	70	(1)
The Unit Resolution Property	71	(2)
Extended Horn Rule Bases	73	(3)
Problems with Integral Polytopes	76	(11)
Balanced Problems	78	(3)
Integrality and Resolution	81	(6)
Limited Backtracking	87	(10)
Maximum Embedded Renamable Horn Systems	89	(2)
Hierarchies of Satisfiability Problems	91	(3)
Generalized and Split Horn Systems	94	(3)
Propositional Logic: The General Case	97	(106)
Two Classic Inference Methods	98	(11)
Resolution for Propositional Logic	99	(2)
A Simple Branching Procedure	101	(2)
Branching Rules	103	(1)
Implementation of a Branching Algorithm	104	(2)
Incremental Satisfiability	106	(3)
Generating Hard Problems	109	(7)
Pigeonhole Problems	110	(1)
Problems Based on Graphs	111	(2)
Random Problems Hard for Resolution	113	(1)
Random Problems Hard for Branching	114	(2)
Branching Methods	116	(7)
Branch and Bound	117	(4)
Jeroslow-Wang Method	121	(1)
Horn Relaxation Method	122	(1)
Bounded Resolution Method	123	(1)
Tableau Methods	123	(10)
The Simplex Method in Tableau Form	124	(4)
Pivot and Complement	128	(3)
Column Subtraction	131	(2)
Cutting Plane Methods	133	(17)
Resolvents as Cutting Planes	134	(2)
Unit Resolution and Rank 1 Cuts	136	(7)
A Separation Algorithm for Rank 1 Cuts	143	(1)
A Branch-and-Cut Algorithm	144	(4)
Extended Resolution and Cutting Planes	148	(2)
Resolution for 0-1 Inequalities	150	(9)
Inequalities as Logical Formulas	153	(1)
A Generalized Resolution Algorithm	154	(3)
Some Examples	157	(2)
A Set-Covering Formulation with Facet Cuts	159	(14)
The Set-Covering Formulation	160	(4)
Elementary Facets of Satisfiability	164	(2)
Resolvent Facets Are Prime Implications	166	(5)
A Lifting Technique for General Facets	171	(2)
A Nonlinear Programming Approach	173	(4)
Formulation as a Nonlinear Programming Problem	174	(1)
An Interior Point Algorithm	175	(1)
A Satisfiability Heuristic	176	(1)
Tautology Checking in Logic Circuits	177	(12)
The Tautology Checking Problem	177	(2)
Solution by Benders Decomposition	179	(3)
Logical Interpretation of the Benders Algorithm	182	(3)
A Nonnumeric Algorithm	185	(3)
Implementation Issues	188	(1)
Inference as Projection	189	(10)
The Logical Projection Problem	191	(1)
Computing Logical Projections by Resolution	191	(2)
Projecting Horn Clauses	193	(1)
The Polyhedral Projection Problem	193	(2)
Inference by Polyhedral Projection	195	(1)
Resolution and Fourier-Motzkin Elimination	196	(1)
Unit Resolution and Polyhedral Projection	197	(1)
Complexity of Inference by Polyhedral Projection	198	(1)
Other Approaches	199	(4)
Probabilistic and Related Logics	203	(64)
Probabilistic Logic	205	(13)
A Linear Programming Model	206	(3)
Sensitivity Analysis	209	(2)
Column Generation Techniques	211	(5)
Point Values Versus Intervals	216	(2)
Bayesian Logic	218	(17)
Possible World Semantics for Bayesian Networks	220	(4)
Using Column Generation with Benders Decomposition	224	(3)
Limiting the Number of Independence Constraints	227	(8)
Dempster-Shafer Theory	235	(15)
Basic Ideas of Dempster-Shafer Theory	236	(3)
A Linear Model of Belief Functions	239	(1)
A Set-Covering Model for Dempster's Combination Rule	240	(4)
Incomplete Belief Functions	244	(2)
Dempster-Shafer Theory vs. Probabilistic Logic	246	(2)
A Modification of Dempster's Combination Rule	248	(2)
Confidence Factors in Rule Systems	250	(17)
Confidence Factors	251	(3)
A Graphical Model of Confidence Factor Calculation	254	(5)
Jeroslow's Representability Theorem	259	(3)
A Mixed Integer Model for Confidence Factors	262	(5)
Predicate Logic	267	(40)
Basic Concepts of Predicate Logic	269	(6)
Formulas	269	(1)
Interpretations	270	(1)
Skolem Normal Form	271	(3)
Herbrand's Theorem	274	(1)
Partial Instantiation Methods	275	(12)
Partial Instantiation	276	(2)
A Primal Approach to Avoiding Blockage	278	(6)
A Dual Approach to Avoiding Blockage	284	(3)
A Method Based on Hypergraphs	287	(8)
A Hypergraph Model for Propositional Logic	288	(2)
Shortest Paths in B-Graphs	290	(1)
Extension to Universally Quantified Logic	290	(5)
Answering Queries	295	(1)
An Infinite 0-1 Programming Model	295	(6)
Infinite Dimensional 0-1 Programming	296	(1)
A Compactness Theorem	297	(1)
Herbrand Theory and Infinite 0-1 Programs	298	(1)
Minimum Solutions	299	(2)
The Logic of Arithmetic	301	(6)
Decision Methods for Arithmetic	301	(1)
Quantitative Methods for Presburger Real Arithmetic	302	(2)
Quantitative Methods for Presburger (Integer) Arithmetic	304	(3)
Nonclassical and Many-Valued Logics	307	(18)
Nonmonotonic Logics	308	(3)
Many-Valued Logics	311	(3)
Modal Logics	314	(2)
Constraint Logic Programming	316	(9)
Some Definitions	318	(1)
The Embedding	319	(2)
Infinite Linear Programs	321	(2)
Infinite 0-1 Mixed Integer Programs	323	(2)
Appendix. Linear Programming	325	(1)
Polyhedral Cones	325	(1)
Convex Polyhedra	326	(4)
Optimization and Dual Linear Programs	330	(1)
Complexity of Linear Programming	331	(2)
Bibliography	333	(25)
Index	358