This paper considers the fragment ∃∀SO of second-order logic. Many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard (ΣP2) and many of these problems are often solved approximately. In this paper, we develop a general approximative method, i.e., a sound but incomplete method, for solving ∃∀SO satisfiability problems. We use a syntactic representation of a constraint propagation method for first-order logic to transform such an ∃∀SO satisfiability problem to an ∃SO(ID) satisfiability problem (second-order logic, extended with inductive definitions). The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. Inductive definitions are a powerful knowledge representation tool, and this moti- vates us to also approximate ∃∀SO(ID) problems. In order to do this, we first show how to perform propagation on such inductive definitions. Next, we use this to approximate ∃∀SO(ID) satisfiability problems. All this provides a general theoretical framework for a number of approximative methods in the literature. Moreover, we also show how we can use this framework for solving practical useful problems, such as conformant planning, in an effective way.

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 behavior 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 declarative 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.