A high-level derivation of global search algorithms (with constraint propagation)

In this paper we describe the formal derivation of a transportation scheduling algorithm. The algorithm is based on the concepts of global search and constraint propagation and was originally derived using kids (Kestrel Interactive Development System). The emphasis in this paper is on clarity of the overall derivation and on expressing concepts at a level of abstraction that permits significant reuse of concepts, laws, inference patterns, etc.