ABSTRACT. In recent years, there have been a proliferation of extensions to ASP, and it's non-monotonic logical counterpart, Equilibrium Logic, enhancing the logical system with hybrid constraints and temporal, deontic, metric and dynamic modalities, to name a few. So great has this proliferation been, that the corresponding systems somewhat lag behind, due to the intricacies of soundly implementing such sophisticated logical systems. On the other hand, the grounder Gringo facilitates meta-programming by grounding reifying the syntactic constructs ground rules, allowing the re-interpretation of these constructs by succinct meta-encodings that assigning new semantics to ground rules. As part of my research, I study the intersection of meta-programming and the aforementioned logical extensions of ASP. In work awaiting publication, coauthors and I develop the metasp system that enhances and facilitates meta-programming in clingo, and successfully implement Temporal, Dynamic and Metric Equilibrium Logic. I show in previous work as part of my Master's thesis, that these meta-programming techniques can be viewed as succinct way of describing Tseitin-style transformations, and prove their correctness in the Temporal setting. As a different avenue of inquiry, I developed the aspen-tree system, a tool which allows for the reification, analysis and transformation of (non-ground) programs, an alternative approach to the established ground and reify method. In future work, I plan to extend the metasp system's functionality, explore new application domains such as hybrid constraints, and to deploy the aspen-tree system in novel domains for meta-programming in ASP, such as static analysis.

ABSTRACT. Many scientific disciplines generate increasingly large datasets that require complex Data Analysis Workflows (DAWs) for processing. As the number of available tools grow, manually constructing valid workflows becomes challenging. Existing automated synthesis tools, such as the Automated Pipeline Explorer (APE), successfully compose workflow candidates using SAT-based encodings but face significant scalability and extendability limits. This doctoral research frames automated workflow synthesis as a search for workflow candidates, representing them as stable models using Answer Set Programming (ASP) via Clingo. To support this research, a framework was developed utilizing a multi-shot incremental solving architecture that replicates the workflow candidates generated by APE using identical domain model inputs. 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 clasp identifier limits during the grounding phase. 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. While ASP consistently achieves faster total runtimes for large domain models, its performance can vary. Depending on the specific domain model and time horizon, ASP may occasionally consume more memory or experience temporary runtime spikes that exceed APE's, despite maintaining an overall speed advantage. Building upon this foundation, future work will focus on optimization, particularly for longer time horizons. 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. 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. This PhD research aims to develop new deontic logic formalisms grounded in Equilibrium Logic and implemented upon Answer Set Programming (ASP). The work starts from Deontic Equilibrium Logic with Explicit Negation (DELX) and its ASP implementation in Deolingo, and aims at improving the representation and automation of normative reasoning in cases where existing approaches remain limited. The first line of research aims to develop a new deontic modal logic formalism that strictly extends DELX and captures more expressive deontic constructions, including obligations over disjunctions, which DELX cannot represent appropriately. A draft specification of this formalism is already available, and proofs of its main theoretical properties are currently being completed. The second line of research extends Deolingo with temporal deontic reasoning capabilities by implementing the deontic temporal framework DeoTEL (Deontic Temporal Equilibrium Logic), enabling the treatment of norm dynamics over time within an ASP-based workflow. A preliminary implementation of this extension is already available. Overall, the ultimate objective is to provide both solid logical foundations and practical tooling for richer and efficient normative reasoning, by leveraging mature ASP technology for implementation.

