Satisfiability and model generation in infinite space

The ultimate goal of the declarative programming paradigm is to represent the knowledge available in a problem domain, rather than that of one specific task dealing with (an instance of) that knowledge. So far, declarative approaches have mainly focused on one generic class of tasks and apply one particular form of inference. Various declarative paradigms have done this with great success, often obtaining spectacular improvements of development time, code size and solution quality, while maintaining acceptable performance. The FO(.)-Knowledge Base System is a state-of-the-art declarative system that is quite unique as it comes with a multitude of inferences and allows developers to use the same information for solving very different kinds of tasks. However, the language and its inferences only allow for finite domains; it is not suited for computing with infinite types like lists, strings, trees, unbounded numbers, sets, etc. This limitation is currently prohibitive and the current proposal wants to rectify this. To do so, this proposal brings together advantages of traditional logic and functional programming, where one can build data structures and reason about infinite domains using the interface that sets offer, and the advantages of FO(.). This will require the design of a new language, as well as new inference methods and their implementations. As result, the class of practical problems that can be satisfactorily tackled by modelling will be greatly extended.