A Proof Theoretic View of Constraint Programming

Article type: Research Article

Authors: Apt, Krzysztof R.^;

Affiliations: CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands | Dept. of Mathematics, Computer Science, Physics & Astronomy, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands. apt@cwi.nl

Note: [] Address for correspondence: CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands

Abstract: We provide here a proof theoretic account of constraint programming that attempts to capture the essential ingredients of this programming style. We exemplify it by presenting proof rules for linear constraints over interval domains, and illustrate their use by analyzing the constraint propagation process for the SEND + MORE = MONEY puzzle. We also show how this approach allows one to build new constraint solvers.

Keywords: constraints, constraint propagation, proof rules, linear constraints

DOI: 10.3233/FI-1998-34304

Journal: Fundamenta Informaticae, vol. 34, no. 3, pp. 295-321, 1998