ABSTRACT. The formal verification of complex real-world systems, such as maritime vessels operating in dense traffic, is fundamentally limited by the explosion of state space exploration. This challenge is particularly pronounced in settings involving multiple interacting entities, hybrid continuous--discrete dynamics, and uncertainty. It arises with a wide range of domains, including autonomous systems, constraint-based reasoning, and time-critical decision-making. This work proposes a domain-independent three-layer reduction framework for scalable verification, based on the principle of eliminating behaviors that are irrelevant, infeasible, or negligible with respect to a given verification goal. The approach integrates: (i) dependency-driven reduction using graph-based representations of constraint systems and cone-of-influence analysis to extract query-relevant components; (ii) structural or geometric feasibility pruning to eliminate configurations that cannot satisfy system constraints; and (iii) probabilistic relevance filtering to discard low-impact behaviors while providing explicit bounds on approximation error induced by model uncertainty. The proposed framework provides formal guarantees: dependency and feasibility reductions preserve correctness, while probabilistic pruning introduces a bounded and controllable deviation characterized by a confidence parameter. The approach is instantiated in the domain of maritime collision verification as a case study, building on prior work in geometric constraint-based analysis. This research aims to establish a unified reduction principle for scalable constraint-based verification across domains, bridging logical reasoning, constraint propagation, and probabilistic analysis. The ongoing work focuses on integrating constraint-solving techniques and evaluating the reduction in complexity achieved by the proposed framework.

ABSTRACT. Neurosymbolic AI aims to combine the perceptual capabilities of neural networks with the reasoning capabilities of symbolic systems. Prior works have proposed the use of Answer Set Programming (ASP) as a reasoning engine in neurosymbolic pipelines, but these approaches often depend on classical ASP solvers, creating a scalability bottleneck. Our work focuses on developing differentiable ASP solvers that can be integrated seamlessly with neural networks, enabling scalable and end-to-end trainable neurosymbolic systems. We propose NDProp (Neural Decision-Propagation), a differentiable bottom-up ASP computation method that alternates falsity decisions and truth propagations. Through experiments on standard neurosymbolic benchmarks, NDProp demonstrates strong performance in terms of both accuracy and scalability compared to existing ASP-based neurosymbolic approaches. In future work, we plan to investigate the effectiveness of NDProp in applications that require both large-scale neural perception and complex reasoning. Autonomous driving is our primary target, where safe and efficient deployment requires both real-time perception and complex reasoning.

ABSTRACT. This research investigates the integration of logic-based reasoning paradigms for explainable and personalized decision-making in digital health. In particular, it combines Description Logics (DL) and Answer Set Programming (ASP) to bridge structured knowledge representation and constraint based reasoning. The core objective is to study how these two paradigms can be effectively combined within a unified framework. In this context, ontological knowledge is represented using the Web Ontology Language (OWL), with a focus on large-scale clinical ontologies such as SNOMED CT. From an implementation perspective, the approach investigates the use of ASP systems such as Clingo, leveraging theory atoms to enable the integration of ontological reasoning within logic programs. The goal is to develop a unified logic-based framework for building explainable and reliable digital health agents.

ABSTRACT. Dynamic problems, involving movement and change over time, arise in many real-world applications but remain difficult to handle in an integrated manner. This project addresses this challenge using Answer Set Programming (ASP) as a unified language for modeling, reasoning, and interacting with dynamic problems. We present contributions across three pillars: temporal extensions of ASP for representation, meta-programming as an implementation technique for reasoning, and ASP-driven user interfaces for interaction. We also outline future directions, from new dynamic formalisms to temporal interactivity and explanation.

ABSTRACT. Answer Set Programming (ASP) has established itself as a premier rule-based formalism for static optimization problems, yet it often struggles in substantial dynamic domains, such as robotic intra-logistics and job-shop scheduling, where reasoning about actions and effects is paramount. This performance gap exists because current ASP solving machinery is primarily tailored to static knowledge, often reducing dynamic knowledge to the static case. My research addresses this by laying the theoretical groundwork for a Dynamical ASP extension that integrates dynamic representation formalisms into the non-monotonic semantics of Equilibrium Logic (EL). To achieve more refined modeling of these environments, I propose a 2-sorted dynamic logic that utilizes a dedicated alphabet to distinguish between actions and fluents.

ABSTRACT. My research deals with the foundations and applications of hybrid ASP. While standard solvers like clingo have become very performant, challenges remain in regard to problems involving large numeric domains with non-trivial calculations. A wide range of hybrid ASP solvers have been introduced and successfully applied over the last couple of years. However, there are still many open questions regarding their theoretical foundations. This is needed not only to improve future implementations but also to gain a deeper understanding of the essence of the problems they are applied to. This will arguably help to find more natural ASP representations. A central application to my research is the field of (product) configuration where we have already found first results.

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.