计算逻辑约束：理论与应用

1 Constraints and Constraint Solving: An Introduction
　1.1 Introduction
　1.2 A First Approach to Constraint Based Calculi
　1.3 A Case Study of a Constraint System: Feature Constraints
　1.4 Programming with Incomplete Constraint Solvers
　1.5 Committed Choice: A More Realistic Approach
2 Constraint Solving on Terms
　2.1 Introduction
　2.2 The Principle of Syntactic Methods
　2.3 Unification Problems
　2.4 Dis-Unification Problems
　2.5 Ordering Constraints
　2.6 Matching Constraints
　2.7 Principles of Automata Based Constraint Solving
　2.8 Presburger Arithmetic and Classical Word Automata
　2.9 Typing Constraints and Tree Automata
　2.10 Set Constraints and Tree Set Automata
　2.11 Examples of Other Constraint Systems Using Tree Automata
3 Combining Constraint Solving
　3.1 Introduction
　3.2 Classification of Constraint Systems and Combination Approaches
　3.3 The Nelson-Oppen Combination Procedure
　3.4 Combination of E-Unification Algorithms
　3.5 The Logical and Algebraic Perspective
　3.6 Generalizations
　3.7 Optimization and Complexity Issues
　3.8 Open Problems
4 Constraints and Theorem Proving
　4.1 Introduction
　4.2 Equality Clauses
　4.3 The Purely Equational Case: Rewriting and Completion
　4.4 Superposition for General Clauses
　4.5 Saturation Procedures
　4.6 Paramodulation with Constrained Clauses
　4.7 Paramodulation with Built-in Equational Theories
　4.8 Effective Saturation of First-Order Theories
5 Functional and Constraint Logic Programming
　5.1 Introduction
　5.2 A Rewriting Logic for Declarative Programming
　5.3 Higher-Order Programming
　5.4 Constraint Programming
　5.5 Conclusions
6 Building Industrial Applications with Constraint Programming
　6.1 Introduction
　6.2 Constraint Programming
　6.3 The CHIP System
　6.4 Application Studies
　6.5 Industrial Applications
　6.6 Case Studies
　6.7 Application Framework
　6.8 Analysis
　6.9 Does CLP Deliver?
　6.10 Limitations
　6.11 Future Trends
　6.12 Conclusions