Marc Denecker

Simon Marynissen, Jesse Heyninck, Bart Bogaerts et al.

Justification theory is a general framework for the definition of semantics of rule-based languages that has a high explanatory potential. Nested justification systems, first introduced by Denecker et al. (2015), allow for the composition of justification systems. This notion of nesting thus enables the modular definition of semantics of rule-based languages, and increases the representational capacities of justification theory. As we show in this paper, the original semantics for nested justification systems lead to the loss of information relevant for explanations. In view of this problem, we provide an alternative characterization of semantics of nested justification systems and show that this characterization is equivalent to the original semantics. Furthermore, we show how nested justification systems allow representing fixpoint definitions (Hou and Denecker 2009).

Pierre Carbonnelle, Gottfried Schenner, Maurice Bruynooghe et al.

We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a ``lifted'' vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Our results justify further research in automatic translation of sentences for symmetry reduction.

Jo Devriendt, Patrick De Causmaecker, Marc Denecker

Applying local search algorithms to combinatorial optimization problems is not an easy feat. Typically, human intervention is required to compile the constraints to input data for some metaheuristic algorithm. In this paper, we establish a link between symmetry properties of constraint optimization problems and local search neighborhoods, and we use this link to automatically generate neighborhoods from a constraint specification in the context of the IDP system. We evaluate the obtained neighborhoods for six classical optimization problems. The resulting observations support the viability of this technique.

Robbe Van den Eede, Marc Denecker

Inductive definitions are an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic FO with general non-monotone inductive definitions. Most existing proof systems for inductive definitions impose syntactic constraints on their definitions, thereby excluding many useful and natural definitions. We extend an existing sequent calculus LKID by Brotherston and Simpson, founded on the principle of mathematical induction, to a sequent calculus SCFO(ID) for FO(ID). The main challenge in this extension is the accommodation of non-monotone inductive definitions. To overcome this challenge, we draw inspiration from the stable semantics, which is a commonly used semantics in logic programming that is closely related to the well-founded semantics behind FO(ID). We corroborate SCFO(ID) by establishing several proof-theoretical properties and through demonstration on various examples. In conclusion, SCFO(ID) is a theoretically substantiated sequent calculus for FO(ID), enabling formal proofs of theorems involving general inductive definitions.

Đorđe Marković, Simon Vandevelde, Linde Vanbesien et al.

Substantial efforts have been made in developing various Decision Modeling formalisms, both from industry and academia. A challenging problem is that of expressing decision knowledge in the context of incomplete knowledge. In such contexts, decisions depend on what is known or not known. We argue that none of the existing formalisms for modeling decisions are capable of correctly capturing the epistemic nature of such decisions, inevitably causing issues in situations of uncertainty. This paper presents a new language for modeling decisions with incomplete knowledge. It combines three principles: stratification, autoepistemic logic, and definitions. A knowledge base in this language is a hierarchy of epistemic theories, where each component theory may epistemically reason on the knowledge in lower theories, and decisions are made using definitions with epistemic conditions.

Linde Vanbesien, Bart Bogaerts, Marc Denecker

Approximation Fixpoint Theory (AFT) is a powerful theory covering various semantics of non-monotonic reasoning formalisms in knowledge representation such as Logic Programming and Answer Set Programming. Many semantics of such non-monotonic formalisms can be characterized as suitable fixpoints of a non-monotonic operator on a suitable lattice. Instead of working on the original lattice, AFT operates on intervals in such lattice to approximate or construct the fixpoints of interest. While AFT has been applied successfully across a broad range of non-monotonic reasoning formalisms, it is confronted by its limitations in other, relatively simple, examples. In this paper, we overcome those limitations by extending consistent AFT to deal with approximations that are more refined than intervals. Therefore, we introduce a more general notion of approximation spaces, showcase the improved expressiveness and investigate relations between different approximation spaces.

Đorđe Marković, Marc Denecker

