Showing 1–39 of 39 results for author: Bogaerts, B

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

Mathematical Foundations for Joining Only Knowing and Common Knowledge (Extended Version)

Authors: Marcos Cramer, Samuele Pollaci, Bart Bogaerts

Abstract: Common knowledge and only knowing capture two intuitive and natural notions that have proven to be useful in a variety of settings, for example to reason about coordination or agreement between agents, or to analyse the knowledge of knowledge-based agents. While these two epistemic operators have been extensively studied in isolation, the approaches made to encode their complex interplay failed to… ▽ More Common knowledge and only knowing capture two intuitive and natural notions that have proven to be useful in a variety of settings, for example to reason about coordination or agreement between agents, or to analyse the knowledge of knowledge-based agents. While these two epistemic operators have been extensively studied in isolation, the approaches made to encode their complex interplay failed to capture some essential properties of only knowing. We propose a novel solution by defining a notion of $μ$-biworld for countable ordinals $μ$, which approximates not only the worlds that an agent deems possible, but also those deemed impossible. This approach allows us to define a multi-agent epistemic logic with common knowledge and only knowing operators, and a three-valued model semantics for it. Moreover, we show that we only really need biworlds of depth at most $ω^2+1$. Based on this observation, we define a Kripke semantics on a canonical Kripke structure and show that this semantics coincides with the model semantics. Finally, we discuss issues arising when combining negative introspection or truthfulness with only knowing and show how positive introspection can be integrated into our logic. △ Less

Submitted 5 June, 2023; originally announced June 2023.

Comments: 18 pages, 2 figures, extended version of the paper "Mathematical Foundations for Joining Only Knowing and Common Knowledge'' accepted for KR 2023

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

Non-deterministic approximation operators: ultimate operators, semi-equilibrium semantics and aggregates (full version)

Authors: Jesse Heyninck, Bart Bogaerts

Abstract: Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of non-monotonic logics. In recent work, AFT was generalized to non-deterministic operators, i.e.\ operators whose range are sets of elements rather than single elements. In this paper, we make three further contributions to non-deterministic AFT: (1) we define and study ultimate approxima… ▽ More Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of non-monotonic logics. In recent work, AFT was generalized to non-deterministic operators, i.e.\ operators whose range are sets of elements rather than single elements. In this paper, we make three further contributions to non-deterministic AFT: (1) we define and study ultimate approximations of non-deterministic operators, (2) we give an algebraic formulation of the semi-equilibrium semantics by Amendola, et al., and (3) we generalize the characterisations of disjunctive logic programs to disjunctive logic programs with aggregates. △ Less

Submitted 18 May, 2023; originally announced May 2023.

Comments: Paper presented at the 39th International Conference on Logic Programming (ICLP 2023)

Preservation theorems for Tarski's relation algebra

Authors: Bart Bogaerts, Balder ten Cate, Brett McLean, Jan Van den Bussche

