Showing 1–50 of 50 results for author: Denecker, M

An epistemic logic for modeling decisions in the context of incomplete knowledge

Authors: Đorđe Marković, Simon Vandevelde, Linde Vanbesien, Joost Vennekens, Marc Denecker

Abstract: Substantial efforts have been made in develo** 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 epi… ▽ More Substantial efforts have been made in develo** 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. △ Less

Submitted 18 December, 2023; originally announced December 2023.

Comments: 9 pages, 3 figures, to be published as a poster version in the ACM/SIGAPP conference

Using Symmetries to Lift Satisfiability Checking

Authors: Pierre Carbonnelle, Gottfried Schenner, Maurice Bruynooghe, Bart Bogaerts, Marc Denecker

Abstract: 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 o… ▽ More 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. △ Less

Submitted 14 December, 2023; v1 submitted 6 November, 2023; originally announced November 2023.

Comments: Accepted at AAAI-24

Distributed Autoepistemic Logic: Semantics, Complexity, and Applications to Access Control

Authors: Marcos Cramer, Pieter Van Hertum, Bart Bogaerts, Marc Denecker

Abstract: In this paper we define and study a multi-agent extension of autoepistemic logic (AEL) called distributed autoepistemic logic (dAEL). We define the semantics of dAEL using approximation fixpoint theory, an abstract algebraic framework that unifies different knowledge representation formalisms by describing their semantics as fixpoints of semantic operators. We define 2- and 3-valued semantic opera… ▽ More In this paper we define and study a multi-agent extension of autoepistemic logic (AEL) called distributed autoepistemic logic (dAEL). We define the semantics of dAEL using approximation fixpoint theory, an abstract algebraic framework that unifies different knowledge representation formalisms by describing their semantics as fixpoints of semantic operators. We define 2- and 3-valued semantic operators for dAEL. Using these operators, approximation fixpoint theory allows us to define a class of semantics for dAEL, each based on different intuitions that are well-studied in the context of AEL. We define a map** from dAEL to AEL and identify the conditions under which the map** preserves semantics, and furthermore argue that when it does not, the dAEL semantics is more desirable than the AEL-induced semantics since dAEL manages to contain inconsistencies. The development of dAEL has been motivated by an application in the domain of access control. We explain how dAEL can be fruitfully applied to this domain and discuss how well-suited the different semantics are for the application in access control. △ Less

Submitted 5 June, 2023; originally announced June 2023.

Interactive Model Expansion in an Observable Environment

Authors: Pierre Carbonnelle, Joost Vennekens, Bart Bogaerts, Marc Denecker

Abstract: 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… ▽ More 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. △ Less

Submitted 20 May, 2023; originally announced May 2023.

Comments: This paper is an extended and revised version of a conference paper appearing in the proceedings of ICLP 2023 and to be published in Theory and Practice of Logic Programming

The Logic of Logic Programming

Authors: Marc Denecker, David S. Warren

Abstract: Our position is that logic programming is not programming in the Horn clause sublogic of classical logic, but programming in a logic of (inductive) definitions. Thus, the similarity between prototypical Prolog programs (e.g., member, append, ...) and how inductive definitions are expressed in mathematical text, is not coincidental but essential. We argue here that this provides a natural solution… ▽ More Our position is that logic programming is not programming in the Horn clause sublogic of classical logic, but programming in a logic of (inductive) definitions. Thus, the similarity between prototypical Prolog programs (e.g., member, append, ...) and how inductive definitions are expressed in mathematical text, is not coincidental but essential. We argue here that this provides a natural solution to the main lingering semantic questions of Logic Programming and its extensions. △ Less

Submitted 26 April, 2023; originally announced April 2023.

MSC Class: 03B70 ACM Class: F.3.2; F.4.3

On Nested Justification Systems (full version)

Authors: Simon Marynissen, Jesse Heyninck, Bart Bogaerts, Marc Denecker

Abstract: 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 cap… ▽ More 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). △ Less

Submitted 9 May, 2022; originally announced May 2022.

Comments: Paper presented at the 38th International Conference on Logic Programming (ICLP 2022), 16 pages

Quantification and Aggregation over Concepts of the Ontology

Authors: Pierre Carbonnelle, Matthias Van der Hallen, Marc Denecker

Abstract: 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 abstr… ▽ More 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. △ Less

Submitted 30 August, 2023; v1 submitted 2 February, 2022; originally announced February 2022.

Comments: In Proceedings ICLP 2023, arXiv:2308.14898

Journal ref: EPTCS 385, 2023, pp. 213-226

Interactive configurator with FO(.) and IDP-Z3

Authors: Pierre Carbonnelle, Simon Vandevelde, Joost Vennekens, Marc Denecker

Abstract: 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 maintai… ▽ More 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. △ Less

Submitted 20 March, 2023; v1 submitted 1 February, 2022; originally announced February 2022.

Comments: Submitted to KR 2023

Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory

Authors: Linde Vanbesien, Maurice Bruynooghe, Marc Denecker

Abstract: 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 aggreg… ▽ More 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. △ Less

Submitted 17 May, 2022; v1 submitted 30 April, 2021; originally announced April 2021.

Comments: Paper presented at the 38th International Conference on Logic Programming (ICLP 2022), 22 pages (including supplementary material)

Justifications and a Reconstruction of Parity Game Solving Algorithms

Authors: Ruben Lapauw, Maurice Bruynooghe, Marc Denecker

Abstract: Parity games are infinite two-player games played on directed graphs. Parity game solvers are used in the domain of formal verification. This paper defines parametrized parity games and introduces an operation, Justify, that determines a winning strategy for a single node. By carefully ordering Justify steps, we reconstruct three algorithms well known from the literature. Parity games are infinite two-player games played on directed graphs. Parity game solvers are used in the domain of formal verification. This paper defines parametrized parity games and introduces an operation, Justify, that determines a winning strategy for a single node. By carefully ordering Justify steps, we reconstruct three algorithms well known from the literature. △ Less

Submitted 2 February, 2021; originally announced February 2021.

Comments: 16 pages, to appear in "LNCS Honorary Volume for Manuel Hermenegildo" [AVERTIS 2019]

Exploiting Game Theory for Analysing Justifications

Authors: Simon Marynissen, Bart Bogaerts, Marc Denecker

