ABSTRACT. Many scientific disciplines generate increasingly large datasets that require complex Data Analysis Workflows (DAWs) for processing. As the number of available tools grows, manually constructing valid workflows becomes challenging. Existing automated synthesis tools, such as the Automated Pipeline Explorer (APE), construct workflow candidates step by step and test their satisfiability with a SAT solver, but face significant scalability and extensibility limits. This doctoral research aims to develop a scalable, preference-aware Answer Set Programming (ASP) framework for automated workflow composition, with scientific data-analysis workflows as the driving case study. It frames workflow synthesis as a search for candidates represented as stable models in ASP. To support this research, a prototype framework was developed using Clingo's multi-shot incremental solving architecture that finds the same workflow candidates as APE using identical domain models and workflow specifications. Preliminary results indicate that ASP provides significant performance and extensibility benefits. A primary challenge in transitioning to ASP was that dense domain models often triggered combinatorial explosions and reached clasp identifier limits during grounding. To mitigate these bottlenecks, an optimized backend featuring a compressed-candidate representation was introduced. This approach shifts computationally heavy compatibility and bindability reasoning from the ASP grounder to a Python-based pre-computation layer. Consequently, for small-to-medium domain models, ASP demonstrates a clear advantage in both runtime and memory usage. Large and dense domain models remain the main open scalability challenge. Depending on the specific domain model and time horizon, ASP may consume more memory or experience runtime spikes exceeding those of APE, even when grounding remains faster. Building upon this foundation, future work will focus on optimization, particularly for longer time horizons, and on developing the prototype into a general, domain-independent solving framework, with scientific workflow synthesis as the motivating case study rather than the only target. My doctoral thesis, specifically, will explore the integration of user preferences through both hard and soft constraints. This approach will allow us to prune the search space and rank workflow candidates based on metrics provided by domain scientists.

ABSTRACT. Datalog is a powerful rule-based language with numerous applications in databases and knowledge representation. Explaining why a fact belongs to the output of a Datalog program over a database is an essential task towards explainable and transparent data-intensive applications. A standard way of explaining a fact is the so-called why-provenance, which provides witnesses in the form of subsets of the input database that as a whole can be used to derive that fact. One successful approach to why-provenance is that of semiring provenance, which unifies different database semantics into one common algebraic framework. Semiring provenance yields a widely applicable notion of provenance and has, over almost two decates now, been applied to a variety of existing logical formalisms. With a recent development of semiring provenance for fixed-point logics, it has progressed into the realm of non-monotonic reasoning formalisms. However, the current approach requires specialized treatment of negation and its interaction with the fixed-point operators, which impairs the application to a wider range of logic programming semantics. There exists a well-developed framework for the uniform treatment of non-monotonic semantics, called justification theory, which has recently been used to extend an existing provenance framework for Datalog to Datalog¬ under both the well-founded and stable semantics. Together these two developments motivate us to investigate how semiring provenance can be extended to general Datalog¬ under arbitrary semantics.

ABSTRACT. Problem modeling in Answer Set Programming (ASP) is not always straightforward as ASP programs producing the same solutions can have great differences in performance during solving. This is exacerbated by the presence of various extensions to the language of ASP, under the name of ASP Modulo Theories (ASPMT). While allowing more performant problem encodings, users still need to learn new syntax and semantics, and understand which problem is suited for which extension. Therefore, in this research, we focus on the transformation of ASP encodings to ASPMT ones, by exploiting syntactic and semantic properties, to ease the experimentation with ASPMT tools. We propose a theoretical characterization of the relevant properties that enable the transformation and the implementation of a tool that performs it.

ABSTRACT. The increased use of Answer Set Programming (ASP) in industrial applications motivates the need for formal verification methods for ASP. This research builds on the anthem system, which verifies correctness and equivalence of logic programs written in a subset of the clingo input language. A first limitation is the restriction on the supported input language of anthem. A second limitation is the non-termination of proof search, which can be due to the complexity of the proof task or due to non-equivalence. This paper discusses ongoing work addressing these limitations as well as outlines possible future research directions.

ABSTRACT. Answer Set Programming (ASP) is a well-known formalism for knowledge representation and declarative problem solving. ASP systems heavily rely on branching heuristics during their solving process. The chosen heuristic significantly affects the overall system performance, and efficient solutions require extensive development effort (e.g., tuning solver parameters, testing alternative encodings, exploiting domain knowledge). Recent advances in Transformer-based large language models (LLMs) have been successful in extracting implicit knowledge about planning domains, which has been exploited to learn custom heuristics. Nonetheless, their application to learning ASP heuristics remains unexplored. This research proposes a general framework for learning domain-specific heuristics by fine-tuning Transformer models on branching sequences produced by a traditional ASP solver, and evaluates it through an initial case study on the planning problem Sokoban.

ABSTRACT. Translating natural language descriptions into formal specifications like Answer Set Programming (ASP) is a significant bottleneck in knowledge representation. While state-of-the-art approaches rely on large, proprietary large language models (LLMs) that require massive computational resources and introduce privacy risks, this research explores the viability of using lightweight, open-weight language models under ten billion parameters. We investigate fine-tuning compact architectures on a diverse, augmented dataset generated via an LLM-driven synthesis pipeline. Additionally, we analyze the necessity of an intermediate Controlled Natural Language (CNL) representation compared to direct translation from natural language to ASP. Our work aims to demonstrate that local execution of specialized small models on commodity hardware offers a cost-effective, private, and accurate alternative for logic programming automation.

ABSTRACT. Previous research has shown that developing train timetables for a single track is intractable. Modern railway systems, however, face growing complexities beyond just timetabling, for example in passenger demand, staffing requirements, rolling stock management, service disruptions, and energy consumption. The need for advanced solutions therefore has become inevitable. Answer set programming has demonstrated success on railway routing problems and has performed well in related problems such as multi-agent pathfinding, scheduling, and urban traffic management. The overall goal of this research is to provide a foundation for modeling large railway systems and their various challenges such that answer set programming can solve them in ways that are advantageous to the state-of-the-art.

ABSTRACT. Answer Set Programming (ASP) owes much of its success as a knowledge representation paradigm to the clear logical foundation for its semantics, which has enabled a wide range of language extensions incorporating temporal, dynamic, metric, deontic, and hybrid modalities. However, ASP solvers are optimized for efficiency rather than extensibility, making the implementation and combination of such extensions a significant undertaking. This DC submission summarizes my doctoral research on closing this implementation and extensibility gap through meta-programming, as well as my inquiry into the theoretical characterization of meta-interpreters in ASP.

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.