Satisfiability and model generation in infinite space

The goal of declarative programming is to represent the knowledge available in a problem domain and solve tasks using inference tools.  The FO(.)-Knowledge Base System IDP is a state-of-the-art declarative system that is unique as it comes with a multitude of inferences and allows developers to use the same information for solving very different kinds of tasks. Currently, the language and its inferences only allow for finite domains; it is not suited for computing with infinite types like unbounded numbers, lists, strings, trees, sets, etc. This limitation is currently prohibitive and the current proposal wants to rectify this.

To do so, this proposal intends to bring together advantages of different logic based programming branches. SMT solvers in particular have been designed with infinite domains in mind. We will combine these techniques with the advantages of FO(.) to create a more powerful Knowledge Base System. This will require designing new language constructs and extending the inference methods to support these. As a result, the class of practical problems that can be satisfactorily tackled will be greatly extended. The results of this research are an interesting contribution to grounding based solvers in general.