Abstract: 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 contrib… ▽ More 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). △ Less

Submitted 4 August, 2020; originally announced August 2020.

Comments: Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 15+8 pages

Journal ref: Theory and Practice of Logic Programming 20 (2020) 880-894

The informal semantics of Answer Set Programming: A Tarskian perspective

Authors: Marc Denecker, Yuliya Lierler, Miroslaw truszczynski, Joost Vennekens

Abstract: 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… ▽ More 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. △ Less

Submitted 25 January, 2019; originally announced January 2019.

Transpiling Programmable Computable Functions to Answer Set Programs

Authors: Ingmar Dasseville, Marc Denecker

Abstract: Programming Computable Functions (PCF) is a simplified programming language which provides the theoretical basis of modern functional programming languages. Answer set programming (ASP) is a programming paradigm focused on solving search problems. In this paper we provide a translation from PCF to ASP. Using this translation it becomes possible to specify search problems using PCF. Programming Computable Functions (PCF) is a simplified programming language which provides the theoretical basis of modern functional programming languages. Answer set programming (ASP) is a programming paradigm focused on solving search problems. In this paper we provide a translation from PCF to ASP. Using this translation it becomes possible to specify search problems using PCF. △ Less

Submitted 23 August, 2018; originally announced August 2018.

Comments: 15 pages, Accepted for presentation in WFLP 2018

A Logical Study of Some Common Principles of Inductive Definition and its Implications for Knowledge Representation

Authors: Marc Denecker, Bart Bogaerts, Joost Vennekens

Abstract: The definition is a common form of human expert knowledge, a building block of formal science and mathematics, a foundation for database theory and is supported in various forms in many knowledge representation and formal specification languages and systems. This paper is a formal study of some of the most common forms of inductive definitions found in scientific text: monotone inductive definitio… ▽ More The definition is a common form of human expert knowledge, a building block of formal science and mathematics, a foundation for database theory and is supported in various forms in many knowledge representation and formal specification languages and systems. This paper is a formal study of some of the most common forms of inductive definitions found in scientific text: monotone inductive definition, definition by induction over a well-founded order and iterated inductive definitions. We define a logic of definitions offering a uniform formal syntax to express definitions of the different sorts, and we define its semantics by a faithful formalization of the induction process. Several fundamental properties of definition by induction emerge: the non-determinism of the induction process, the confluence of induction processes, the role of the induction order and its relation to the inductive rules, how the induction order constrains the induction process and, ultimately, that the induction order is irrelevant: the defined set does not depend on the induction order. We propose an inductive construction capable of constructing the defined set without using the induction order. We investigate borderline definitions of the sort that appears in definitional paradoxes. △ Less

Submitted 15 February, 2017; originally announced February 2017.

Implementing a Relevance Tracker Module

Authors: Joachim Jansen, Jo Devriendt, Bart Bogaerts, Gerda Janssens, Marc Denecker

Abstract: 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… ▽ More 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. △ Less

Submitted 19 August, 2016; originally announced August 2016.

Comments: Paper presented at the 9th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2016), New York City, USA, 16 October 2016

On Local Domain Symmetry for Model Expansion

Authors: Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, Marc Denecker

Abstract: Symmetry in combinatorial problems is an extensively studied topic. We continue this research in the context of model expansion problems, with the aim of automating the workflow of detecting and breaking symmetry. We focus on local domain symmetry, which is induced by permutations of domain elements, and which can be detected on a first-order level. As such, our work is a continuation of the symme… ▽ More Symmetry in combinatorial problems is an extensively studied topic. We continue this research in the context of model expansion problems, with the aim of automating the workflow of detecting and breaking symmetry. We focus on local domain symmetry, which is induced by permutations of domain elements, and which can be detected on a first-order level. As such, our work is a continuation of the symmetry exploitation techniques of model generation systems, while it differs from more recent symmetry breaking techniques in answer set programming which detect symmetry on ground programs. Our main contributions are sufficient conditions for symmetry of model expansion problems, the identification of local domain interchangeability, which can often be broken completely, and efficient symmetry detection algorithms for both local domain interchangeability as well as local domain symmetry in general. Our approach is implemented in the model expansion system IDP, and we present experimental results showcasing the strong and weak points of our approach compared to SBASS , a symmetry breaking technique for answer set programming. △ Less

Submitted 9 August, 2016; originally announced August 2016.

Comments: Paper presented at the 32nd International Conference on Logic Programming (ICLP 2016), New York City, USA, 16-21 October 2016, 15 pages, LaTeX, 3 PDF figures (arXiv:YYMM.NNNNN)

The KB paradigm and its application to interactive configuration

Authors: Pieter Van Hertum, Ingmar Dasseville, Gerda Janssens, Marc Denecker

Abstract: 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 feasibili… ▽ More 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). △ Less

Submitted 6 May, 2016; originally announced May 2016.

Comments: To appear in Theory and Practice of Logic Programming (TPLP)

Visualising interactive inferences with IDPD3

Authors: Ruben Lapauw, Ingmar Dasseville, Marc Denecker

Abstract: 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. 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. △ Less

Submitted 3 November, 2015; originally announced November 2015.

Comments: International Workshop on User-Oriented Logic Programming (IULP 2015), co-located with the 31st International Conference on Logic Programming (ICLP 2015), Proceedings of the International Workshop on User-Oriented Logic Programming (IULP 2015), Editors: Stefan Ellmauthaler and Claudia Schulz, pages 67-81, August 2015

Semantics of templates in a compositional framework for building logics

Authors: Ingmar Dasseville, Matthias van der Hallen, Gerda Janssens, Marc Denecker

Abstract: There is a growing need for abstractions in logic specification languages such as FO(.) and ASP. One technique to achieve these abstractions are templates (sometimes called macros). While the semantics of templates are virtually always described through a syntactical rewriting scheme, we present an alternative view on templates as second order definitions. To extend the existing definition constru… ▽ More There is a growing need for abstractions in logic specification languages such as FO(.) and ASP. One technique to achieve these abstractions are templates (sometimes called macros). While the semantics of templates are virtually always described through a syntactical rewriting scheme, we present an alternative view on templates as second order definitions. To extend the existing definition construct of FO(.) to second order, we introduce a powerful compositional framework for defining logics by modular integration of logic constructs specified as pairs of one syntactical and one semantical inductive rule. We use the framework to build a logic of nested second order definitions suitable to express templates. We show that under suitable restrictions, the view of templates as macros is semantically correct and that adding them does not extend the descriptive complexity of the base logic, which is in line with results of existing approaches. △ Less

