ABSTRACT. Business processes underpin many real-world domains, from healthcare and manufacturing to e-commerce, by defining how activities are coordinated to achieve organizational goals. Process Mining (PM) aims at discovering, analyzing and monitoring business processes from event logs. While classical approaches assume complete observations in logs and deterministic process models, real-world applications are inherently affected by uncertainty. Event logs may contain missing or ambiguous events, while process models may need to distinguish between mandatory requirements and soft recommendations rather than strict Boolean constraints.

This talk introduces the foundations of "Declarative" Process Mining based on the DECLARE language and reviews the current state of the art on uncertainty management in this field. It then shows how probabilistic logics, and in particular Probabilistic Logic Programming (PLP), provide a natural semantic framework for modeling uncertainty in both process models and log activities.

By transferring the Distribution Semantics from PLP to Declarative PM, probabilities can be associated with process models' constraints and uncertain events, yielding a unified framework for the main tasks in PM: (probabilistic) conformance checking and (probabilistic) process discovery. Recent developments on efficient conformance checking algorithms and PLP-based discovery are also presented.

The talk concludes by discussing current research directions, including scalable inference, causal process discovery, and richer forms of uncertainty over event data.

ABSTRACT. The well-founded semantics (WFS) yields a unique three-valued model for logic programs that serves as an efficient core for skeptical reasoning, but lacks built-in mechanisms for choice and case-based reasoning, limiting its expressiveness for problems such as decision making and planning. Propositional SAT solvers excel at combinatorial problems but, unlike WFS, do not naturally support reasoning under incomplete information or encoding transitive closure properties. We present an integration of a choice operator into WFS that preserves the suitability of the semantics for scalable, partial-information reasoning, as well as an efficient solving procedure.

ABSTRACT. The notion of uniform equivalence is a powerful tool for determining if two answer set programs behave identically under any set of input facts. However, in practice, developers are often only interested in specific problem instances. While it is possible to use existing equivalence checkers by adding a representation of an instance generator to prune non-admissible inputs, there is a lack of direct model-theoretic characterization for how programs behave under such restricted input sets. In this paper, we generalize uniform equivalence to \chi-equivalence, where \chi represents a specific set of potential input facts. We introduce \chi-models, a novel model-theoretic characterization that tracks SE-interpretations relevant to the restricted input set. We show that deciding \chi-equivalence between two programs amounts to checking whether their \chi-models coincide. This approach provides a beneficial access to the semantics of the programs at hand: the number of \chi-models can be significantly smaller than the total number of answer sets computed across all specific sets of facts, as we shall illustrate on some example scenarios. Finally, we also provide a first complexity analysis for the problem of deciding \chi-equivalence.

ABSTRACT. Studying strong equivalence is useful for the practice of answer set programming because replacing a group of rules within a program with a strongly equivalent group of rules does not change the meaning of the program. But this behavior is not guaranteed when some symbols occurring in the programs are used as placeholders. We show how to remedy this issue by generalizing the definition of strong equivalence. The new definition makes this relation dependent on a user guide--a formal expression describing how programs are expected to be used.

ABSTRACT. Systems for declarative problem-solving often include a ``grounding'' step to remove first-order variables in order to produce a purely propositional representation. Because a naive implementation of this grounding step can be highly inefficient, algorithms were created to derive new information from the problem specification which can be used to reduce the size of the grounding. In this paper, we show how to use this technique with bit vectors, thereby taking advantage of the fact that, on modern computers, logical operations on bit vectors can be executed at extreme speeds, and investigate some places where bit vectors may perform badly. We conduct an experimental analysis, which shows that bit vectors perform well on certain problems, but have limitations.

ABSTRACT. Meta-programming is a powerful technique in Answer Set Programming (ASP) for prototyping language extensions and exploring alternative semantics. While traditional approaches predominantly operate on ground logic programs, many language design tasks require the manipulation of non-ground source code prior to instantiation. We introduce aspen, a novel system for the reification, transformation, and analysis of non-ground ASP programs. Built upon the treesitter parsing library, aspen provides a language-independent and iterative framework for mapping source code to a reified fact base. These facts are then processed by clingo using meta-encodings to generate high-level transformation instructions, which are applied via a templating engine to update the source code. We demonstrate the utility of aspen through two case studies on program analysis and transformation in ASP-Core-2.

ABSTRACT. Linear-algebraic methods for computing stable models of propositional logic programs have recently shown encouraging results. However, existing complete approaches incur prohibitive computation and memory costs, which limit their practical applicability, while other approaches are incomplete and cannot enumerate all stable models or prove the absence of stable models. In this paper, we introduce search into algebraic approaches to logic programming, which to the best of our knowledge has not been studied before. We first represent a normal logic program as a program matrix via a standardization procedure that runs in linear time. We then redefine fixpoint computation and the stable-model condition as a sequence of linear transformations. Based on this reformulation, we propose incremental and decremental backtracking search algorithms that enumerate the stable models of a normal logic program without pre-allocating all possible initial guesses. Experiments on ground programs suggest that the proposed methods offer improvements over previous linear-algebraic approaches and can achieve performance comparable to clingo on certain classes of instances.

ABSTRACT. Abductive reasoning is a central task in artificial intelligence, which has recently been given semantics in the context of Probabilistic Logic Programming with the introduction of the class of probabilistic abductive logic programs (PALPs). In a nutshell, a PALP is a probabilistic logic program extended with a set of abducible facts. The goal is to find the optimal set of sets (possibly only one) of abducibles, called abductive explanation, such that the probability of a query is maximized. In this paper, we investigate the relation with Maximum-a-Posteriori detailing similarities and differences and provide a complexity study. Overall, this work provides a comprehensive characterization of abduction in Probabilistic Logic Programming.