Satisfiability and model generation in infinite space

The ultimate goal of declarative problem solving is to represent human expert
information about a problem domain in a logic, and to solve problems and
execute tasks by running generic, domain independent inference engines on these
representations. This goal is pursued in various declarative and formal
programming paradigms (constraint programming, operations research, logic
programming, SAT and SMT). It often results in spectacular
improvements of development time, code size and solution quality with
acceptable performance.
With the FO(.)-Knowledge Base System, we developed one of the richest
declarative languages to date and combined it with multiple forms of
inference. However, the system only has a finite domain solver; it is not
suited for computing with infinite types like lists, strings, trees, unbounded
numbers, sets, etc. This limitation is currently prohibitive.
Traditional logic and functional programming can deal with unbounded domains,
but provides only a single form of inference. Our objective is to get the
best of both worlds by extending the FO(.) modelling language with the
infinitary features of the latter languages (complex datastructures,
higher-order constructs and modularity support), and developing new inference
algorithms for the extended language. This requires the design of a new
language, new inference methods and their implementation. As result, the class
of practical problems that can be satisfactorily tackled by modelling is
greatly extended.