Submitted 24 July, 2015; originally announced July 2015.

Journal ref: Theory and Practice of Logic Programming 15 (2015) 681-695

FO(C): A Knowledge Representation Language of Causality

Authors: Bart Bogaerts, Joost Vennekens, Marc Denecker, Jan Van den Bussche

Abstract: 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 ex… ▽ More 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. △ Less

Submitted 9 May, 2014; v1 submitted 8 May, 2014; originally announced May 2014.

Comments: To appear in Theory and Practice of Logic Programming (TPLP)

Modelling Delegation and Revocation Schemes in IDP

Authors: Marcos Cramer, Pieter Van Hertum, Diego Agustin Ambrossio, Marc Denecker

Abstract: 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 b… ▽ More 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. △ Less

Submitted 7 May, 2014; originally announced May 2014.

Comments: 16 pages

Simulating dynamic systems using Linear Time Calculus theories

Authors: Bart Bogaerts, Joachim Jansen, Maurice Bruynooghe, Broes De Cat, Joost Vennekens, Marc Denecker

Abstract: To appear in Theory and Practice of Logic Programming (TPLP). Dynamic systems play a central role in fields such as planning, verification, and databases. Fragmented throughout these fields, we find a multitude of languages to formally specify dynamic systems and a multitude of systems to reason on such specifications. Often, such systems are bound to one specific language and one specific infer… ▽ More To appear in Theory and Practice of Logic Programming (TPLP). Dynamic systems play a central role in fields such as planning, verification, and databases. Fragmented throughout these fields, we find a multitude of languages to formally specify dynamic systems and a multitude of systems to reason on such specifications. Often, such systems are bound to one specific language and one specific inference task. It is troublesome that performing several inference tasks on the same knowledge requires translations of your specification to other languages. In this paper we study whether it is possible to perform a broad set of well-studied inference tasks on one specification. More concretely, we extend IDP3 with several inferences from fields concerned with dynamic specifications. △ Less

Submitted 17 June, 2024; v1 submitted 7 May, 2014; originally announced May 2014.

Journal ref: Theory and Practice of Logic Programming 14 (2014) 477-492

FO(C) and Related Modelling Paradigms

Authors: Bart Bogaerts, Joost Vennekens, Marc Denecker, Jan Van den Bussche

Abstract: Recently, C-Log was introduced as a language for modelling causal processes. Its formal semantics has been defined together with introductory examples, but the study of this language is far from finished. In this paper, we compare C-Log to other declarative modelling languages. More specifically, we compare to first-order logic (FO), and argue that C-Log and FO are orthogonal and that their integr… ▽ More Recently, C-Log was introduced as a language for modelling causal processes. Its formal semantics has been defined together with introductory examples, but the study of this language is far from finished. In this paper, we compare C-Log to other declarative modelling languages. More specifically, we compare to first-order logic (FO), and argue that C-Log and FO are orthogonal and that their integration, FO(C), is a knowledge representation language that allows for clear and succinct models. We compare FO(C) to E-disjunctive logic programming with the stable semantics, and define a fragment on which both semantics coincide. Furthermore, we discuss object-creation in FO(C), relating it to mathematics, business rules systems, and data base systems. △ Less

Submitted 25 April, 2014; originally announced April 2014.

Comments: This paper appears in the Proceedings of the 15th International Workshop on Non-Monotonic Reasoning (NMR 2014)

Inference in the FO(C) Modelling Language

Authors: Bart Bogaerts, Joost Vennekens, Marc Denecker, Jan Van den Bussche

Abstract: Recently, FO(C), the integration of C-Log with classical logic, was introduced as a knowledge representation language. Up to this point, no systems exist that perform inference on FO(C), and very little is known about properties of inference in FO(C). In this paper, we study both of the above problems. We define normal forms for FO(C), one of which corresponds to FO(ID). We define transformations… ▽ More Recently, FO(C), the integration of C-Log with classical logic, was introduced as a knowledge representation language. Up to this point, no systems exist that perform inference on FO(C), and very little is known about properties of inference in FO(C). In this paper, we study both of the above problems. We define normal forms for FO(C), one of which corresponds to FO(ID). We define transformations between these normal forms, and show that, using these transformations, several inference tasks for FO(C) can be reduced to inference tasks for FO(ID), for which solvers exist. We implemented a prototype of this transformation, and thus present the first system to perform inference in FO(C). We also provide results about the complexity of reasoning in FO(C). △ Less

Submitted 25 April, 2014; originally announced April 2014.

Comments: The paper appears in the Proceedings of the 15th International Workshop on Non-Monotonic Reasoning (NMR 2014)

Lazy Model Expansion: Interleaving Grounding with Search

Authors: Broes De Cat, Marc Denecker, Peter Stuckey, Maurice Bruynooghe

Abstract: Finding satisfying assignments for the variables involved in a set of constraints can be cast as a (bounded) model generation problem: search for (bounded) models of a theory in some logic. The state-of-the-art approach for bounded model generation for rich knowledge representation languages, like ASP, FO(.) and Zinc, is ground-and-solve: reduce the theory to a ground or propositional one and appl… ▽ More Finding satisfying assignments for the variables involved in a set of constraints can be cast as a (bounded) model generation problem: search for (bounded) models of a theory in some logic. The state-of-the-art approach for bounded model generation for rich knowledge representation languages, like ASP, FO(.) and Zinc, is ground-and-solve: reduce the theory to a ground or propositional one and apply a search algorithm to the resulting theory. An important bottleneck is the blowup of the size of the theory caused by the reduction phase. Lazily grounding the theory during search is a way to overcome this bottleneck. We present a theoretical framework and an implementation in the context of the FO(.) knowledge representation language. Instead of grounding all parts of a theory, justifications are derived for some parts of it. Given a partial assignment for the grounded part of the theory and valid justifications for the formulas of the non-grounded part, the justifications provide a recipe to construct a complete assignment that satisfies the non-grounded part. When a justification for a particular formula becomes invalid during search, a new one is derived; if that fails, the formula is split in a part to be grounded and a part that can be justified. The theoretical framework captures existing approaches for tackling the grounding bottleneck such as lazy clause generation and grounding-on-the-fly, and presents a generalization of the 2-watched literal scheme. We present an algorithm for lazy model expansion and integrate it in a model generator for FO(ID), a language extending first-order logic with inductive definitions. The algorithm is implemented as part of the state-of-the-art FO(ID) Knowledge-Base System IDP. Experimental results illustrate the power and generality of the approach. △ Less

