Universal Quantification in a Constraint-Based Planner

We present a general approach to planning with a restricted class of universally quantified constraints. These constraints stem from expressive action descriptions, coupled with large or infinite universes and incomplete information. The approach essentially consists of checking that the quantified constraint is satisfied for all members of the universe. We present a general algorithm for proving that quantified constraints are satisfied when the domains of all of the variables are finite. We then describe a class of quantified constraints for which we can efficiently prove satisfiability even when the domains are infinite. These form the basis of constraint reasoning systems that can be used by a variety of planners