Constraints in computational logics(计算逻辑约束：理论与应用)

Constraints provide a declarative way of representing infinite sets of data. They are well suited for combining different logical or programming paradigms as has been known for constraint logic programming since the 1980s and more recently for functional programming. The use of constraints in automated deduction is more recent and has proved to be very successful, moving the control from the meta-level to the constraints, which are now first-class objects.This monograph-like book presents six thoroughly reviewed and revised lectures given by leading researchers at the summer school organized by the ESPRIT CCL Working Group in Gif-sur-Yvette, France, in September 1999. The book offers coherently written chapters on constraints and constraint solving, constraint solving on terms, combining constraint solving, constraints and theorem proving, functional and constraint logic programming, and building industrial applications.

在线阅读本书

Constraints provide a declarative way of representing infinite sets of data. They are well suited for combining different logical or programming paradigms as has been known for constraint logic programming since the 1980s and more recently for functional programming. The use of constraints in automated deduction is more recent and has proved to be very successful, moving the control from the meta-level to the constraints, which are now first-class objects.This monograph-like book presents six thoroughly reviewed and revised lectures given by leading researchers at the summer school organized by the ESPRIT CCL Working Group in Gif-sur-Yvette, France, in September 1999. The book offers coherently written chapters on constraints and constraint solving, constraint solving on terms, combining constraint solving, constraints and theorem proving, functional and constraint logic programming, and building industrial applications.

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