A logical framework for configuration software

There are many reasons why software can be hard to implement. For important classes of applications, the main source of complexity is the domain knowledge that is involved. One such class is that of configuration software, which serves to assist a user in making choices in accordance with certain constraints. For instance, consider an application that helps students compose a study program that complies with all relevant university regulations. The reason why this may be difficult to implement is that these regulations can get quite complicated, making them hard to handle, at least for imperative programming methods. A better approach might be to follow the paradigm of a knowledge base system: explicitly represent the domain knowledge in a declarative way, and implement the behaviour of the application by performing various logical inference methods on it. Doing this well, however, requires that a number of different components be got right. Most importantly, we need an expressive and purely declaratively knowledge representation language, together with a set of useful inference methods. In this paper, we present a framework for implementing this kind of software, based on a rich extension of first-order logic.status: publishe