Subtyping, also known as subtype polymorphism, is a concept extensively studied in programming language theory, delineating the substitutability relation among datatypes. This property ensures that programs designed for supertype objects remain compatible with their subtypes. In this paper, we explore the capability of order-sorted logic for utilizing these ideas in the context of Knowledge Representation. We recognize two fundamental limitations: First, the inability of this logic to address the concept rather than the value of non-logical symbols, and second, the lack of language constructs for constraining the type of terms. Consequently, we propose guarded order-sorted intensional logic, where guards are language constructs for annotating typing information and intensional logic provides support for quantification over concepts.

Pierre Carbonnelle, Joost Vennekens, Bart Bogaerts et al.

Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the \emph{environment}, while satisfying certain conditions that are formally specified. Such problems are found in, e.g., engineering, law or economics. We study this class of problems in a context where some of the relevant information about the environment is not known by the user at the start of the search. During the search, the user may consider tentative solutions that make implicit hypotheses about these unknowns. To ensure that the solution is appropriate, these hypotheses must be verified by observing the environment. Furthermore, we assume that, in addition to knowledge of what constitutes a solution, knowledge of general laws of the environment is also present. We formally define partial solutions with enough verified facts to guarantee the existence of complete and appropriate solutions. Additionally, we propose an interactive system to assist the user in their search by determining 1) which hypotheses implicit in a tentative solution must be verified in the environment, and 2) which observations can bring useful information for the search. We present an efficient method to over-approximate the set of relevant information, and evaluate our implementation.

Pierre Carbonnelle, Matthias Van der Hallen, Marc Denecker

We argue that in some KR applications, we want to quantify over sets of concepts formally represented by symbols in the vocabulary. We show that this quantification should be distinguished from second-order quantification and meta-programming quantification. We also investigate the relationship with concepts in intensional logic. We present an extension of first-order logic to support such abstractions, and show that it allows writing expressions of knowledge that are elaboration tolerant. To avoid nonsensical sentences in this formalism, we refine the concept of well-formed sentences, and propose a method to verify well-formedness with a complexity that is linear with the number of tokens in the formula. We have extended FO(.), a Knowledge Representation language, and IDP-Z3, a reasoning engine for FO(.), accordingly. We show that this extension was essential in accurately modelling various problem domains in an elaboration-tolerant way, i.e., without reification.

Pierre Carbonnelle, Simon Vandevelde, Joost Vennekens et al.

Industry abounds with interactive configuration problems, i.e., constraint solving problems interactively solved by persons with the assistance of a computer. The computer program, called a configurator, needs to perform a variety of reasoning tasks with the (often incomplete) information that the user provides. Imperative programming approaches make such systems difficult to implement and maintain. Knowledge-based configurators have been proposed to help engineers solve such problems, but many challenges remain. We present IDP-Z3, a new reasoning engine for the FO(.) KR language, and we report on its use for building configurators automatically from a knowledge base.

Linde Vanbesien, Maurice Bruynooghe, Marc Denecker

Aggregates provide a concise way to express complex knowledge. The problem of selecting an appropriate formalisation of aggregates for answer set programming (ASP) remains unsettled. This paper revisits it from the viewpoint of Approximation Fixpoint Theory (AFT). We introduce an AFT formalisation equivalent with the Gelfond-Lifschitz reduct for basic ASP programs and we extend it to handle aggregates. We analyse how existing approaches relate to our framework. We hope this work sheds some new light on the issue of a proper formalisation of aggregates. This paper is under consideration for acceptance in TPLP.

Simon Marynissen, Bart Bogaerts, Marc Denecker

Justification theory is a unifying semantic framework. While it has its roots in non-monotonic logics, it can be applied to various areas in computer science, especially in explainable reasoning; its most central concept is a justification: an explanation why a property holds (or does not hold) in a model. In this paper, we continue the study of justification theory by means of three major contributions. The first is studying the relation between justification theory and game theory. We show that justification frameworks can be seen as a special type of games. The established connection provides the theoretical foundations for our next two contributions. The second contribution is studying under which condition two different dialects of justification theory (graphs as explanations vs trees as explanations) coincide. The third contribution is establishing a precise criterion of when a semantics induced by justification theory yields consistent results. In the past proving that such semantics were consistent took cumbersome and elaborate proofs. We show that these criteria are indeed satisfied for all common semantics of logic programming. This paper is under consideration for acceptance in Theory and Practice of Logic Programming (TPLP).

