Title Participants Abstract "Towards Systematic Treatment of Partial Functions in Knowledge Representation" "Dorde Markovic, Maurice Bruynooghe, Marc Denecker" "Partial functions are ubiquitous in Knowledge Representation applications, ranging from practical, e.g., business applications, to more abstract, e.g., mathematical and programming applications. Expressing propositions about partial functions may lead to non/denoting terms resulting in undefinedness errors and ambiguity, causing subtle modeling and reasoning problems. In our approach, formulas are well-defined (true or false) and non/ambiguous in all structures. We develop a base extension of three/valued predicate logic, in which partial function terms are guarded by domain expressions ensuring the well/definedness property despite the three/valued nature of the underlying logic. To tackle the verbosity of this core language, we propose different ways to increase convenience by using disambiguating annotations and non/commutative connectives. We show a reduction of the logic to two/valued logic of total functions and prove that many different unnesting methods turning partial functions into graph predicates, which are not equivalence preserving in general, are equivalence preserving in the proposed language, showing that ambiguity is avoided." "Justifications and a Reconstruction of Parity Game Solving Algorithms" "Ruben Lapauw, Maurice Bruynooghe, Marc Denecker" "On the semantics of ""null"" in DMN: Undefined is not unknown" "Dorde Markovic, Simon Vandevelde, Joost Vennekens, Marc Denecker" "Decision Model and Notation (DMN) is a formalism for the representation of knowledge about decision processes. It represents a set of decision rules in an easy-to-understand tabular format, called a decision table. In this paper, we argue that current formal semantics for DMN have certain limitations and we propose a novel formal semantics. Our semantics considers a decision table as a definition. The semantics consists of two components: the first component captures the meaning of one row (rule), and the second component aggregates the meaning of the rules into meaning for the whole table. By choosing the second component in different ways, the different ""hit policies"" of DMN (i.e., mechanisms for deciding what happens when multiple rows of the same table are applicable) can be represented. Our semantics can cope better with undefined and unknown values and provides a foundation for forms of reasoning different from deriving the output for a given set of inputs." "On Nested Justification Systems" "Marc Denecker" "On the Relation Between Approximation Fixpoint Theory and Justification Theory" "Simon Marynissen, Marc Denecker" "Approximation Fixpoint Theory (AFT) and Justification Theory (JT) are two frameworks to unify logical formalisms. AFT studies semantics in terms of fixpoints of lattice operators, and JT in terms of so-called justifications, which are explanations of why certain facts do or do not hold in a model. While the approaches differ, the frameworks were designed with similar goals in mind, namely to study the different semantics that arise in (mainly) non-monotonic logics. The First contribution of our current paper is to provide a formal link between the two frameworks. To be precise, we show that every justification frame induces an approximator and that this mapping from JT to AFT preserves all major semantics. The second contribution exploits this correspondence to extend JT with a novel class of semantics, namely ultimate semantics: we formally show that ultimate semantics can be obtained in JT by a syntactic transformation on the justification frame, essentially performing some sort of resolution on the rules." "Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory" "Linde Vanbesien, Maurice Bruynooghe, Marc Denecker" "Reconstructing and Improving Parity Game Solvers with Justifications" "Ruben Lapauw" "In certain industries, such as medical or aerospace, failure can result inunacceptable losses. To ensure safety, checks are implemented for every stepin the process: standards, certifications, testing, maintenance schedules. . . Forsoftware, this encompasses researching diverse approaches including automatictesting, safer programming languages, declarative languages to separateknowledge from execution, or generating provably correct software from alist of expected behaviours.This thesis is situated in the domains exploring the two last ideas: KnowledgeRepresentation and Reasoning (KRR) and Formal Verification (FV). KRRresearches how knowledge can be represented for humans while supporting(automatic) reasoning with this knowledge. Formal Verification focuses onmodelling the behaviour of systems, verifying correct behaviour in all relevantscenarios.One technique, used in KRR for improving reasoning capabilities of algorithms,is called justifications. Justifications store how consequences were derived in agraph used for tracing unsupported arguments when invalidating assumptions.This text explores how justifications improve parity game algorithms, which playa central role in FV. A parity game is an infinite two-player game on a directedgraph. The core problem of a parity game is deciding the winner of certainnodes and a corresponding strategy. The solution of a parity game informswhether an implementation is valid or allows extracting a valid implementation.First, justifications are adapted to parity games. We introduce an operationJustify to manipulate justifications for solving parity games. Then, four well-known recursive algorithms are reconstructed using this operation. Thesenew variants are also implemented and evaluated experimentally and showjustifications improve the state-of-the-art algorithms. Finally, we show thatjustifications for parity games are equivalent to justifications for propositionalnested fixpoint definitions, an older logic with different applications." "Exploiting Game Theory for Analysing Justifications" "Simon Marynissen, Marc Denecker" "Improving Parity Game Solvers with Justifications" "Ruben Lapauw, Maurice Bruynooghe, Marc Denecker" "Parity games are infinite two-player games played on node-weighted directed graphs. Formal verification problems such as verifying and synthesizing automata, bounded model checking of LTL, CTL*, propositional µ-calculus, ...reduce to problems over parity games. The core problem of parity game solving is deciding the winner of some (or all) nodes in a parity game. In this paper, we improve several parity game solvers by using a justification graph. Experimental evaluation shows our algorithms improve upon the state-of-the-art." "Knowledge Representation Analysis of Graph Mining" "Matthias van der Hallen, Sergey Paramonov, Gerda Janssens, Marc Denecker" "This paper analyses the graph mining problem, and the frequent pattern mining task associated with it. In general, frequent pattern mining looks for a graph which occurs frequently within a network or, in the transactional setting, within a dataset of graphs. We discuss this task in the transactional setting, which is a problem of interest in many fields such as bioinformatics, chemoinformatics and social networks. We look at the graph mining problem from a Knowledge Representation point of view, hoping to learn something about support for higher-order logics in declarative languages and solvers. Graph mining is studied as a prototypical problem; it is easily expressible mathematically and exists in many variations. As such, it appears to be a prime candidate for a declarative approach; one would expect this allows for a clear, structured, statement of the problem combined with easy adaptation to changing requirements and variations. Current state-of-the-art KR languages such as IDP and ASP aspire to be practical solvers for such problems (Bruynooghe, Theory Practice Logic Program. (TPLP) 15(6), 783–817 2015). Nevertheless, expressing the graph mining problem in these languages requires unexpectedly complicated and unintuitive encoding techniques. These techniques are in contrast to the ease with which one can transform the mathematical definition of graph mining to a higher-order logic specification, and distract from the problem essentials, complicating possible future adaptation. In this paper, we argue that efforts should be made towards supporting higher-order logic specifications in modern specification languages, without unintuitive and complicated encoding techniques. We argue that this not only makes representation clearer and more susceptible to future adaptation, but might also allow for faster, more competitive solver techniques to be implemented."