Submitted 3 February, 2015; v1 submitted 27 February, 2014; originally announced February 2014.

Journal ref: Journal of Artificial Intelligence Research, feb 2015, volume 52, pages 235-286

Predicate Logic as a Modelling Language: The IDP System

Authors: Broes De Cat, Bart Bogaerts, Maurice Bruynooghe, Gerda Janssens, Marc Denecker

Abstract: With the technology of the time, Kowalski's seminal 1974 paper {\em Predicate Logic as a Programming Language} was a breakthrough for the use of logic in computer science. It introduced two fundamental ideas: on the declarative side, the use of the Horn clause logic fragment of classical logic, which was soon extended with negation as failure, on the procedural side the procedural interpretation w… ▽ More With the technology of the time, Kowalski's seminal 1974 paper {\em Predicate Logic as a Programming Language} was a breakthrough for the use of logic in computer science. It introduced two fundamental ideas: on the declarative side, the use of the Horn clause logic fragment of classical logic, which was soon extended with negation as failure, on the procedural side the procedural interpretation which made it possible to write algorithms in the formalism. Since then, strong progress was made both on the declarative understanding of the logic programming formalism and in automated reasoning technologies, particularly in SAT solving, Constraint Programming and Answer Set Programming. This has paved the way for the development of an extension of logic programming that embodies a more pure view of logic as a modelling language and its role for problem solving. In this paper, we present the \idp language and system. The language is essentially classical logic extended with one of logic programmings most important contributions to knowledge representation: the representation of complex definitions as rule sets under well-founded semantics. The system is a knowledge base system: a system in which complex declarative information is stored in a knowledge base which can be used to solve different computational problems by applying multiple forms of inference. In this view, theories are declarative modellings, bags of information, descriptions of possible states of affairs. They are neither procedures nor descriptions of computational problems. As such, the \idp language and system preserve the fundamental idea of a declarative reading of logic programs, while they break with the fundamental idea of the procedural interpretation of logic programs. △ Less

Submitted 13 March, 2018; v1 submitted 24 January, 2014; originally announced January 2014.

Grounding FO and FO(ID) with Bounds

Authors: Johan Wittocx, Maarten Mariën, Marc Denecker

Abstract: 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 ground… ▽ More 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. △ Less

Submitted 15 January, 2014; originally announced January 2014.

Journal ref: Journal Of Artificial Intelligence Research, Volume 38, pages 223-269, 2010

Predicate Logic as a Modeling Language: Modeling and Solving some Machine Learning and Data Mining Problems with IDP3

Authors: Maurice Bruynooghe, Hendrik Blockeel, Bart Bogaerts, Broes De Cat, Stef De Pooter, Joachim Jansen, Anthony Labarre, Jan Ramon, Marc Denecker, Sicco Verwer

Abstract: 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… ▽ More 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. △ Less

Submitted 28 March, 2014; v1 submitted 26 September, 2013; originally announced September 2013.

Comments: To appear in Theory and Practice of Logic Programming (TPLP)

Journal ref: Theory and Practice of Logic Programming 15 (2014) 783-817

Extending FO(ID) with Knowledge Producing Definitions: Preliminary Results

Authors: Joost Vennekens, Marc Denecker

Abstract: 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, ther… ▽ More 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. △ Less

Submitted 7 January, 2013; originally announced January 2013.

Comments: Proceedings of Answer Set Programming and Other Computing Paradigms (ASPOCP 2012), 5th International Workshop, September 4, 2012, Budapest, Hungary

LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions

Authors: ** Hou, Johan Wittocx, Marc Denecker

Abstract: 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), whic… ▽ More 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 develo** 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). △ Less

Submitted 10 July, 2012; originally announced July 2012.

Comments: Journal paper

A prototype of a knowledge-based programming environment

Authors: Stef De Pooter, Johan Wittocx, Marc Denecker

Abstract: In this paper we present a proposal for a knowledge-based programming environment. In such an environment, declarative background knowledge, procedures, and concrete data are represented in suitable languages and combined in a flexible manner. This leads to a highly declarative programming style. We illustrate our approach on an example and report about our prototype implementation. In this paper we present a proposal for a knowledge-based programming environment. In such an environment, declarative background knowledge, procedures, and concrete data are represented in suitable languages and combined in a flexible manner. This leads to a highly declarative programming style. We illustrate our approach on an example and report about our prototype implementation. △ Less

Submitted 29 August, 2011; originally announced August 2011.

Comments: 6 pages, appears in the Proceedings of the 19th International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2011)

Reiter's Default Logic Is a Logic of Autoepistemic Reasoning And a Good One, Too

Authors: Marc Denecker, Victor W. Marek, Miroslaw Truszczynski

Abstract: A fact apparently not observed earlier in the literature of nonmonotonic reasoning is that Reiter, in his default logic paper, did not directly formalize informal defaults. Instead, he translated a default into a certain natural language proposition and provided a formalization of the latter. A few years later, Moore noted that propositions like the one used by Reiter are fundamentally different t… ▽ More A fact apparently not observed earlier in the literature of nonmonotonic reasoning is that Reiter, in his default logic paper, did not directly formalize informal defaults. Instead, he translated a default into a certain natural language proposition and provided a formalization of the latter. A few years later, Moore noted that propositions like the one used by Reiter are fundamentally different than defaults and exhibit a certain autoepistemic nature. Thus, Reiter had developed his default logic as a formalization of autoepistemic propositions rather than of defaults. The first goal of this paper is to show that some problems of Reiter's default logic as a formal way to reason about informal defaults are directly attributable to the autoepistemic nature of default logic and to the mismatch between informal defaults and the Reiter's formal defaults, the latter being a formal expression of the autoepistemic propositions Reiter used as a representation of informal defaults. The second goal of our paper is to compare the work of Reiter and Moore. While each of them attempted to formalize autoepistemic propositions, the modes of reasoning in their respective logics were different. We revisit Moore's and Reiter's intuitions and present them from the perspective of autotheoremhood, where theories can include propositions referring to the theory's own theorems. We then discuss the formalization of this perspective in the logics of Moore and Reiter, respectively, using the unifying semantic framework for default and autoepistemic logics that we developed earlier. We argue that Reiter's default logic is a better formalization of Moore's intuitions about autoepistemic propositions than Moore's own autoepistemic logic. △ Less