Marc Denecker, Yuliya Lierler, Miroslaw truszczynski et al.

In Knowledge Representation, it is crucial that knowledge engineers have a good understanding of the formal expressions that they write. What formal expressions state intuitively about the domain of discourse is studied in the theory of the informal semantics of a logic. In this paper we study the informal semantics of Answer Set Programming. The roots of answer set programming lie in the language of Extended Logic Programming, which was introduced initially as an epistemic logic for default and autoepistemic reasoning. In 1999, the seminal papers on answer set programming proposed to use this logic for a different purpose, namely, to model and solve search problems. Currently, the language is used primarily in this new role. However, the original epistemic intuitions lose their explanatory relevance in this new context. How answer set programs are connected to the specifications of problems they model is more easily explained in a classical Tarskian semantics, in which models correspond to possible worlds, rather than to belief states of an epistemic agent. In this paper, we develop a new theory of the informal semantics of answer set programming, which is formulated in the Tarskian setting and based on Frege's compositionality principle. It differs substantially from the earlier epistemic theory of informal semantics, providing a different view on the meaning of the connectives in answer set programming and on its relation to other logics, in particular classical logic.

Joachim Jansen, Jo Devriendt, Bart Bogaerts et al.

PC(ID) extends propositional logic with inductive definitions: rule sets under the well-founded semantics. Recently, a notion of relevance was introduced for this language. This notion determines the set of undecided literals that can still influence the satisfiability of a PC(ID) formula in a given partial assignment. The idea is that the PC(ID) solver can make decisions only on relevant literals without losing soundness and thus safely ignore irrelevant literals. One important insight that the relevance of a literal is completely determined by the current solver state. During search, the solver state changes have an effect on the relevance of literals. In this paper, we discuss an incremental, lightweight implementation of a relevance tracker module that can be added to and interact with an out-of-the-box SAT(ID) solver.

Pieter Van Hertum, Ingmar Dasseville, Gerda Janssens et al.

The knowledge base paradigm aims to express domain knowledge in a rich formal language, and to use this domain knowledge as a knowledge base to solve various problems and tasks that arise in the domain by applying multiple forms of inference. As such, the paradigm applies a strict separation of concerns between information and problem solving. In this paper, we analyze the principles and feasibility of the knowledge base paradigm in the context of an important class of applications: interactive configuration problems. In interactive configuration problems, a configuration of interrelated objects under constraints is searched, where the system assists the user in reaching an intended configuration. It is widely recognized in industry that good software solutions for these problems are very difficult to develop. We investigate such problems from the perspective of the KB paradigm. We show that multiple functionalities in this domain can be achieved by applying different forms of logical inferences on a formal specification of the configuration domain. We report on a proof of concept of this approach in a real-life application with a banking company. To appear in Theory and Practice of Logic Programming (TPLP).

Ruben Lapauw, Ingmar Dasseville, Marc Denecker

A large part of the use of knowledge base systems is the interpretation of the output by the end-users and the interaction with these users. Even during the development process visualisations can be a great help to the developer. We created IDPD3 as a library to visualise models of logic theories. IDPD3 is a new version of $ID^{P}_{Draw}$ and adds support for visualised interactive simulations.

Bart Bogaerts, Joost Vennekens, Marc Denecker et al.

Cause-effect relations are an important part of human knowledge. In real life, humans often reason about complex causes linked to complex effects. By comparison, existing formalisms for representing knowledge about causal relations are quite limited in the kind of specifications of causes and effects they allow. In this paper, we present the new language C-Log, which offers a significantly more expressive representation of effects, including such features as the creation of new objects. We show how C-Log integrates with first-order logic, resulting in the language FO(C). We also compare FO(C) with several related languages and paradigms, including inductive definitions, disjunctive logic programming, business rules and extensions of Datalog.

Marcos Cramer, Pieter Van Hertum, Diego Agustin Ambrossio et al.

