The Logic of Constraint Satisfaction
University of British Columbia, Department of Computer Science, 1991 - Logic, Symbolic and mathematical - 20 pages
Abstract: "The Constraint Satisfaction Problem (CSP) formalization has been a productive tool within Artificial Intelligence and related areas. The Finite CSP (FCSP) framework is presented here as a restricted logical calculus within a space of logical representation and reasoning systems. FCSP is formulated in a variety of logical settings: theorem proving in first order predicate calculus, propositional theorem proving (and hence SAT), the Prolog and Datalog approaches, constraint network algorithms, a logical interpreter for networks of constraints, the Constraint Logic Programming (CLP) paradigm and propositional model finding (and hence SAT, again). Several standard, and some not-so-standard, logical methods can therefore be used to solve these problems.
What people are saying - Write a review
We haven't found any reviews in the usual places.
8th National Conference AC rewrite rule arc consistency binary constraint British Columbia Canadian Flag completion(Constraints Computer Science Conference on Artificial Constraint Logic Programming constraint satisfaction problems Constraints h Query CSP paradigm CSP's Databases Definite Clause Programs deletes directed constraint network domain encoding FCS as Theorem FCS Decision Problem FCSDP Finite Constraint Satisfaction flag example formula hence SAT Herbrand universe Horn clauses HornSAT algorithm iff Constraints Kleer lift to CSP LINC logical framework logical interpreter logical methods logical representation Mackworth mixed clauses model of F model-finding framework ne(r ne(X negative clauses networks of constraints order predicate calculus posed positive literal Proc Prolog properties of FCSP Propositional Calculus Propositional Logic propositional theory PX(X reasoning systems representation and reasoning restricted logical calculus shown in Figure SLD-resolution solution exists special properties specified subsumption theory Constraints tuples unary unit resolution universal quantifiers values X:r V X:w Y:r V Y:w Z:r V Z:w