Submitted 16 August, 2011; originally announced August 2011.

Comments: In G. Brewka, V.M. Marek, and M. Truszczynski, eds. Nonmonotonic Reasoning -- Essays Celebrating its 30th Anniversary, College Publications, 2011 (a volume of papers presented at NonMOn at 30 meeting, Lexington, KY, USA, October 2010

MSC Class: I.2.4

Coherent Integration of Databases by Abductive Logic Programming

Authors: O. Arieli, M. Bruynooghe, M. Denecker, B. Van Nuffelen

Abstract: We introduce an abductive method for a coherent integration of independent data-sources. The idea is to compute a list of data-facts that should be inserted to the amalgamated database or retracted from it in order to restore its consistency. This method is implemented by an abductive solver, called Asystem, that applies SLDNFA-resolution on a meta-theory that relates different, possibly contrad… ▽ More We introduce an abductive method for a coherent integration of independent data-sources. The idea is to compute a list of data-facts that should be inserted to the amalgamated database or retracted from it in order to restore its consistency. This method is implemented by an abductive solver, called Asystem, that applies SLDNFA-resolution on a meta-theory that relates different, possibly contradicting, input databases. We also give a pure model-theoretic analysis of the possible ways to `recover' consistent data from an inconsistent database in terms of those models of the database that exhibit as minimal inconsistent information as reasonably possible. This allows us to characterize the `recovered databases' in terms of the `preferred' (i.e., most consistent) models of the theory. The outcome is an abductive-based application that is sound and complete with respect to a corresponding model-based, preferential semantics, and -- to the best of our knowledge -- is more expressive (thus more general) than any other implementation of coherent integration of databases. △ Less

Submitted 30 June, 2011; originally announced July 2011.

Journal ref: Journal Of Artificial Intelligence Research, Volume 21, pages 245-286, 2004

Constraint Propagation for First-Order Logic and Inductive Definitions

Authors: Johan Wittocx, Marc Denecker, Maurice Bruynooghe

Abstract: Constraint propagation is one of the basic forms of inference in many logic-based reasoning systems. In this paper, we investigate constraint propagation for first-order logic (FO), a suitable language to express a wide variety of constraints. We present an algorithm with polynomial-time data complexity for constraint propagation in the context of an FO theory and a finite structure. We show that… ▽ More Constraint propagation is one of the basic forms of inference in many logic-based reasoning systems. In this paper, we investigate constraint propagation for first-order logic (FO), a suitable language to express a wide variety of constraints. We present an algorithm with polynomial-time data complexity for constraint propagation in the context of an FO theory and a finite structure. We show that constraint propagation in this manner can be represented by a datalog program and that the algorithm can be executed symbolically, i.e., independently of a structure. Next, we extend the algorithm to FO(ID), the extension of FO with inductive definitions. Finally, we discuss several applications. △ Less

Submitted 8 July, 2011; v1 submitted 12 August, 2010; originally announced August 2010.

Comments: 43 pages, 1 figure submitted to ACM Transactions on Computational Logic

ACM Class: I.2.4; F.4.1

FO(FD): Extending classical logic with rule-based fixpoint definitions

Authors: Hou **, Broes De Cat, Marc Denecker

Abstract: We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to differenc… ▽ More We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic. These reductions are evaluated in the computation of models for FO(FD) theories representing fairness conditions and we provide potential applications of FO(FD). △ Less

Submitted 22 July, 2010; originally announced July 2010.

Comments: Presented at ICLP 2010. 16 pages, 1 figure

MSC Class: 68T27 ACM Class: I.2.4; F.4.3

Journal ref: Theory and Practice of Logic Programming, Volume 10, Special Issue 4-6, July 2010, pp 581-596

CP-logic: A Language of Causal Probabilistic Events and Its Relation to Logic Programming

Authors: Joost Vennekens, Marc Denecker, Maurice Bruynooghe

Abstract: This papers develops a logical language for representing probabilistic causal laws. Our interest in such a language is twofold. First, it can be motivated as a fundamental study of the representation of causal knowledge. Causality has an inherent dynamic aspect, which has been studied at the semantical level by Shafer in his framework of probability trees. In such a dynamic context, where the ev… ▽ More This papers develops a logical language for representing probabilistic causal laws. Our interest in such a language is twofold. First, it can be motivated as a fundamental study of the representation of causal knowledge. Causality has an inherent dynamic aspect, which has been studied at the semantical level by Shafer in his framework of probability trees. In such a dynamic context, where the evolution of a domain over time is considered, the idea of a causal law as something which guides this evolution is quite natural. In our formalization, a set of probabilistic causal laws can be used to represent a class of probability trees in a concise, flexible and modular way. In this way, our work extends Shafer's by offering a convenient logical representation for his semantical objects. Second, this language also has relevance for the area of probabilistic logic programming. In particular, we prove that the formal semantics of a theory in our language can be equivalently defined as a probability distribution over the well-founded models of certain logic programs, rendering it formally quite similar to existing languages such as ICL or PRISM. Because we can motivate and explain our language in a completely self-contained way as a representation of probabilistic causal laws, this provides a new way of explaining the intuitions behind such probabilistic logic programs: we can say precisely which knowledge such a program expresses, in terms that are equally understandable by a non-logician. Moreover, we also obtain an additional piece of knowledge representation methodology for probabilistic logic programs, by showing how they can express probabilistic causal laws. △ Less

Submitted 10 April, 2009; originally announced April 2009.

Comments: To be published in Theory and Practice of Logic Programming (TPLP)

ACM Class: I.2.4

Well-founded and Stable Semantics of Logic Programs with Aggregates

Authors: Nikolay Pelov, Marc Denecker, Maurice Bruynooghe

Abstract: In this paper, we present a framework for the semantics and the computation of aggregates in the context of logic programming. In our study, an aggregate can be an arbitrary interpreted second order predicate or function. We define extensions of the Kripke-Kleene, the well-founded and the stable semantics for aggregate programs. The semantics is based on the concept of a three-valued immediate c… ▽ More In this paper, we present a framework for the semantics and the computation of aggregates in the context of logic programming. In our study, an aggregate can be an arbitrary interpreted second order predicate or function. We define extensions of the Kripke-Kleene, the well-founded and the stable semantics for aggregate programs. The semantics is based on the concept of a three-valued immediate consequence operator of an aggregate program. Such an operator approximates the standard two-valued immediate consequence operator of the program, and induces a unique Kripke-Kleene model, a unique well-founded model and a collection of stable models. We study different ways of defining such operators and thus obtain a framework of semantics, offering different trade-offs between precision and tractability. In particular, we investigate conditions on the operator that guarantee that the computation of the three types of semantics remains on the same level as for logic programs without aggregates. Other results show that, in practice, even efficient three-valued immediate consequence operators which are very low in the precision hierarchy, still provide optimal precision. △ Less

Submitted 15 May, 2006; v1 submitted 8 September, 2005; originally announced September 2005.

Comments: 54 pages; To appear in Theory and Practice of Logic Programming (TPLP)

A Logic for Non-Monotone Inductive Definitions

Authors: Marc Denecker, Eugenia Ternovska

Abstract: Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-founded sets and iterated induction. In this work, we define a logic formalizing induction over well-founded sets and monotone and iterated induction. Just as the principle of positive induction has been formalized in FO(LFP), and the pri… ▽ More Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-founded sets and iterated induction. In this work, we define a logic formalizing induction over well-founded sets and monotone and iterated induction. Just as the principle of positive induction has been formalized in FO(LFP), and the principle of inflationary induction has been formalized in FO(IFP), this paper formalizes the principle of iterated induction in a new logic for Non-Monotone Inductive Definitions (ID-logic). The semantics of the logic is strongly influenced by the well-founded semantics of logic programming. Our main result concerns the modularity properties of inductive definitions in ID-logic. Specifically, we formulate conditions under which a simultaneous definition $\D$ of several relations is logically equivalent to a conjunction of smaller definitions $\D_1 \land ... \land \D_n$ with disjoint sets of defined predicates. The difficulty of the result comes from the fact that predicates $P_i$ and $P_j$ defined in $\D_i$ and $\D_j$, respectively, may be mutually connected by simultaneous induction. Since logic programming and abductive logic programming under well-founded semantics are proper fragments of our logic, our modularity results are applicable there as well. △ Less

Submitted 12 January, 2005; originally announced January 2005.

Comments: 50 pages, TOCL submission

Splitting an operator: Algebraic modularity results for logics with fixpoint semantics

Authors: Joost Vennekens, David Gilis, Marc Denecker

Abstract: It is well known that, under certain conditions, it is possible to split logic programs under stable model semantics, i.e. to divide such a program into a number of different "levels", such that the models of the entire program can be constructed by incrementally constructing models for each level. Similar results exist for other non-monotonic formalisms, such as auto-epistemic logic and default… ▽ More It is well known that, under certain conditions, it is possible to split logic programs under stable model semantics, i.e. to divide such a program into a number of different "levels", such that the models of the entire program can be constructed by incrementally constructing models for each level. Similar results exist for other non-monotonic formalisms, such as auto-epistemic logic and default logic. In this work, we present a general, algebraicsplitting theory for logics with a fixpoint semantics. Together with the framework of approximation theory, a general fixpoint theory for arbitrary operators, this gives us a uniform and powerful way of deriving splitting results for each logic with a fixpoint semantics. We demonstrate the usefulness of these results, by generalizing existing results for logic programming, auto-epistemic logic and default logic. △ Less

Submitted 26 October, 2006; v1 submitted 3 May, 2004; originally announced May 2004.

Comments: Revised to correct a substantial error in Section 4.2.2 (certain results which only hold for_consistent_ possible world sets were stated to hold in general)

ACM Class: I.2.3; I.2.4

Journal ref: ACM Transactions on Computational Logic, Volume 7, Number 4, 2006

Repairing Inconsistent Databases: A Model-Theoretic Approach and Abductive Reasoning

Authors: Ofer Arieli, Marc Denecker, Bert Van Nuffelen, Maurice Bruynooghe

Abstract: In this paper we consider two points of views to the problem of coherent integration of distributed data. First we give a pure model-theoretic analysis of the possible ways to `repair' a database. We do so by characterizing the possibilities to `recover' consistent data from an inconsistent database in terms of those models of the database that exhibit as minimal inconsistent information as reas… ▽ More In this paper we consider two points of views to the problem of coherent integration of distributed data. First we give a pure model-theoretic analysis of the possible ways to `repair' a database. We do so by characterizing the possibilities to `recover' consistent data from an inconsistent database in terms of those models of the database that exhibit as minimal inconsistent information as reasonably possible. Then we introduce an abductive application to restore the consistency of a given database. This application is based on an abductive solver (A-system) that implements an SLDNFA-resolution procedure, and computes a list of data-facts that should be inserted to the database or retracted from it in order to keep the database consistent. The two approaches for coherent data integration are related by soundness and completeness results. △ Less

Submitted 25 July, 2002; originally announced July 2002.

Comments: 15 pages. Originally published in proc. PCL 2002, a FLoC workshop; eds. Hendrik Decker, Dina Goldin, Jorgen Villadsen, Toshiharu Waragai (http://floc02.diku.dk/PCL/)

ACM Class: F.4.1; H.2.7; I.2.3

Ultimate approximations in nonmonotonic knowledge representation systems

Authors: Marc Denecker, Victor W. Marek, Miroslaw Truszczynski

Abstract: We study fixpoints of operators on lattices. To this end we introduce the notion of an approximation of an operator. We order approximations by means of a precision ordering. We show that each lattice operator O has a unique most precise or ultimate approximation. We demonstrate that fixpoints of this ultimate approximation provide useful insights into fixpoints of the operator O. We apply our… ▽ More We study fixpoints of operators on lattices. To this end we introduce the notion of an approximation of an operator. We order approximations by means of a precision ordering. We show that each lattice operator O has a unique most precise or ultimate approximation. We demonstrate that fixpoints of this ultimate approximation provide useful insights into fixpoints of the operator O. We apply our theory to logic programming and introduce the ultimate Kripke-Kleene, well-founded and stable semantics. We show that the ultimate Kripke-Kleene and well-founded semantics are more precise then their standard counterparts We argue that ultimate semantics for logic programming have attractive epistemological properties and that, while in general they are computationally more complex than the standard semantics, for many classes of theories, their complexity is no worse. △ Less

Submitted 11 May, 2002; originally announced May 2002.

Comments: This paper was published in Principles of Knowledge Representation and Reasoning, Proceedings of the Eighth International Conference (KR2002)

ACM Class: I.2.4

Abductive reasoning with temporal information

Authors: Sven Verdoolaege, Marc Denecker, Frank Van Eynde

Abstract: Texts in natural language contain a lot of temporal information, both explicit and implicit. Verbs and temporal adjuncts carry most of the explicit information, but for a full understanding general world knowledge and default assumptions have to be taken into account. We will present a theory for describing the relation between, on the one hand, verbs, their tenses and adjuncts and, on the other… ▽ More Texts in natural language contain a lot of temporal information, both explicit and implicit. Verbs and temporal adjuncts carry most of the explicit information, but for a full understanding general world knowledge and default assumptions have to be taken into account. We will present a theory for describing the relation between, on the one hand, verbs, their tenses and adjuncts and, on the other, the eventualities and periods of time they represent and their relative temporal locations, while allowing interaction with general world knowledge. The theory is formulated in an extension of first order logic and is a practical implementation of the concepts described in Van Eynde 2001 and Schelkens et al. 2000. We will show how an abductive resolution procedure can be used on this representation to extract temporal information from texts. The theory presented here is an extension of that in Verdoolaege et al. 2000, adapted to VanEynde 2001, with a simplified and extended analysis of adjuncts and with more emphasis on how a model can be constructed. △ Less

Submitted 23 November, 2000; originally announced November 2000.

Comments: 16 pages

ACM Class: I.2.4; I.2.7

Semantic interpretation of temporal information by abductive inference

Authors: Sven Verdoolaege, Marc Denecker, Ness Schelkens, Danny De Schreye, Frank Van Eynde

Abstract: Besides temporal information explicitly available in verbs and adjuncts, the temporal interpretation of a text also depends on general world knowledge and default assumptions. We will present a theory for describing the relation between, on the one hand, verbs, their tenses and adjuncts and, on the other, the eventualities and periods of time they represent and their relative temporal locations.… ▽ More Besides temporal information explicitly available in verbs and adjuncts, the temporal interpretation of a text also depends on general world knowledge and default assumptions. We will present a theory for describing the relation between, on the one hand, verbs, their tenses and adjuncts and, on the other, the eventualities and periods of time they represent and their relative temporal locations. The theory is formulated in logic and is a practical implementation of the concepts described in Ness Schelkens et al. We will show how an abductive resolution procedure can be used on this representation to extract temporal information from texts. △ Less

Submitted 22 November, 2000; originally announced November 2000.

Comments: 11 pages

ACM Class: I.2.4; I.2.7

Logic Programming Approaches for Representing and Solving Constraint Satisfaction Problems: A Comparison

Authors: Nikolay Pelov, Emmanuel De Mot, Marc Denecker

Abstract: Many logic programming based approaches can be used to describe and solve combinatorial search problems. On the one hand there is constraint logic programming which computes a solution as an answer substitution to a query containing the variables of the constraint satisfaction problem. On the other hand there are systems based on stable model semantics, abductive systems, and first order logic m… ▽ More Many logic programming based approaches can be used to describe and solve combinatorial search problems. On the one hand there is constraint logic programming which computes a solution as an answer substitution to a query containing the variables of the constraint satisfaction problem. On the other hand there are systems based on stable model semantics, abductive systems, and first order logic model generators which compute solutions as models of some theory. This paper compares these different approaches from the point of view of knowledge representation (how declarative are the programs) and from the point of view of performance (how good are they at solving typical problems). △ Less

Submitted 21 November, 2000; originally announced November 2000.

Comments: 15 pages, 3 eps-figures

ACM Class: I.2.3; I.2.4

Journal ref: LPAR 2000, Lecture Notes in Artificial Intelligence, vol. 1955, Springer, 2000, pp. 225-239

Detecting Unsolvable Queries for Definite Logic Programs

Authors: Maurice Bruynooghe, Henk Vandecasteele, D. Andre de Waal, Marc Denecker

Abstract: In solving a query, the SLD proof procedure for definite programs sometimes searches an infinite space for a non existing solution. For example, querying a planner for an unreachable goal state. Such programs motivate the development of methods to prove the absence of a solution. Considering the definite program and the query ``<- Q'' as clauses of a first order theory, one can apply model gener… ▽ More In solving a query, the SLD proof procedure for definite programs sometimes searches an infinite space for a non existing solution. For example, querying a planner for an unreachable goal state. Such programs motivate the development of methods to prove the absence of a solution. Considering the definite program and the query ``<- Q'' as clauses of a first order theory, one can apply model generators which search for a finite interpretation in which the program clauses as well as the clause ``false <- Q'' are true. This paper develops a new approach which exploits the fact that all clauses are definite. It is based on a goal directed abductive search in the space of finite pre-interpretations for a pre-interpretation such that ``Q'' is false in the least model of the program based on it. Several methods for efficiently searching the space of pre-interpretations are presented. Experimental results confirm that our approach find solutions with less search than with the use of a first order model generator. △ Less

Submitted 17 March, 2000; originally announced March 2000.

Comments: 32 pages including appendix. A preliminary version appeared in proceedings PLILP/ALP98 (Springer LNCS 1490) This version, without appendix appeared in Journal Functional and Logic Programming 1999

ACM Class: D.1.6; F.3.1; F.4.1

Journal ref: Journal of Functional and Logic Programming, Vol. 1999, 1-35, 1999

A note on the Declarative reading(s) of Logic Programming

Authors: Marc Denecker

Abstract: This paper analyses the declarative readings of logic programming. Logic programming - and negation as failure - has no unique declarative reading. One common view is that logic programming is a logic for default reasoning, a sub-formalism of default logic or autoepistemic logic. In this view, negation as failure is a modal operator. In an alternative view, a logic program is interpreted as a de… ▽ More This paper analyses the declarative readings of logic programming. Logic programming - and negation as failure - has no unique declarative reading. One common view is that logic programming is a logic for default reasoning, a sub-formalism of default logic or autoepistemic logic. In this view, negation as failure is a modal operator. In an alternative view, a logic program is interpreted as a definition. In this view, negation as failure is classical objective negation. From a commonsense point of view, there is definitely a difference between these views. Surprisingly though, both types of declarative readings lead to grosso modo the same model semantics. This note investigates the causes for this. △ Less

Submitted 13 March, 2000; originally announced March 2000.

Comments: 6 pages; poster at NMR2000, Breckenridge, April 2000

ACM Class: I.2.3; I.2.4; F.4.1

Problem solving in ID-logic with aggregates: some experiments

Authors: Bert Van Nuffelen, Marc Denecker

Abstract: The goal of the LP+ project at the K.U.Leuven is to design an expressive logic, suitable for declarative knowledge representation, and to develop intelligent systems based on Logic Programming technology for solving computational problems using the declarative specifications. The ID-logic is an integration of typed classical logic and a definition logic. Different abductive solvers for this lang… ▽ More The goal of the LP+ project at the K.U.Leuven is to design an expressive logic, suitable for declarative knowledge representation, and to develop intelligent systems based on Logic Programming technology for solving computational problems using the declarative specifications. The ID-logic is an integration of typed classical logic and a definition logic. Different abductive solvers for this language are being developed. This paper is a report of the integration of high order aggregates into ID-logic and the consequences on the solver SLDNFA. △ Less

Submitted 8 March, 2000; originally announced March 2000.

Comments: 9 pages conference: NMR2000, special track on abductive reasoning

ACM Class: F.4.1; I.2.4; I.2.3

Extending Classical Logic with Inductive Definitions

Authors: Marc Denecker

Abstract: The goal of this paper is to extend classical logic with a generalized notion of inductive definition supporting positive and negative induction, to investigate the properties of this logic, its relationships to other logics in the area of non-monotonic reasoning, logic programming and deductive databases, and to show its application for knowledge representation by giving a typology of definitio… ▽ More The goal of this paper is to extend classical logic with a generalized notion of inductive definition supporting positive and negative induction, to investigate the properties of this logic, its relationships to other logics in the area of non-monotonic reasoning, logic programming and deductive databases, and to show its application for knowledge representation by giving a typology of definitional knowledge. △ Less

Submitted 7 March, 2000; originally announced March 2000.

Comments: 9 pages to be presented at NMR2000, Breckenridge, April 2000

ACM Class: I.2.3; I.2.4; F.4.1

Uniform semantic treatment of default and autoepistemic logics

Authors: Marc Denecker, Victor W. Marek, Miroslaw Truszczynski

Abstract: We revisit the issue of connections between two leading formalisms in nonmonotonic reasoning: autoepistemic logic and default logic. For each logic we develop a comprehensive semantic framework based on the notion of a belief pair. The set of all belief pairs together with the so called knowledge ordering forms a complete lattice. For each logic, we introduce several semantics by means of fixpoi… ▽ More We revisit the issue of connections between two leading formalisms in nonmonotonic reasoning: autoepistemic logic and default logic. For each logic we develop a comprehensive semantic framework based on the notion of a belief pair. The set of all belief pairs together with the so called knowledge ordering forms a complete lattice. For each logic, we introduce several semantics by means of fixpoints of operators on the lattice of belief pairs. Our results elucidate an underlying isomorphism of the respective semantic constructions. In particular, we show that the interpretation of defaults as modal formulas proposed by Konolige allows us to represent all semantics for default logic in terms of the corresponding semantics for autoepistemic logic. Thus, our results conclusively establish that default logic can indeed be viewed as a fragment of autoepistemic logic. However, as we also demonstrate, the semantics of Moore and Reiter are given by different operators and occupy different locations in their corresponding families of semantics. This result explains the source of the longstanding difficulty to formally relate these two semantics. In the paper, we also discuss approximating skeptical reasoning with autoepistemic and default logics and establish constructive principles behind such approximations. △ Less

Submitted 3 February, 2000; originally announced February 2000.

Comments: Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning (KR2000); 11 pages

ACM Class: I.2.3; I.2.4

Journal ref: Artificial Intelligence Journal, 143 (2003), pp. 79--122

Fixpoint 3-valued semantics for autoepistemic logic

Authors: M. Denecker, V. Marek, M. Truszczynski

Abstract: The paper presents a constructive fixpoint semantics for autoepistemic logic (AEL). This fixpoint characterizes a unique but possibly three-valued belief set of an autoepistemic theory. It may be three-valued in the sense that for a subclass of formulas F, the fixpoint may not specify whether F is believed or not. The paper presents a constructive 3-valued semantics for autoepistemic logic (AEL)… ▽ More The paper presents a constructive fixpoint semantics for autoepistemic logic (AEL). This fixpoint characterizes a unique but possibly three-valued belief set of an autoepistemic theory. It may be three-valued in the sense that for a subclass of formulas F, the fixpoint may not specify whether F is believed or not. The paper presents a constructive 3-valued semantics for autoepistemic logic (AEL). We introduce a derivation operator and define the semantics as its least fixpoint. The semantics is 3-valued in the sense that, for some formulas, the least fixpoint does not specify whether they are believed or not. We show that complete fixpoints of the derivation operator correspond to Moore's stable expansions. In the case of modal representations of logic programs our least fixpoint semantics expresses well-founded semantics or 3-valued Fitting-Kunen semantics (depending on the embedding used). We show that, computationally, our semantics is simpler than the semantics proposed by Moore (assuming that the polynomial hierarchy does not collapse). △ Less

Submitted 12 January, 1999; originally announced January 1999.

Comments: Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI-98), pages 840--845, (MIT Press, 1998)

ACM Class: I.2.4, F.4.1, I.2.3