In ownership-based access control frameworks with the possibility of delegating permissions and administrative rights, chains of delegated accesses will form. There are different ways to treat these delegation chains when revoking rights, which give rise to different revocation schemes. In this paper, we show how IDP - a knowledge base system that integrates technology from ASP, SAT and CP - can be used to efficiently implement executable revocation schemes for an ownership-based access control system based on a declarative specification of their properties.

Johan Wittocx, Maarten Mariën, Marc Denecker

Grounding is the task of reducing a first-order theory and finite domain to an equivalent propositional theory. It is used as preprocessing phase in many logic-based reasoning systems. Such systems provide a rich first-order input language to a user and can rely on efficient propositional solvers to perform the actual reasoning. Besides a first-order theory and finite domain, the input for grounders contains in many applications also additional data. By exploiting this data, the size of the grounders output can often be reduced significantly. A common practice to improve the efficiency of a grounder in this context is by manually adding semantically redundant information to the input theory, indicating where and when the grounder should exploit the data. In this paper we present a method to compute and add such redundant information automatically. Our method therefore simplifies the task of writing input theories that can be grounded efficiently by current systems. We first present our method for classical first-order logic (FO) theories. Then we extend it to FO(ID), the extension of FO with inductive definitions, which allows for more concise and comprehensive input theories. We discuss implementation issues and experimentally validate the practical applicability of our method.

Maurice Bruynooghe, Hendrik Blockeel, Bart Bogaerts et al.

This paper provides a gentle introduction to problem solving with the IDP3 system. The core of IDP3 is a finite model generator that supports first order logic enriched with types, inductive definitions, aggregates and partial functions. It offers its users a modeling language that is a slight extension of predicate logic and allows them to solve a wide range of search problems. Apart from a small introductory example, applications are selected from problems that arose within machine learning and data mining research. These research areas have recently shown a strong interest in declarative modeling and constraint solving as opposed to algorithmic approaches. The paper illustrates that the IDP3 system can be a valuable tool for researchers with such an interest. The first problem is in the domain of stemmatology, a domain of philology concerned with the relationship between surviving variant versions of text. The second problem is about a somewhat related problem within biology where phylogenetic trees are used to represent the evolution of species. The third and final problem concerns the classical problem of learning a minimal automaton consistent with a given set of strings. For this last problem, we show that the performance of our solution comes very close to that of a state-of-the art solution. For each of these applications, we analyze the problem, illustrate the development of a logic-based model and explore how alternatives can affect the performance.

Joost Vennekens, Marc Denecker

Previous research into the relation between ASP and classical logic has identified at least two different ways in which the former extends the latter. First, ASP program typically contain sets of rules that can be naturally interpreted as inductive definitions, and the language FO(ID) has shown that such inductive definitions can elegantly be added to classical logic in a modular way. Second, there is of course also the well-known epistemic component of ASP, which was mainly emphasized in the early papers on stable model semantics. To investigate whether this kind of knowledge can also, and in a similarly modular way, be added to classical logic, the language of Ordered Epistemic Logic was presented in recent work. However, this logic views the epistemic component as entirely separate from the inductive definition component, thus ignoring any possible interplay between the two. In this paper, we present a language that extends the inductive definition construct found in FO(ID) with an epistemic component, making such interplay possible. The eventual goal of this work is to discover whether it is really appropriate to view the epistemic component and the inductive definition component of ASP as two separate extensions of classical logic, or whether there is also something of importance in the combination of the two.

Ping Hou, Johan Wittocx, Marc Denecker

The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes the view on these formalisms as logics of (generalized) inductive definitions. The goal of this paper is to study a deductive inference method for PC(ID), which is the propositional fragment of FO(ID). We introduce a formal proof system based on the sequent calculus (Gentzen-style deductive system) for this logic. As PC(ID) is an integration of classical propositional logic and propositional inductive definitions, our sequent calculus proof system integrates inference rules for propositional calculus and definitions. We present the soundness and completeness of this proof system with respect to a slightly restricted fragment of PC(ID). We also provide some complexity results for PC(ID). By developing the proof system for PC(ID), it helps us to enhance the understanding of proof-theoretic foundations of FO(ID), and therefore to investigate useful proof systems for FO(ID).