Higher Order Modelling for First Order Solvers

Many common computational problems can be posed as model expansion problems, where the task is to find a solution satisfying a set of constraints. Many different paradigms and approaches exist to solve these problems. Likewise, there are many languages to express these problems in. Some of these are standardized, such as Answer Set Programming (ASP) or Minizinc. For some languages there is only one system, like the FO(.) language. The language one chooses to express the problem in, has a high impact on both readability of the modelling and the efficiency of an automated solver. In this thesis we explore higher-order language constructs for modelling languages. These are generally considered very readable yet very inefficient, but in some cases this tradeoff is not so strict. This thesis is divided into three parts. The first part of the thesis focusses on the semantics of higher-order languages. Chapter 2 extends \fodot{} with templates as second-order definitions. Templates were already known as language constructs in other languages such as ASP, but their semantics were given through a rewriting process rather than giving a meaning to the templates themselves. Chapter 3 explores how logics are built and introduces infons as the basis for defining the semantics of an arbitrary language construct. Using this approach, we introduce a uniform way to extend languages with (higher-order) language constructs and define a higher-order logic with definitions. The second part of the thesis shows how existing ASP solvers can be used to solve model expansion problems posed in a higher-order language. Chapter 4 explains a translation from Programming Computable Functions (PCF) to Answer Set Programming. It then explains how this translation can handle extensions of PCF to obtain a higher-order modelling language which can be translated to ASP. Chapter 5 explains the workflow of the Functional Modelling System (FMS). This system is a prototype implementation of the language described in Chapter 4. It describes techniques for optimising modellings and how the translation phase fits in a larger system. Even the best languages are easier to use with good supportive software. In the last part of the thesis, we shift our focus away from higher-order features and introduce some tooling that was developed for the IDP3 system. Chapter 6 introduces a web-based IDE for IDP3. This IDE enables new users to easier write theories and get started with IDP. Chapter 7 introduces an interactive configuration tool which was developed to show how specifications written in Decision Model and Notation (DMN) can be used to do more than just draw conclusions from premises. It enables the user to interactively explore the solution space of a configuration problem.

Jaar van publicatie:2019

Toegankelijkheid:Open