Abstract: We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain several positive and negative results along these lines. Specifically, the homomorphism-safe fragment is finitely generated (both over finite and over arbitrary stru… ▽ More We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain several positive and negative results along these lines. Specifically, the homomorphism-safe fragment is finitely generated (both over finite and over arbitrary structures). The function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable function-preserving operations). Similarly, the total-function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable total-function-preserving operations). In contrast, the forward-looking function-preserving fragment is finitely generated by composition, intersection, antidomain, and preferential union. Similarly, the forward-and-backward-looking injective-function-preserving fragment is finitely generated by composition, intersection, antidomain, inverse, and an `injective union' operation. △ Less

Submitted 11 April, 2024; v1 submitted 8 May, 2023; originally announced May 2023.

Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)

Authors: Emilio Gamba, Bart Bogaerts, Tias Guns

Abstract: We build on a recently proposed method for stepwise explaining solutions of Constraint Satisfaction Problems (CSP) in a human-understandable way. An explanation here is a sequence of simple inference steps where simplicity is quantified using a cost function. The algorithms for explanation generation rely on extracting Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploit… ▽ More We build on a recently proposed method for stepwise explaining solutions of Constraint Satisfaction Problems (CSP) in a human-understandable way. An explanation here is a sequence of simple inference steps where simplicity is quantified using a cost function. The algorithms for explanation generation rely on extracting Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called non-redundant explanations and MUSs. However, MUS extraction algorithms do not provide any guarantee of subset minimality or optimality with respect to a given cost function. Therefore, we build on these formal foundations and tackle the main points of improvement, namely how to generate explanations efficiently that are provably optimal (with respect to the given cost metric). For that, we developed (1) a hitting set-based algorithm for finding the optimal constrained unsatisfiable subsets; (2) a method for re-using relevant information over multiple algorithm calls; and (3) methods exploiting domain-specific information to speed up the explanation sequence generation. We experimentally validated our algorithms on a large number of CSP problems. We found that our algorithms outperform the MUS approach in terms of explanation quality and computational time (on average up to 56 % faster than a standard MUS approach). △ Less

Submitted 28 November, 2023; v1 submitted 21 March, 2023; originally announced March 2023.

Comments: arXiv admin note: text overlap with arXiv:2105.11763

Report number: 78, 2023 MSC Class: 68T27 ACM Class: F.4.1

Journal ref: Journal of Artificial Intelligence Research (JAIR) Volume 78 (2023): pages 709-746

Distributed Subweb Specifications for Traversing the Web

Authors: Bart Bogaerts, Bas Ketsman, Younes Zeboudj, Heba Aamer, Ruben Taelman, Ruben Verborgh

Abstract: Link Traversal-based Query Processing (ltqp), in which a sparql query is evaluated over a web of documents rather than a single dataset, is often seen as a theoretically interesting yet impractical technique. However, in a time where the hypercentralization of data has increasingly come under scrutiny, a decentralized Web of Data with a simple document-based interface is appealing, as it enables d… ▽ More Link Traversal-based Query Processing (ltqp), in which a sparql query is evaluated over a web of documents rather than a single dataset, is often seen as a theoretically interesting yet impractical technique. However, in a time where the hypercentralization of data has increasingly come under scrutiny, a decentralized Web of Data with a simple document-based interface is appealing, as it enables data publishers to control their data and access rights. While ltqp allows evaluating complex queries over such webs, it suffers from performance issues (due to the high number of documents containing data) as well as information quality concerns (due to the many sources providing such documents). In existing ltqp approaches, the burden of finding sources to query is entirely in the hands of the data consumer. In this paper, we argue that to solve these issues, data publishers should also be able to suggest sources of interest and guide the data consumer towards relevant and trustworthy data. We introduce a theoretical framework that enables such guided link traversal and study its properties. We illustrate with a theoretic example that this can improve query results and reduce the number of network requests. We evaluate our proposal experimentally on a virtual linked web with specifications and indeed observe that not just the data quality but also the efficiency of querying improves. Under consideration in Theory and Practice of Logic Programming (TPLP). △ Less

Submitted 27 March, 2023; v1 submitted 28 February, 2023; originally announced February 2023.

Comments: Under consideration in Theory and Practice of Logic Programming (TPLP)

Expressiveness of SHACL Features and Extensions for Full Equality and Disjointness Tests

Authors: Bart Bogaerts, Maxime Jakubowski, Jan Van den Bussche

Abstract: SHACL is a W3C-proposed schema language for expressing structural constraints on RDF graphs. Recent work on formalizing this language has revealed a striking relationship to description logics. SHACL expressions can use three fundamental features that are not so common in description logics. These features are equality tests; disjointness tests; and closure constraints. Moreover, SHACL is peculiar… ▽ More SHACL is a W3C-proposed schema language for expressing structural constraints on RDF graphs. Recent work on formalizing this language has revealed a striking relationship to description logics. SHACL expressions can use three fundamental features that are not so common in description logics. These features are equality tests; disjointness tests; and closure constraints. Moreover, SHACL is peculiar in allowing only a restricted form of expressions (so-called targets) on the left-hand side of inclusion constraints. The goal of this paper is to obtain a clear picture of the impact and expressiveness of these features and restrictions. We show that each of the four features is primitive: using the feature, one can express boolean queries that are not expressible without using the feature. We also show that the restriction that SHACL imposes on allowed targets is inessential, as long as closure constraints are not used. In addition, we show that enriching SHACL with "full" versions of equality tests, or disjointness tests, results in a strictly more powerful language. △ Less

Submitted 20 February, 2024; v1 submitted 7 December, 2022; originally announced December 2022.

Journal ref: Logical Methods in Computer Science (February 28, 2024) lmcs:10442

Non-Deterministic Approximation Fixpoint Theory and Its Application in Disjunctive Logic Programming

Authors: Jesse Heyninck, Ofer Arieli, Bart Bogaerts

Abstract: Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of nonmonotonic logics. It provides a unifying study of the semantics of different formalisms for nonmonotonic reasoning, such as logic programming, default logic and autoepistemic logic. In this paper, we extend AFT to dealing with non-deterministic constructs that allow to handle indefin… ▽ More Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of nonmonotonic logics. It provides a unifying study of the semantics of different formalisms for nonmonotonic reasoning, such as logic programming, default logic and autoepistemic logic. In this paper, we extend AFT to dealing with non-deterministic constructs that allow to handle indefinite information, represented e.g. by disjunctive formulas. This is done by generalizing the main constructions and corresponding results of AFT to non-deterministic operators, whose ranges are sets of elements rather than single elements. The applicability and usefulness of this generalization is illustrated in the context of disjunctive logic programming. △ Less

Submitted 1 December, 2022; v1 submitted 30 November, 2022; originally announced November 2022.

Executable First-Order Queries in the Logic of Information Flows

Authors: Heba Aamer, Bart Bogaerts, Dimitri Surinx, Eugenia Ternovska, Jan Van den Bussche

Abstract: The logic of information flows (LIF) has recently been proposed as a general framework in the field of knowledge representation. In this framework, tasks of procedural nature can still be modeled in a declarative, logic-based fashion. In this paper, we focus on the task of query processing under limited access patterns, a well-studied problem in the database literature. We show that LIF is well-su… ▽ More The logic of information flows (LIF) has recently been proposed as a general framework in the field of knowledge representation. In this framework, tasks of procedural nature can still be modeled in a declarative, logic-based fashion. In this paper, we focus on the task of query processing under limited access patterns, a well-studied problem in the database literature. We show that LIF is well-suited for modeling this task. Toward this goal, we introduce a variant of LIF called "forward" LIF (FLIF), in a first-order setting. FLIF takes a novel graph-navigational approach; it is an XPath-like language that nevertheless turns out to be equivalent to the "executable" fragment of first-order logic defined by Nash and Ludäscher. One can also classify the variables in FLIF expressions as inputs and outputs. Expressions where inputs and outputs are disjoint, referred to as io-disjoint FLIF expressions, allow a particularly transparent translation into algebraic query plans that respect the access limitations. Finally, we show that general FLIF expressions can always be put into io-disjoint form. △ Less

Submitted 21 May, 2024; v1 submitted 1 October, 2022; originally announced October 2022.

ACM Class: H.2.3; I.2.4

Inputs, Outputs, and Composition in the Logic of Information Flows

Authors: Heba Aamer, Bart Bogaerts, Dimitri Surinx, Eugenia Ternovska, Jan Van den Bussche

Abstract: The logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. The first contribution of this paper is to propose semantic and syntactic definitions of inputs and outputs of LIF expressions. We study how the two relate and show that our syntactic definition is optimal in a sense that is made precise. The secon… ▽ More The logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. The first contribution of this paper is to propose semantic and syntactic definitions of inputs and outputs of LIF expressions. We study how the two relate and show that our syntactic definition is optimal in a sense that is made precise. The second contribution is a systematic study of the expressive power of sequential composition in LIF. Our results on composition tie in the results on inputs and outputs, and relate LIF to first-order logic (FO) and bounded-variable LIF to bounded-variable FO. △ Less

Submitted 14 September, 2022; originally announced September 2022.

Comments: This paper is the extended version of a paper presented at KR 2020

Tree-Like Justification Systems are Consistent

Authors: Simon Marynissen, Bart Bogaerts

Abstract: Justification theory is an abstract unifying formalism that captures semantics of various non-monotonic logics. One intriguing problem that has received significant attention is the consistency problem: under which conditions are justifications for a fact and justifications for its negation suitably related. Two variants of justification theory exist: one in which justifications are trees and one… ▽ More Justification theory is an abstract unifying formalism that captures semantics of various non-monotonic logics. One intriguing problem that has received significant attention is the consistency problem: under which conditions are justifications for a fact and justifications for its negation suitably related. Two variants of justification theory exist: one in which justifications are trees and one in which they are graphs. In this work we resolve the consistency problem once and for all for the tree-like setting by showing that all reasonable tree-like justification systems are consistent. △ Less

Submitted 5 August, 2022; originally announced August 2022.

Comments: In Proceedings ICLP 2022, arXiv:2208.02685

Journal ref: EPTCS 364, 2022, pp. 1-11

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

Certified Symmetry and Dominance Breaking for Combinatorial Optimisation

Authors: Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström

Abstract: Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method… ▽ More Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes XOR and cardinality reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems. △ Less

Submitted 16 August, 2023; v1 submitted 23 March, 2022; originally announced March 2022.

Comments: This paper was published in the Journal of Artificial Intelligence Research https://doi.org/10.1613/jair.1.14296 It is an extended version of our (equally-named) paper to appear in the proceedings of AAAI 2022 https://ojs.aaai.org/index.php/AAAI/article/view/20283

Journal ref: Journal of Artificial Intelligence Research, volume 77: pages 1539-1589, 2023

Fixpoint Semantics for Recursive SHACL

Authors: Bart Bogaerts, Maxime Jakubowski

Abstract: SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. The recommendation only specifies semantics for non-recursive SHACL; recently, some efforts have been made to allow recursive SHACL schemas. In this paper, we argue that for defining and studying semantics of recursive SHACL, lessons can be learned from years of research in non-monotonic reasoning. We show tha… ▽ More SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. The recommendation only specifies semantics for non-recursive SHACL; recently, some efforts have been made to allow recursive SHACL schemas. In this paper, we argue that for defining and studying semantics of recursive SHACL, lessons can be learned from years of research in non-monotonic reasoning. We show that from a SHACL schema, a three-valued semantic operator can directly be obtained. Building on Approximation Fixpoint Theory (AFT), this operator immediately induces a wide variety of semantics, including a supported, stable, and well-founded semantics, related in the expected ways. By building on AFT, a rich body of theoretical results becomes directly available for SHACL. As such, the main contribution of this short paper is providing theoretical foundations for the study of recursive SHACL, which can later enable an informed decision for an extension of the W3C recommendation. △ Less

Submitted 16 September, 2021; originally announced September 2021.

Comments: In Proceedings ICLP 2021, arXiv:2109.07914

Journal ref: EPTCS 345, 2021, pp. 41-47

Proceedings 37th International Conference on Logic Programming (Technical Communications)

Authors: Andrea Formisano, Yanhong Annie Liu, Bart Bogaerts, Alex Brik, Veronica Dahl, Carmine Dodaro, Paul Fodor, Gian Luca Pozzato, Joost Vennekens, Neng-Fa Zhou

Abstract: ICLP is the premier international event for presenting research in logic programming. Contributions to ICLP 2021 were sought in all areas of logic programming, including but not limited to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages issues: Concurrency, Objects, Coordination, Mobility, Higher order, Types, Modes, Assertions, Modules, Meta-… ▽ More ICLP is the premier international event for presenting research in logic programming. Contributions to ICLP 2021 were sought in all areas of logic programming, including but not limited to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages issues: Concurrency, Objects, Coordination, Mobility, Higher order, Types, Modes, Assertions, Modules, Meta-programming, Logic-based domain-specific languages, Programming techniques. Programming support: Program analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing, Execution visualization. Implementation: Compilation, Virtual machines, Memory management, Parallel and Distributed execution, Constraint handling rules, Tabling, Foreign interfaces, User interfaces. Related Paradigms and Synergies: Inductive and coinductive logic programming, Constraint logic programming, Answer set programming, Interaction with SAT, SMT and CSP solvers, Theorem proving, Argumentation, Probabilistic programming, Machine learning. Applications: Databases, Big data, Data integration and federation, Software engineering, Natural language processing, Web and semantic web, Agents, Artificial intelligence, Computational life sciences, Cyber-security, Robotics, Education. △ Less

Submitted 14 September, 2021; originally announced September 2021.

Journal ref: EPTCS 345, 2021

SHACL: A Description Logic in Disguise

Authors: Bart Bogaerts, Maxime Jakubowski, Jan Van den Bussche

Abstract: SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. In recent years, SHACL's popularity has risen quickly. This rise in popularity comes with questions related to its place in the semantic web, particularly about its relation to OWL (the de facto standard for expressing ontological information on the web) and description logics (which form the formal foundations o… ▽ More SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. In recent years, SHACL's popularity has risen quickly. This rise in popularity comes with questions related to its place in the semantic web, particularly about its relation to OWL (the de facto standard for expressing ontological information on the web) and description logics (which form the formal foundations of OWL). We answer these questions by arguing that SHACL is in fact a description logic. On the one hand, our answer is surprisingly simple, some might even say obvious. But, on the hand, our answer is also controversial. By resolving this issue once and for all, we establish the field of description logics as the solid formal foundations of SHACL. △ Less

Submitted 28 June, 2022; v1 submitted 13 August, 2021; originally announced August 2021.

Comments: Presented at LPNRM conference 2022

Efficiently Explaining CSPs with Unsatisfiable Subset Optimization

Authors: Emilio Gamba, Bart Bogaerts, Tias Guns

Abstract: We build on a recently proposed method for explaining solutions of constraint satisfaction problems. An explanation here is a sequence of simple inference steps, where the simplicity of an inference step is measured by the number and types of constraints and facts used, and where the sequence explains all logical consequences of the problem. We build on these formal foundations and tackle two emer… ▽ More We build on a recently proposed method for explaining solutions of constraint satisfaction problems. An explanation here is a sequence of simple inference steps, where the simplicity of an inference step is measured by the number and types of constraints and facts used, and where the sequence explains all logical consequences of the problem. We build on these formal foundations and tackle two emerging questions, namely how to generate explanations that are provably optimal (with respect to the given cost metric) and how to generate them efficiently. To answer these questions, we develop 1) an implicit hitting set algorithm for finding optimal unsatisfiable subsets; 2) a method to reduce multiple calls for (optimal) unsatisfiable subsets to a single call that takes constraints on the subset into account, and 3) a method for re-using relevant information over multiple calls to these algorithms. The method is also applicable to other problems that require finding cost-optimal unsatiable subsets. We specifically show that this approach can be used to effectively find sequences of optimal explanation steps for constraint satisfaction problems like logic grid puzzles. △ Less

Submitted 5 July, 2021; v1 submitted 25 May, 2021; originally announced May 2021.

MSC Class: 68T27 ACM Class: F.4.1

LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

Authors: Wolf De Wulf, Bart Bogaerts

Abstract: Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP… ▽ More Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP programs into pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane-based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean solving. Our results are mixed: overall, traditional ASP solvers still outperform our translational approach, but several benchmark families are identified where the balance shifts the other way, thereby suggesting that further investigation into a stronger proof system for ASP is valuable. △ Less

Submitted 21 September, 2020; originally announced September 2020.

Comments: In Proceedings ICLP 2020, arXiv:2009.09158

ACM Class: I.2.8; I.2.4; D.3.2; I.2.3

Journal ref: EPTCS 325, 2020, pp. 206-219

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

A framework for step-wise explaining how to solve constraint satisfaction problems

Authors: Bart Bogaerts, Emilio Gamba, Tias Guns

Abstract: We explore the problem of step-wise explaining how to solve constraint satisfaction problems, with a use case on logic grid puzzles. More specifically, we study the problem of explaining the inference steps that one can take during propagation, in a way that is easy to interpret for a person. Thereby, we aim to give the constraint solver explainable agency, which can help in building trust in the… ▽ More We explore the problem of step-wise explaining how to solve constraint satisfaction problems, with a use case on logic grid puzzles. More specifically, we study the problem of explaining the inference steps that one can take during propagation, in a way that is easy to interpret for a person. Thereby, we aim to give the constraint solver explainable agency, which can help in building trust in the solver by being able to understand and even learn from the explanations. The main challenge is that of finding a sequence of simple explanations, where each explanation should aim to be as cognitively easy as possible for a human to verify and understand. This contrasts with the arbitrary combination of facts and constraints that the solver may use when propagating. We propose the use of a cost function to quantify how simple an individual explanation of an inference step is, and identify the explanation-production problem of finding the best sequence of explanations of a CSP. Our approach is agnostic of the underlying constraint propagation mechanisms, and can provide explanations even for inference steps resulting from combinations of constraints. In case multiple constraints are involved, we also develop a mechanism that allows to break the most difficult steps up and thus gives the user the ability to zoom in on specific parts of the explanation. Our proposed algorithm iteratively constructs the explanation sequence by using an optimistic estimate of the cost function to guide the search for the best explanation at each step. Our experiments on logic grid puzzles show the feasibility of the approach in terms of the quality of the individual explanations and the resulting explanation sequences obtained. △ Less

Submitted 11 June, 2020; originally announced June 2020.

MSC Class: 68T27 ACM Class: F.4.1

Proceedings 35th International Conference on Logic Programming (Technical Communications)

Authors: Bart Bogaerts, Esra Erdem, Paul Fodor, Andrea Formisano, Giovambattista Ianni, Daniela Inclezan, German Vidal, Alicia Villanueva, Marina De Vos, Fangkai Yang

Abstract: Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages: Concurrency, Objects, Coordination, Mobility, Higher Order,… ▽ More Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Modules, Meta-programming, Logic-based domain-specific languages, Programming Techniques. Declarative programming: Declarative program development, Analysis, Type and mode inference, Partial evaluation, Abstract interpretation, Transformation, Validation, Verification, Debugging, Profiling, Testing, Execution visualization Implementation: Virtual machines, Compilation, Memory management, Parallel/distributed execution, Constraint handling rules, Tabling, Foreign interfaces, User interfaces. Related Paradigms and Synergies: Inductive and Co-inductive Logic Programming, Constraint Logic Programming, Answer Set Programming, Interaction with SAT, SMT and CSP solvers, Logic programming techniques for type inference and theorem proving, Argumentation, Probabilistic Logic Programming, Relations to object-oriented and Functional programming. Applications: Databases, Big Data, Data integration and federation, Software engineering, Natural language processing, Web and Semantic Web, Agents, Artificial intelligence, Computational life sciences, Education, Cybersecurity, and Robotics. △ Less

Submitted 17 September, 2019; originally announced September 2019.

Journal ref: EPTCS 306, 2019

Enabling Humans to Plan Inspection Paths Using a Virtual Reality Interface

Authors: Boris Bogaerts, Seppe Sels, Steve Vanlanduit, Rudi Penne

Abstract: In this work, we investigate whether humans can manually generate high-quality robot paths for optical inspections. Typically, automated algorithms are used to solve the inspection planning problem. The use of automated algorithms implies that specialized knowledge from users is needed to set up the algorithm. We aim to replace this need for specialized experience, by entrusting a non-expert human… ▽ More In this work, we investigate whether humans can manually generate high-quality robot paths for optical inspections. Typically, automated algorithms are used to solve the inspection planning problem. The use of automated algorithms implies that specialized knowledge from users is needed to set up the algorithm. We aim to replace this need for specialized experience, by entrusting a non-expert human user with the planning task. We augment this user with intuitive visualizations and interactions in virtual reality. To investigate if humans can generate high-quality inspection paths, we perform a user study in which users from different experience categories, generate inspection paths with the proposed virtual reality interface. From our study, it can be concluded that users without experience can generate high-quality inspection paths: The median inspection quality of user generated paths ranged between 66-81\% of the quality of a state-of-the-art automated algorithm on various inspection planning scenarios. We noticed however, a sizable variation in the performance of users, which is a result of some typical user behaviors. These behaviors are discussed, and possible solutions are provided. △ Less

Submitted 13 September, 2019; originally announced September 2019.

Near-Optimal Path Planning for Complex Robotic Inspection Tasks

Authors: Boris Bogaerts, Seppe Sels, Steve Vanlanduit, Rudi Penne

Abstract: In this paper, we consider the problem of generating inspection paths for robots. These paths should allow an attached measurement device to perform high-quality measurements. We formally show that generating robot paths, while maximizing the inspection quality, naturally corresponds to the submodular orienteering problem. Traditional methods that are able to generate solutions with mathematical g… ▽ More In this paper, we consider the problem of generating inspection paths for robots. These paths should allow an attached measurement device to perform high-quality measurements. We formally show that generating robot paths, while maximizing the inspection quality, naturally corresponds to the submodular orienteering problem. Traditional methods that are able to generate solutions with mathematical guarantees do not scale to real-world problems. In this work, we propose a method that is able to generate near-optimal solutions for real-world complex problems. We experimentally test this method in a wide variety of inspection problems and show that it nearly always outperforms traditional methods. We furthermore show that the near-optimality of our approach makes it more robust to changing the inspection problem, and is thus more general. △ Less

Submitted 14 May, 2019; originally announced May 2019.

Interactive Camera Network Design using a Virtual Reality Interface

Authors: Boris Bogaerts, Seppe Sels, Steve Vanlanduit, Rudi Penne

Abstract: Traditional literature on camera network design focuses on constructing automated algorithms. These require problem specific input from experts in order to produce their output. The nature of the required input is highly unintuitive leading to an unpractical workflow for human operators. In this work we focus on develo** a virtual reality user interface allowing human operators to manually desig… ▽ More Traditional literature on camera network design focuses on constructing automated algorithms. These require problem specific input from experts in order to produce their output. The nature of the required input is highly unintuitive leading to an unpractical workflow for human operators. In this work we focus on develo** a virtual reality user interface allowing human operators to manually design camera networks in an intuitive manner. From real world practical examples we conclude that the camera networks designed using this interface are highly competitive with, or superior to those generated by automated algorithms, but the associated workflow is much more intuitive and simple. The competitiveness of the human-generated camera networks is remarkable because the structure of the optimization problem is a well known combinatorial NP-hard problem. These results indicate that human operators can be used in challenging geometrical combinatorial optimization problems given an intuitive visualization of the problem. △ Less

Submitted 20 September, 2018; originally announced September 2018.

Comments: 11 pages, 8 figures

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.

BreakID: Static Symmetry Breaking for ASP (System Description)

Authors: Jo Devriendt, Bart Bogaerts

Abstract: Symmetry breaking has been proven to be an efficient preprocessing technique for satisfiability solving (SAT). In this paper, we port the state-of-the-art SAT symmetry breaker BreakID to answer set programming (ASP). The result is a lightweight tool that can be plugged in between the grounding and the solving phases that are common when modelling in ASP. We compare our tool with sbass, the current… ▽ More Symmetry breaking has been proven to be an efficient preprocessing technique for satisfiability solving (SAT). In this paper, we port the state-of-the-art SAT symmetry breaker BreakID to answer set programming (ASP). The result is a lightweight tool that can be plugged in between the grounding and the solving phases that are common when modelling in ASP. We compare our tool with sbass, the current state-of-the-art symmetry breaker for ASP. △ Less

Submitted 30 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

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)

Stable-Unstable Semantics: Beyond NP with Normal Logic Programs

Authors: Bart Bogaerts, Tomi Janhunen, Shahab Tasharrofi

Abstract: Standard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of disjunctive logic programs offers the most prominent way of reaching the second level of the PH, but encoding respective hard problems as disjunctive programs typically requires sophis… ▽ More Standard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of disjunctive logic programs offers the most prominent way of reaching the second level of the PH, but encoding respective hard problems as disjunctive programs typically requires sophisticated techniques such as saturation or meta-interpretation. The application of such techniques easily leads to encodings that are inaccessible to non-experts. Furthermore, while disjunctive ASP solvers often rely on calls to a (co-)NP oracle, it may be difficult to detect from the input program where the oracle is being accessed. In other formalisms, such as Quantified Boolean Formulas (QBFs), the interface to the underlying oracle is more transparent as it is explicitly recorded in the quantifier prefix of a formula. On the other hand, ASP has advantages over QBFs from the modeling perspective. The rich high-level languages such as ASP-Core-2 offer a wide variety of primitives that enable concise and natural encodings of search problems. In this paper, we present a novel logic programming--based modeling paradigm that combines the best features of ASP and QBFs. We develop so-called combined logic programs in which oracles are directly cast as (normal) logic programs themselves. Recursive incarnations of this construction enable logic programming on arbitrarily high levels of the PH. We develop a proof-of-concept implementation for our new paradigm. This paper is under consideration for acceptance in TPLP. △ Less

Submitted 15 August, 2016; v1 submitted 5 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, 16 pages, LaTeX, no figures

MSC Class: 68T30 ACM Class: D.1.6; F.4.1; I.2.3

Propagators and Solvers for the Algebra of Modular Systems

Authors: Bart Bogaerts, Eugenia Ternovska, David Mitchell

Abstract: To appear in the proceedings of LPAR 21. Solving complex problems can involve non-trivial combinations of distinct knowledge bases and problem solvers. The Algebra of Modular Systems is a knowledge representation framework that provides a method for formally specifying such systems in purely semantic terms. Formally, an expression of the algebra defines a class of structures. Many expressive for… ▽ More To appear in the proceedings of LPAR 21. Solving complex problems can involve non-trivial combinations of distinct knowledge bases and problem solvers. The Algebra of Modular Systems is a knowledge representation framework that provides a method for formally specifying such systems in purely semantic terms. Formally, an expression of the algebra defines a class of structures. Many expressive formalism used in practice solve the model expansion task, where a structure is given on the input and an expansion of this structure in the defined class of structures is searched (this practice overcomes the common undecidability problem for expressive logics). In this paper, we construct a solver for the model expansion task for a complex modular systems from an expression in the algebra and black-box propagators or solvers for the primitive modules. To this end, we define a general notion of propagators equipped with an explanation mechanism, an extension of the alge- bra to propagators, and a lazy conflict-driven learning algorithm. The result is a framework for seamlessly combining solving technology from different domains to produce a solver for a combined system. △ Less

Submitted 3 April, 2017; v1 submitted 27 June, 2016; originally announced June 2016.

Comments: To appear in the proceedings of LPAR 21

Knowledge Compilation of Logic Programs Using Approximation Fixpoint Theory

Authors: Bart Bogaerts, Guy Van den Broeck

Abstract: To appear in Theory and Practice of Logic Programming (TPLP), Proceedings of ICLP 2015 Recent advances in knowledge compilation introduced techniques to compile \emph{positive} logic programs into propositional logic, essentially exploiting the constructive nature of the least fixpoint computation. This approach has several advantages over existing approaches: it maintains logical equivalence, d… ▽ More To appear in Theory and Practice of Logic Programming (TPLP), Proceedings of ICLP 2015 Recent advances in knowledge compilation introduced techniques to compile \emph{positive} logic programs into propositional logic, essentially exploiting the constructive nature of the least fixpoint computation. This approach has several advantages over existing approaches: it maintains logical equivalence, does not require (expensive) loop-breaking preprocessing or the introduction of auxiliary variables, and significantly outperforms existing algorithms. Unfortunately, this technique is limited to \emph{negation-free} programs. In this paper, we show how to extend it to general logic programs under the well-founded semantics. We develop our work in approximation fixpoint theory, an algebraical framework that unifies semantics of different logics. As such, our algebraical results are also applicable to autoepistemic logic, default logic and abstract dialectical frameworks. △ Less

Submitted 23 July, 2015; originally announced July 2015.

Journal ref: Theory and Practice of Logic Programming 15 (2015) 464-480

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)

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)

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.

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