Predicate logic as a modelling language: The IDP system

per Predicate Logic as a Programming Language was a breakthrough for the use of logic in computer science. The more recent tremendous pro-gress in automated reasoning technologies, particularly in SAT solving and Constraint Programming, has paved the way for the use of logic as a modelling language. This paper describes the realisation of such a mod-elling language as the IDP knowledge-base system (KBS). In contrast to declarative programming, the user only specifies her knowledge about a problem and has not to pay attention to control issues. In the IDP system, declarative modelling is done in the language FO(·)IDP which combines inductive definitions (similar to sets of Prolog rules) with first-order logic, types and aggregates, allowing for concise specifications. The paper presents the language, motivates the design choices and gives an overview of the system architecture and the implementation tech-niques. It also gives an overview of different inference tasks supported by the system such as query evaluation, model expansion and theorem prov-ing, and explains in detail how combining various functionalities results in a state-of-the-art model expansion engine. Finally, it explains how a tight integration with a procedural language (Lua) allows users to treat logical components as first-class citizens and to solve complex problems in a workflow of (multi-inference) interactions.