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. Integration of Answer Set Programming (ASP) with neural networks has emerged as a promising tool in Neuro-symbolic AI. While existing approaches extend the capabilities of ASP to real world domains, their reasoning pipelines depend on classical solvers, which is a bottleneck for scalability. To tackle this problem, we propose a new method to compute stable models, called decision-propagation (DProp), which alternates falsity decisions and truth propagations. Successful DProp computations are shown to capture the stable model semantics. We then develop Neural DProp (NDProp), a differentiable extension of DProp with neural computation for decisions and fuzzy evaluation for propagations. We evaluate the capabilities of NDProp for learning decision heuristics as well as neuro-symbolic integration, and compare it with existing neuro-symbolic approaches. The results show that NDProp can learn to efficiently compute stable models, and it improves accuracy and scalability on neuro-symbolic benchmarks.

ABSTRACT. Answer Set Programming (ASP) is a well-known declarative paradigms for knowledge representation and automated reasoning, where solutions are represented as stable models of logic programs. The success of ASP is due to a rich set of language extensions that ease the modeling of complex domains, such as SUM aggregates. A common pattern in real-world problems is the co-occurrence of SUM constraints with At-Most-One (AMO) constraints. In particular, sum constraints assert that a weighted sum of literals meets a given threshold, while AMO constraints restrict the simultaneous truth of multiple elements in a set. Recently, the AMOSUM propagator has been introduced to jointly handle SUM and AMO constraints, demonstrating significant performance improvements compared to approaches that treat these constraint types independently. This propagator has been further investigated in ongoing work, proposing several configurations that enhance the original AMOSUM propagator. However, no single configuration has been shown to dominate across all problem instances, motivating the need for a more adaptive strategy. In this work, we propose a Machine Learning (ML) based approach to automatically select the most effective propagator configuration on a per-instance basis. We describe the construction of a diverse training dataset across three combinatorial benchmarks and we extract from it semantically meaningful features capturing the interaction between SUM and AMO constraints. Finally, we develop a series of ML-based selectors to obtain best propagator configurations based on the extracted features. Experimental results show that the ML-based selectors substantially outperform any single static configuration in terms of both solved instances and average runtime.

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. Approximation Fixpoint Theory (AFT) provides a unifying semantic framework for a wide range of non-monotonic log- ics, including many dialects of logic programming. Despite its conceptual elegance, practical implementations of AFT- based semantics remain limited. In this paper, we present an implementation of AFT using meta-programming in Answer Set Programming (ASP). We show how approximators and different kinds of fixpoints can be encoded at the meta-level, allowing existing ASP solvers to compute AFT-based seman- tics for normal logic programs without modifying the solver itself.

ABSTRACT. We introduce a new planning problem with deterministic actions where a plan has to be computed for an instance when initial knowledge is incomplete. The automated planning community has developed a number of domain independent heuristics that facilitate search and help compute long plans. There are several research sub-areas related to planning and scheduling. In classical planning and conformant planning, it is assumed that there are finitely many named objects given in advance, and that only they can participate in actions and in fluents. This is the Domain Closure Assumption (DCA). However, there are realistic open-world deterministic planning problems where the set of initially given objects changes as planning proceeds: new objects are created, and old objects cease to exist. These problems are particularly challenging when knowledge is incomplete. We formulate the novel bounded proper planning (BPP) problem in first-order logic, assume an initial incomplete theory is a finite consistent set of fluent literals, consider a special form of weakly context free action theories, impose an integer upper bound on the length of the plan, and propose to organize search for a plan over sequences of actions that are grounded at planning time. In contrast to numeric planning problems, where each state is a finite set, in the BPP each state is associated with infinitely many infinitely sized first order models. We show how a planner can solve the BPP problem by using a domain-independent heuristic that guides search over sequences of actions. We propose a proof-of-concept implementation. We discuss the differences between our approach and the previously explored formulations of the automated planning problem.

ABSTRACT. We present plank, a practical toolkit for epistemic planning based on Dynamic Epistemic Logic (DEL), a well-known powerful semantics for reasoning about knowledge change. The toolkit has been developed with two audiences in mind: for more expert researchers, plank provides a rich set of features to assist in the development and testing of benchmarks written in EPDDL, a recent language to represent epistemic planning tasks; for less experienced practitioners, the toolkit offers several commands to manipulate, model-check and visualise epistemic states, thus facilitating the early learning process of the main theoretical constituents of DEL. In this paper, we briefly showcase the main features of our open-source software, and highlight the benefits of using plank to assist epistemic planning research.

ABSTRACT. We introduce a typing system that is particularly well suited for typing the linear λ -calculus in de Bruijn notation. This typing discipline, which is reminiscent of Hodas’ and Miller’s model of ressource consumption, guarantees that any well-typed term is linear without the need for an occurrence check. We then establish the subject reduction property.

ABSTRACT. Generalising similar notions from the literature, we introduce the model of recurrent arithmetic circuits, which can be seen as arithmetic analogues of sequential or logical circuits. These circuits utilise so-called \emph{memory gates} which are used to store data between iterations of the recurrent circuit. We introduce a notion of complexity classes for this model and show under which circumstances the newfound hierarchy of theses classes collapses.

ABSTRACT. Answer Set Programming (ASP) is widely recognized as a powerful paradigm for knowledge representation and reasoning, yet broadening its adoption beyond the core community remains a challenge. A contributing factor is the historical lack of tooling that developers take for granted in mainstream languages; such as linters, code completion, and documentation generators. This work addresses the documentation gap with mkdoclingo, an automated tool that analyzes clingo ASP encodings and generates structured, navigable documentation from the source code and lightweight comment annotations. Built as an extension of the popular MkDocs ecosystem, it integrates seamlessly into Markdown-based documentation sites. Its main features include rendered and annotated encoding sections, predicate classification into input and output, dependency graph visualization, and a navigable glossary with per-predicate argument descriptions and file references.

ABSTRACT. Symmetries in Boolean satisfiability (SAT) problems often cause redundant exploration of equivalent regions of the search space, significantly degrading solver performance. Symmetry breaking constraints (SBCs) address this issue by eliminating symmetric solutions while preserving satisfiability. In this work, we study the generation of SBCs from known symmetries for a given SAT formula. We present a tool for constructing SBCs using patterns, a compact representation introduced in previous work. The proposed approach generates clauses using selected sets of permutations while allowing control over the depth of generating constraints, providing a trade-off between the strength of symmetry breaking and the size of the resulting formula. Our main focus is an experimental evaluation of how different sets of permutations influence the effectiveness of symmetry breaking. The experiments are conducted on problems naturally representable as binary matrices, but more complex problems may be considered. We evaluate both solving performance and the reduction in the number of symmetric solutions using state-of-the-art SAT solvers.

ABSTRACT. This paper is a contribution to the analysis of variable ordering heuristics for constraint satisfaction problems. A model of information flow leading to heuristic decisions is presented that includes four distinguishable components: discriminability, feature and message value quality, and decision quality. Experimental results demonstrate that each of the quality components has a definite effect on performance when other components are held constant. These results should improve the analysis of CSP heuristics going forward. They also bear on an earlier analysis of heuristic effects, or heuristic actions, since they clarify one of these actions that had not been adequately characterized prior to this work. As a result, we now have the makings of a complete framework for explaining how variable ordering heuristics actually work.

ABSTRACT. Earlier work has shown that variable ordering heuristics for CSPs improve search by enhancing two fundamentally different actions, labeled simplification and contention. The present work deals with the corresponding problem of why different problems in a supposedly homogeneous set respond differentially to these two heuristic actions. To this end, DNNs were tested to determine whether they could learn to discriminate among problems on this basis given a particular set of feature measurements. Following the success of these tests, XAI (specifically, SHAP) methods were used to gain some insight into the basis for this capacity. The most important features involved the structure of the constraint graph, in particular the degree distribution across variables. However, further tests showed that a number of other features had to be incorporated for highly accurate classification.

ABSTRACT. We introduce an extension of Description Logics (DL), appropriate for modelling and reasoning about deontic notions. DLs represent a family of logical systems, most of them corresponding to a specific fragment of first-order logic, developed to reason about taxonomies and ontologies. Starting from defeasible ALC, an extension of the DL ALC which allows us to model and reason about defeasible information (rules that admit exceptions), we show how to modify the semantics in order to also represent and manage conditional obligations and permissions, and we present the correspondent, and easily implementable, decision procedures. Also, we define a semantics combining reasoning about expectations and reasoning about norms, pairing it with corresponding decision procedures.

ABSTRACT. Reasoning in presence of multiple viewpoints or approximate concepts is a long-standing challenge for knowledge representation formalisms. In this paper, we introduce $\mathcal{ALC}^{\lhd\Box}$, a description logic extending the classical $\mathcal{ALC}$ with two pairs of concept constructors that allow us to talk about objects that ``on some/all accounts, are acknowledged to be $C$'' (with $\lhd C$ and $\Box C$, respectively), as well as ``on some/all accounts, are compatible with being $C$'' (with the duals $\rhd C$ and $\Diamond C$, respectively). Semantically, a function equips each element of the domain with a family of \emph{neighbourhoods}, subsets of the domain that represent multiple, possibly imprecise, or even conflicting, accounts on that element. We show that $\mathcal{ALC}^{\lhd\Box}$ concept satisfiability under a knowledge base is reducible in polynomial-time to the same problem for $\mathcal{ALC}$, hence obtaining an $textsc{ExpTime}$-completeness result. Moreover, we investigate additional conditions on the neighbourhood function, so to capture natural constraints that can be imposed on the accounts of an object: existence, consistency, partial consistency, correctness, and partial correctness. In all these cases, we show that the (tight) $textsc{ExpTime}$ upper bound is preserved, by providing reductions to $\mathcal{ALC}$, $\mathcal{ALCHI}$, or the two-variable guarded fragment $\mathsf{GF}^2$.

ABSTRACT. Standpoint extensions of KR formalisms have been recently introduced to incorporate multi-perspective modelling and reasoning capabilities. In such modal extensions, the integration of conceptual modelling and perspective annotations can be more or less tight, with monodic standpoint extensions striking a good balance as they enable advanced modelling while preserving good reasoning complexities. This extended abstract reports on a paper published in KR'25 where we consider the very expressive description logics SHOIQBs and SROIQBs, which subsume the popular W3C-standardized OWL 1 and OWL 2 ontology languages, and show that they allow for monodic standpoint extensions without any increase of standard reasoning complexity. We do this by first proving the result for the extension of C2 - the counting two-variable fragment of first-order logic - by monodic standpoints and then by showing how to handle role chain axioms. At the core of our treatise is a polytime translation of formulae in said formalism into standpoint-free C2, requiring elaborate model-theoretic arguments. By virtue of this translation, the NExpTime-complete complexity of checking satisfiability in C2 carries over to our formalism. As our formalism subsumes monodic S5 over C2, our result also significantly advances the state of the art in research on first-order modal logics. We prove that NExpTime-hardness already occurs in much less expressive DLs as long as they feature both nominals and monodic standpoints. We also show that, with inverses, functionality, and nominals present, minimally lifting the monodicity restriction leads to undecidability.

ABSTRACT. This extended abstract summarizes our KR’26 paper, where we explore the use of answer set programming (ASP) and its extension with quantifiers, ASP(Q), for inconsistency-tolerant querying of prioritized data. We consider the variants of three well-known semantics (AR, brave and IAR) that use three notions of optimal repairs (Pareto-, globally- and completion-optimal), and for which query answering is in the first or second level of the polynomial hierarchy for a large class of logical theories. Notably, this paper presents the first implementation of globally-optimal repair-based semantics, as well as the first implementation of the grounded semantics, which is a tractable under-approximation of all these optimal repair-based semantics. Our experimental evaluation sheds light on the feasibility of computing answers under globally-optimal repair semantics and the impact of adopting different semantics, approximations, and encodings.

ABSTRACT. Tensor networks and circuits are widely used data structures to represent pseudo-Boolean functions. These two formalisms have been studied primarily in separate communities, and this paper aims to establish equivalences between them. We show that some classes of tensor networks that are appealing in practice correspond to classes of circuits with specific properties that have been studied in knowledge compilation as tractable circuits. In particular, we prove that matrix product states (tensor trains) coincide with nondeterministic edge-valued decision diagrams and that tree tensor networks exactly correspond to structured-decomposable circuits. These correspondences enable direct transfer of structural and algorithmic results; for example, canonicity and tractability guarantees known for circuits yield analogous guarantees for the associated tensor networks, and vice versa.

ABSTRACT. We introduce new parallel algorithms for efficient simulation of stabilizer (Clifford) circuits on GPUs. Our approach reformulates key bottlenecks in stabilizer simulation, such as Gaussian elimination and measurement updates, into GPU-tailored primitives that eliminate sequential dependencies and maximize memory coalescing. We implement these techniques in QuaSARQ, a GPU-accelerated stabilizer simulator designed for large qubit counts and many-shot sampling. Across a broad benchmark suite reaching 180,000 qubits and depth 1,000 (roughly 130M gates), QuaSARQ shows substantial runtime improvements, with up to $105\times$ speedup and over 80% energy reduction on demanding instances. Moreover, QuaSARQ consistently outperforms Stim, a state-of-the-art CPU-optimized stabilizer simulator, as well as Qiskit Aer (CPU/GPU), Qibo, Cirq, and PennyLane. These results demonstrate that our parallel algorithms can significantly advance the scalability of stabilizer-circuit simulation, particularly for measurement-heavy and many-shot workloads, while providing a scalable backend for formal analysis, verification, and benchmarking of Clifford circuits.

ABSTRACT. High-dimensional quantum computation needs a native circuit-level equational theory for qudits. We give the first finite schematic equational theory that is sound and complete for exact unitary qudit circuits in every finite dimension at least two. The result is entirely circuit-level: circuits are built from local gates, sequential and parallel composition, and value-controls, and equality is derivable exactly when two circuits have the same standard unitary semantics. For each dimension, the theory is presented by a finite family of local bounded-arity axiom schemata whose diagrammatic shapes are uniform in the dimension. The key syntactic ingredient is primitive value-control, which builds control on a chosen basis value directly into the language. This gives the language a useful internal algebra of controlled operations from local rules while keeping the presentation native to qudit circuits. The result provides a finite, dimension-uniform foundation for exact equational reasoning about qudit circuits.

ABSTRACT. Organizations rely on structured business processes to coordinate complex tasks. While business process management (BPM) has traditionally assumed full control over participants, also called agents, real processes involve autonomous decision-makers such as human workers and, increasingly, AI-based agents powered by, e.g., large language models. Agents are strategic reasoners that pursue individual goals, subject to a shared process specification constraining the joint execution, a modeling referred to as agentic BPM. We identify and formalize three fundamental settings of agentic BPM, for each of which we study four core problems, namely realizability, synthesis, model-checking, and guardrailing.

ABSTRACT. The video game industry continuously demands highly sophisticated, realistic, and autonomous Non-Player Characters (NPCs). While commercial game engines have historically approached AI from a strictly technical perspective, the core of video game logic remains largely distanced from formal Game Theory. Recently, formal methods have emerged to bridge this gap, recognizing games as Multi-Agent Systems. In our foundational work, we introduced a novel framework utilizing Alternating-time Temporal Logic (ATL) directly within a modern game engine. This paper reports the salient points of that offline-to-runtime architecture, provides a comparative analysis with recent formal developments, such as logics for imperfect information and natural strategic ability, and discusses future extensions, including Probabilistic ATL (PATL) and Neuro-Symbolic integration, to enhance the strategic reasoning of video game AI.

ABSTRACT. We present a formalisation of RTFD*, a multi-agent argumentation protocol, in the Run-Time Event Calculus (RTEC→), a stream reasoning engine with native support for events with delayed effects. Compared to the original specification of RTFD* in the action language C+, our formulation supports time windows for objections and efficient reasoning over high-velocity streams of agent messages, allowing us to handle more realistic argumentation scenarios. We report empirical results demonstrating low-latency monitoring of argumentation procedures at scale.

ABSTRACT. Dung's abstract Argumentation Framework (AF) has been extended in several directions to make knowledge representation and reasoning more intuitive and expressive. In this paper, we discuss the Knowledge-based Argumentation Framework (KAF), an extension of AF with a Knowledge Base (KB) expressed in DL-Lite, which includes concept and role instances describing the topology of an AF, besides additional knowledge on the domain~[1]. The KAF semantics is given by a set of KAF extensions, each consisting of an extension of the underlying AF together with a ``pertinent'' subset of the original KB, which is obtained by discarding assertions referring to arguments that have been ruled out in the AF extension. Then, the framework is further expanded into the Constrained KAF (CKAF), where a set of restricted relational calculus formulae is used for reasoning over `feasible' subframeworks that satisfy the formulae and minimally differ from the original framework.

ABSTRACT. Description Logic (DL) terminologies are collections of rules in which a class is defined in terms of a complex DL concept. Various semantics for terminologies have been proposed over the past decades. However, the tight relation with the recent W3C SHACL standard for expressing constraints over RDF graphs motivated the need to enrich terminologies with forms of commonsense reasoning. In this paper, we explore how reasoning over DL terminologies can be captured in argumentative terms, by establishing a translation into Assumption-Based Argumentation (ABA), a rule-based formalism comprising defeasible assumptions, where argumentation semantics are used to retrieve sets of jointly acceptable assumptions. We focus on the problem of graph completion, where a labeled graph is extended by assigning additional labels only to existing nodes while satisfying a given terminology. Building on the existing correspondence between logic programs and ABA, we show how a DL terminology and a labeled graph can be encoded as an ABA framework such that different completions of the graph arise from different criteria for selecting sets of assumptions. We present results for DL terminologies in ALCI under the classical semantics, the minimal model semantics of Circumscription, and the stable model semantics of Quantified Equilibrium Logic. Furthermore, we provide preliminary results for fragments of the DL-Lite family, where the problem of graph completion is extended to allow the introduction of new domain elements, enabling full model construction.

ABSTRACT. Modifying a knowledge base to remove an unwanted consequence is a difficult task, since it is not obvious how to change it so that the unwanted consequence is no longer implied while avoiding unnecessary loss of information. This problem has been widely researched in belief change under the name of contraction and in ontology engineering under the name of ontology repair. The extension of belief change theory to description logic ontologies represents an important development for both areas, as it allows repair techniques to benefit from advances in belief change and enables contraction operations to preserve more consequences than classical contractions based on subsets of the belief base by utilizing advances in repair techniques. Consequently, to different variations of these postulates have emerged in the literature, seeking to preserve the same intuitions as the original sets in different ways, as is the case with the use of Description Logics. This paper discusses the existing contraction postulates and their adequacy across different scenarios, exploring the intuition behind them and the use of different types of contraction postulates in the literature.

ABSTRACT. Knowledge graphs (KGs) are increasingly used in autonomous driving (AD) to make traffic scene entities and relations explicit for prediction and reasoning. Existing traffic-scene KGs, however, primarily emphasize trajectory forecasting or general scene understanding. This paper presents the nuScenes Intention Knowledge Graph (NIKG), a focused Web Ontology Language (OWL)-based semantic representation and construction pipeline for ego-centric vehicle intention context. NIKG instantiates nuScenes scenes as a self-describing Turtle graph and promotes three intention-relevant relations to first-class properties of each scene participant: ego-relative motion, spatial configuration, and time to collision (TTC) risk. The pipeline uses a small input contract available in many ego-centric driving datasets: ego pose, tracked object annotations, and temporal keyframe order. NIKG is released as an ontology-backed, self-describing graph artifact together with a reproducible construction pipeline and validation protocol for ego-centric intention context. Applying this pipeline to nuScenes mini yields a graph of 211,335 triples across 404 keyframes; under the validation protocol, ego-relative motion labels achieve 92.5% forward consistency. Coverage, logical consistency, and temporal coherence analyses over this artifact are further reported. NIKG occupies the space between scene-oriented traffic KGs and intention-prediction models: a small, explicit semantic layer intended to support downstream work such as knowledge graph embedding (KGE), SPARQL Protocol and RDF Query Language (SPARQL)-based feature extraction, or hybrid neuro-symbolic reasoning.

ABSTRACT. Large Language Models (LLMs) perform well on general NLP tasks but often underperform in domain-specific settings where proprietary knowledge and concept hierarchies are required. Chain of Concepts (CoC) mitigates this by injecting structured conceptual guidance via manually curated graphs, but expert curation is costly and hard to scale or reproduce. We propose Automatic Chain of Concepts (AutoCoC), a fully automated pipeline that (i) induces a rooted concept tree directly from domain documentation, (ii) enriches nodes with representative examples for in-context learning, and (iii) linearizes the tree into a pedagogically ordered prompt sequence via breadth-first traversal. We evaluate AutoCoC on OWL ontology generation (Turtle) across 10 domains, comparing against handcrafted CoC and reverse-engineered baselines. AutoCoC achieves the best mean composite score (0.832) and produces substantially richer ontologies (21.7 classes/file vs. 13.5 and 14.8). Semantic constraint compliance (OntoClean-inspired) is marginally higher (90.6% vs. 89.4%), while confidence is competitive (0.893 vs. 0.864), though per-domain confidence remains higher for the handcrafted baseline in several domains. A self-consistency analysis over 200 runs shows high concept-level stability (0.889) but moderate structural variability (0.625). These results suggest that automated concept-structure induction is a viable way to scale concept-based prompting for structured, domain-specific generation tasks without relying on expert-authored hierarchies. Overall, AutoCoC contributes a reproducible and scalable alternative to expert-authored concept hierarchies by automatically deriving domain-specific prompt structures from documentation, making concept-based prompting more practical for structured knowledge generation.

ABSTRACT. In computational law, formalization of legal rule-based reasoning relies heavily on the subsumption phase, where natural language case descriptions are aligned with formal logical fact formulas. However, several challenges arise due to semantic gaps. This paper investigates the capability of Large Language Models (LLMs) to identify these semantic gaps during legal subsumption. We define a structured methodology categorizing semantic gaps into four distinct types (contradicted, unmentioned, open-textured, and specified) and preliminarily evaluate off-the-shelf LLMs (GPT-4o mini, GPT-4.1, Gemini 3.0 Pro, and Gemini 3.0 Flash Lite). The results show that all models perform well on the task, with greater agreement in identifying contradicted and unmentioned gaps, but less agreement in identifying open-textured and specified gaps.

ABSTRACT. Large language models asked a legal question will always produce an answer. In fragmented treaty regimes, where overlapping international instruments create genuinely contested obligations, this is an ethical problem rather than a technical achievement. This paper argues that the capacity for formal irresolution-the ability of a system to identify and communicate that the applicable law does not yield a determinate answer is an ethical requirement for AI systems operating in high-stakes legal domains. We ground this argument in empirical findings from LLM-based legal information retrieval over a Hohfeld-Structured Normative Knowledge Base of 377 provisions from three marine biodiversity treaties, where LLMs achieve modest precision and middling recall, systematically missing dispersed obligations. We distinguish formal irresolution from technical approaches to epistemic uncertainty in machine learning, arguing that legal indeterminacy is a structural property of fragmented regimes rather than an epistemic gap that better models could close. We illustrate the proposal through a worked scenario demonstrating three distinct output types: determinate answers, structured presentations of competing obligations, and acknowledgements of incompleteness. Formal reasoning frameworks grounded in legal theory can distinguish between settled and contested legal questions, preserving the interpretive authority of human legal actors and preventing what we characterise as a form of hermeneutical injustice through technical architecture.

ABSTRACT. Large Language Models (LLMs) are increasingly used as coordinators in multi-agent systems (MAS), particularly in settings composed entirely of LLM-based agents; however, their ability to coordinate symbolic or hybrid agents under partial observability remains underexplored. In this paper, we investigate whether LLM-based orchestrators can reliably detect and resolve coordination deadlocks in heterogeneous MAS with horizontally partitioned knowledge. We evaluate this problem using a distributed zebra-style constraint satisfaction task involving three specialized agents with restricted reasoning capabilities: equivalence reasoning, relational reasoning, and negation reasoning. We compare fully neural (LLM-only) and neural-symbolic (LLM + Prolog) execution settings under the same orchestration framework, augmented with explicit plan generation, symbolic verification, execution monitoring, and structured planning traces. Our results show that while LLM-based coordination performs effectively in LLM-only settings, it struggles to resolve stagnation and deadlocks when coordinating symbolic agents, despite the symbolic agents maintaining high role-faithfulness and logically valid local reasoning. We further observe that successful LLM-only coordination frequently coincides with violations of role-restricted reasoning boundaries, suggesting that apparent coordination success may partially arise from cross-partition inference leakage rather than robust long-horizon planning. These findings highlight a failure modeinLLMorchestration for heterogeneous MAS and motivate evaluation metrics that consider role compliance and coordination validity in addition to task completion.

ABSTRACT. Multi-hop question generation is the task of generating complex questions that require reasoning over multiple information from multiple contexts. Though the recent works on multi-hop question generation have shown a great impact with excellent outcomes using sequence-to-sequence models and large language models (LLMs), in this paper, we have shown the impact of knowledge graph-based prompting approach on multi-hop question generation. For this purpose, we have proposed a framework, KGP-QG (Knowledge Graph Based Prompting for Question Generation), where, at first, we have generated knowledge graph from the input contexts. The generated knowledge graph is integrated back into the input context to form a knowledge graph-based prompt. Generated knowledge graph enriched prompt is fed to LLMs, where the prompt is used for fine-tuning in two LLMs- BART and T5 models. For this research, the HotpotQA dataset is used for result evaluation and fine-tuning. The result of our proposed framework, KGP-QG, has outperformed the existing methodology

ABSTRACT. MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

ABSTRACT. In the continuation of works that link operational semantics (OGS) with process calculi, we build on top of a type system that enforces visibility in a sequential pi-calculus to also enforce blindness and obtain a full-abstraction result for a sequential pi-calculus with ground references. Blindness is a game semantics notion modeling ground references in languages with exchanges of references; it was introduced by Murawski and Tzevelekos in order to prove full-abstraction for Reduced ML.

ABSTRACT. The presence of shared (or aliased) mutable state has long been recognised as the root cause of many difficulties in programming, particularly complicating understanding and reasoning about the behaviour of programs. Approaches to controlling aliasing are a rich area of study and have become increasingly adopted in mainstream programming languages, for example Rust and Linear Haskell. The policy many of these languages adopt (aliasing XOR mutability and linearity, in the examples, respectively) are incompatible with common, impure, higher-order patterns based on sharing of mutable state. Reachability Types are a recent approach to provide control over sharing in a higher-order functional programming language, by tracking in the type system information about what resources are reachable from a term, which allows separation requirements to be enforced using types. In this talk, I will discuss how to apply operational game semantics (OGS) to investigate the meaning of Reachability Types and the impact these have on the language. This work is detailed in my forthcoming DPhil thesis. An earlier version on this work was presented at GaLoP 2025, based upon the LICS 2025 paper Reachability Types, Traces and Full Abstraction. This talked is intended to be a update on this project, with an improved pedagogical presentation, which I hope will be of interest to the GaLoP audience.

ABSTRACT. Algebraic effects let programmers declare the syntax of operations which can be used to write and compose effectful programs. Such programs can be run by applying effect handlers that give programmers control over when and how many times to call continuations of operations. Embedding algebraic effects and handlers in an existing language provides a lightweight and powerful approach to programming with effects. Such embeddings typically use host language functions to represent continuations of programs. While host language functions offer an ergonomic interface for programming with and handling effects, they also hinder programmers wishing to define custom optimizations for effectful programs. Specifically, optimizations that statically analyze and transform variable bindings cannot be defined, as that would require meta-programming facilities for host language functions. This paper presents a solution to this problem by embedding algebraic effects as intrinsically typed, De Bruijn-indexed syntax. Working in Agda, we demonstrate how this provides a safe-by-construction approach to programming with effects that is almost as ergonomic as the traditional embedding, but which additionally supports optimizations that inspect and transform variable binding.

ABSTRACT. This work studies semiarrows: profunctors that carry both a monoid structure under the Day convolution (parallel composition with unit) and a semigroup structure under profunctor composition (sequential composition without identity), linked by an interchange law and a unit interaction law. The term and definition were introduced in the author's doctoral thesis, generalising monoidal profunctors and arrows. We construct the free semiarrow over an arbitrary base profunctor~$p$, presented as a GADT |FreeSemi p| with five constructors corresponding to the semiarrow operations. We give the interpretation function |interpretSync|, which, given a natural transformation from~$p$ to any target semiarrow~$q$, produces the unique semiarrow homomorphism extending the natural transformation. As a running example we develop an arithmetic-circuit DSL over a prime field. Primitive gates form a GADT; |FreeSemi RelGate| is the resulting circuit term algebra for constraint checking. Because no |arr| combinator is available, every fan-out and structural routing must appear explicitly, making every circuit term inspectable. We present an interpretation of the R1CS cost model via |interpretSync|.

ABSTRACT. Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger, and we recognize this structure in many intensional models of Martin-Löf type theory. This talk is based on a recently published paper and its ongoing continuation.

ABSTRACT. Bipolar disorder is a condition characterised by episodes of extreme mood fluctuation. Effective treatment typically includes psychoeducation, which aims to equip patients with the knowledge needed to make informed decisions that can influence the course of their illness. Key to this process is the ability to monitor the patient's behaviour (both by patients themselves and involved healthcare specialists) in order to recognise early signs of future episodes. To support this monitoring task, we propose a framework grounded in medical ontologies and metric interval temporal logic (MITL). The framework enables real-time monitoring of patient behaviour and the identification of emerging episodes based on behavioral patterns and established clinical guidelines. This paper outlines the formal foundations of the framework and describes future steps towards its adoption in practice.

ABSTRACT. In this work, we consider binary temporal relations, i.e. sets of pairs of time points that capture how events are temporally connected. Such relations arise naturally in applications like as multi-step journey planning, uncertain cause-effect analysis, or disease propagation modelling. Recently, a graph query language called Temporal Regular Path Queries (TRPQs) was introduced in [1] that operates on such relations, by navigating through temporal graphs via regular path expressions extended with a temporal navigation operator. An open question was how to represent TRPQ answers compactly over dense time or time domains of varying granularity, and how compactness can be preserved throughout query evaluation. We addressed these issues in [2], in which we proposed and studied four compact representations of answers to TRPQ. The representations range from two simpler ones that aggregate answers along a single temporal dimension (either departure times or travel distances), to two more complex ones that aggregate results over both dimensions. This line of work opened several questions that remain unaddressed, which we discuss in this paper. Precisely, we discuss: (i) how to abstract TRPQs to graphs annotated with arbitrary Kleene algebras, in order to benefit from results on semiring-based frameworks for relational and path queries; (ii) the relationship between TRPQs and temporal query languages based on Allen’s interval algebra; (iii) alternative representations and visualization strategies for TRPQ answer sets; and (iv) implementation techniques for the two more complex representations, for which coalescing is intractable and cannot be implemented in standard SQL, as identified in our companion implementation work [3].

ABSTRACT. When studying machine learning (ML) models induced from the same training data, one query of interest is predictive equivalence, i.e. to decide whether two models compute the same function. By keeping a single representative of the ML models computing the same function, one removes unwanted redundancy from the Rashomon set associated with the given training data. Furthermore, it is often paramount to answer queries about ML models when not all inputs are known, i.e. when there exists missing data. Examples of relevant queries include prediction sufficiency, but also several other queries related to explainable artificial intelligence (XAI). This paper shows that most of these queries related with reasoning about decision trees can be solved in polynomial time. Furthermore, the paper proves a lower bound on the complexity of enumeration of abductive explanations also in the case of DTs.

ABSTRACT. This project introduces a case study which investigates how pretrained Large Language Models (LLMs), namely OPT, BLOOM, Llama-2, and Llama-3.1, handle five tasks from the bAbI dataset -- a set of common sense and reading comprehension problems stemming from the Facebook research group in 2015. In this investigation, our goal is to provide evaluations of the models themselves rather than their embedding within more complex platforms such as chatbots. By reframing bAbI question answering tasks as language generation problems, we study whether LLMs can function as general-purpose alternatives to specialized information extraction and question answering systems. To this end, we contextualize this investigation with respect to specialized tools designed to solve tasks from the bAbI dataset, including the neural network approach AM+NG+NL MemNN as well as joint statistical NLP and symbolic reasoning approaches s IRLR and TEXT2ALM.

ABSTRACT. The integration of Large Language Models (LLMs) into multi-agent systems promises to enhance agent decision-making with flexible natural-language reasoning, yet raises concerns about controllability, predictability, and safety. We present a principled approach to this problem implemented in DALI2, a logic-based multi-agent framework running on SWI-Prolog. Our key insight is that the tell/told communication filters—originally designed in the DALI language for inter-agent message filtering—can be uniformly extended to govern agent-LLM interactions. Tell rules declaratively constrain what queries an agent may send to an LLM oracle; told rules constrain which responses the agent will accept, with support for pattern matching, state-dependent conditions, and priority-based ordering. The mechanism is fully declarative, bidirectional, and operates within the standard agent reasoning cycle without architectural changes. We formalise the filtering protocol, evaluate it on three test scenarios (smart agriculture, emergency response, and a state-dependent suite), and discuss its properties in comparison with existing LLM guardrail approaches.

ABSTRACT. We exhibit a formula in the language of system F which is provable in classical linear logic (when implication is interpreted as a linear one) but not in system F.

ABSTRACT. Proofs in a logic are usually considered (at least) up to cut-elimination. This is the case in linear logic, that also has another equivalence relation on proofs: rule commutation. We prove that these two notions coincide in second-order linear logic and many of its fragments. Moreover, we show that equality up to rule commutation is undecidable in propositional linear logic—and so is equality up to cut-elimination.

ABSTRACT. We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and is sufficient for sequentialization in the fragment corresponding to the half-polarized typing system for call-by-push-value by Ehrhard.

ABSTRACT. Tensorial logic is a primitive logic of sum, tensor and negation which refines linear logic by relaxing the requirement that linear negation is involutive. The logic is designed in such a way that its formulas [modulo canonical isomorphism] are in a one-to-one correspondence with dialogue games, and that its proofs [modulo cut-elimination] are in a one-to-one correspondence with innocent strategies. In this paper, we explain how to accommodate the exponential modality of linear logic $A\mapsto {!\,A}$ and extend our functorial and proof-theoretic approach to game semantics beyond the multiplicative and additive fragment of tensorial logic. The extension relies on a notion of relative linear-non-linear adjunction on a dialogue category which refines the traditional notion of linear-non-linear adjunction on a $\ast$-autonomous category. In this description of full propositional tensorial logic, every exponential modality of linear logic $A\mapsto {!\,A}$ is attached to a negation of tensorial logic $A\mapsto \tensorialnegation{A}$. Two forms of negations thus coexist in the logic: the original non-involutive tensorial negation $A\mapsto \tensorialnegation{A}$ and a new backtracking exponential negation $A\mapsto\, \pointednegation{A}$ which stands for the ``modality + negation'' combinator~$A\mapsto \, !\, \lnot\, A$ and defines a relative comonad on the linear non-involutive negation.

ABSTRACT. Interactive Theorem Provers are crucial for certifying system correctness, but they impose a steep learning curve and require a high level of user expertise. While Machine Learning techniques have been employed to suggest proof commands, current approaches often rely on resource-intensive pipelines to process the proof data used as input to the model. This work addresses this inefficiency by proposing a methodology that trains autoregressive language models directly on raw proof states, along with LLM-PVS, a prototype implementation integrated into the VSCode IDE. This approach allows PVS users to receive proof-command recommendations and lemma suggestions from local models without depending on extensive preprocessing of the proof data. While initial empirical evaluation indicates that this direct approach achieves competitive performance in restricted contexts, challenges regarding model hallucinations, lack of explainability, and scalability in premise selection remain to be addressed.

ABSTRACT. Constraint satisfaction, the task of finding an assignment of variables that respects a set of constraints, is a key area in artificial intelligence, with many industrial applications. In general, many constraint satisfaction problems are NP-hard; hence, exhaustive searches are intractable. Local search is a popular paradigm for solving such problems: instead of exploring the entire search space, local search solvers transition, for a limited number of steps, from one assignment to another, guided by hand-crafted, problem-dependent heuristics. Recently, neural networks have been studied as a means of automatically learning heuristics for transitioning between assignments. A particular class of neural local search solvers uses neural networks as generative models to produce joint probability distributions over the problem's variables, conditioned on the current assignment. Then, transitioning to the next assignment is done by sampling from the generated probability distribution. However, these solvers do not integrate constraint reasoning; hence, any assignment can be generated during the local search. In this work, we propose to integrate knowledge compilation into neural local search solvers. By first compiling constraint satisfaction problems into multi-valued decision diagrams (MDDs) and sampling assignments in them, constraints can be applied to reduce the number of unsatisfying assignments in the sampling space. Our experiments show that using MDDs yields a sampling space that can be orders of magnitude smaller while incurring negligible overhead. Moreover, our MDD-based sampling procedure significantly improves the number of instances solved on Sudoku and graph colouring problems.

ABSTRACT. We propose a feature-free approach to algorithm selection that replaces hand-crafted instance features with pretrained text embeddings. Our method, ZeroFolio, proceeds in three steps: it reads the raw instance file as plain text, embeds it with a pretrained embedding model, and selects an algorithm via weighted $k$-nearest neighbors. The key to our approach is the observation that pretrained embeddings produce representations that distinguish problem instances without any domain knowledge or task-specific training. This allows us to apply the same three-step pipeline (serialize, embed, select) across diverse problem domains with text-based instance formats. We evaluate our approach on 11 ASlib scenarios spanning 7 domains (SAT, MaxSAT, QBF, ASP, CSP, MIP, and graph problems). Our experiments show that this approach outperforms a random forest trained on hand-crafted features in 10 of 11 scenarios with a single fixed configuration, and in all 11 with two-seed voting; the margin is often substantial. On the three scenarios with published AutoFolio results from the 2015 ASlib competition, ZeroFolio with two-seed voting matches or outperforms AutoFolio without per-scenario configuration tuning. Our ablation study shows that inverse-distance weighting, line shuffling, and Manhattan distance are the key design choices.

ABSTRACT. We investigate theorem proving by large language models (LLMs) in a controlled proof-from-scratch setting, where models must construct induction proofs using only recursive definitions and mathematical induction. Building on our previous Direct Induction Proof Challenge, we introduce variable-generalization settings that systematically increase formula and proof complexity. We compare a reasoning-oriented model (GPT-5.2) with a non-reasoning baseline (GPT-4o) on Lean 4 proof generation tasks. While GPT-5.2 nearly saturates the original 20-problem benchmark, performance degrades rapidly as the number of variables and required commutativity applications increase. These results suggest that controlled induction benchmarks provide a useful diagnostic framework for evaluating the limits of current LLM theorem proving systems.

ABSTRACT. Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifiers to ensure output correctness. In this paper, we present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability, being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, our model learns better representations than models trained for classification only, with a much higher data efficiency -- requiring orders of magnitude less training data. NeuRes employs propositional resolution as a proof system to generate proofs of unsatisfiability and to accelerate the process of finding satisfying truth assignments, exploring both possibilities in parallel. To realize this, we propose an attention-based architecture that autoregressively selects pairs of clauses from a dynamic formula embedding to derive new clauses. Furthermore, we employ expert iteration whereby model-generated proofs progressively replace longer teacher proofs as the new ground truth. This enables our model to reduce a dataset of proofs generated by an advanced solver by $\sim$$32\%$ after training on it with no extra guidance. This shows that NeuRes is not limited by the optimality of the teacher algorithm owing to its self-improving workflow. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.

ABSTRACT. Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion include the relation of lambda-terms with terms typed in other substructural type systems, such as the relevant and the ordered type systems, and the use of quantitative types to relate the strongly normalising lambda-terms with weak linear terms that share the same normal form. Here we define a new term expansion for a calculus with explicit substitutions, using it to relate a lambda-calculus with explicit substitutions to Boudol's resource aware lambda-calculus with multiplicities, where function arguments have a possibly limited availability.

ABSTRACT. This paper establishes the cut-elimination theorem for intuitionistic propositional multiplicative-additive linear logic with the least and greatest fixpoints (μIMALL) in terms of its phase semantics. A classical first-order multiplicative-additive linear logic system with the least and greatest fixpoints was introduced in Baelde-Miller (2007). Its intuitionistic fragment was discussed in Baelde (2012), but the cut-elimination theorem for this fragment has not yet been proved. We introduce a propositional fragment of this system, μIMALL, and establish the cut-elimination theorem. To prove the theorem, we define phase semantics for μIMALL and show the following two statements: (1) Soundness: if a formula is provable in μIMALL, then it is true in all phase semantics, and (2) Cut-free Completeness: if a formula is true in all phase semantics, then it is provable in μIMALL without Cut. Okada (1999, 2002) employed a phase semantic method to prove the cut-elimination theorems for classical and intuitionistic linear logic systems. De et al. (2022) applied this method to a propositional fragment of classical propositional multiplicative-additive linear logic with the least and greatest fixpoints. We refine and apply their arguments to prove the cut-elimination theorem for μIMALL.

ABSTRACT. We propose a logical formalisation of computational errors in reactive, non-deterministic systems. To this aim, we introduce a new three-valued symmetric non-deterministic disjunction, designed to provide a faithful logical representation of the non-deterministic choice arising in concurrent computations. The connective is defined within the framework of non-deterministic matrices (Nmatrices) and derives from a minimal combination of Kleene’s tolerant semantics and Bochvar’s symmetric error persistence, thereby eliminating the residual asymmetry induced by sequential evaluation strategies such as McCarthy’s logic. The resulting semantics admits genuinely non-deterministic outcomes in mixed cases involving errors, while preserving commutativity and operational symmetry.

ABSTRACT. The relational semantics of linear logic is a powerful framework for defining resource-aware models of the λ-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on λ-terms, and demonstrate that it coincides with the preorder associated to the relational semantics, studied through non-idempotent intersection types.

ABSTRACT. Decidability of higher-order matching was established by Stirling via a sophisticated game-semantic argument. We propose an alternative specification of higher-order matching as an intersection type inhabitation problem. Concretely, we use the recently proposed system R, a syntax-directed intersection type system in which judgements derive vectors of types and binary relations control information flow between coordinates. Bounding the dimension of type vectors in system R derivations makes inhabitation in system R decidable. We outline how a solution to a higher-order matching instance corresponds to an inhabitant in system R of bounded dimension. The work is in progress; the central challenge is establishing a dimensional bound that depends only on the matching instance.

ABSTRACT. We propose a solver-in-the-loop self-improvement framework for training neural policies to guide domain-independent dynamic programming (DIDP) in solving combinatorial optimization problems. For each instance, DIDP-based beam search is run within a DIDP model, leveraging its pruning mechanisms such as dual bounds and state constraints, and the best solution found is extracted as an expert trajectory. The policy is then trained by minimizing a cross-entropy imitation loss. Experiments on the four combinatorial optimization problems show that the proposed method consistently reduces node expansions and achieves competitive solve time, while significantly outperforming the same DIDP models and solvers guided by Proximal Policy Optimization (PPO) and by the default dual bound guidance.

ABSTRACT. Dynamic programming solvers in existence today combine a modeling language with fixed search algorithms. While they allow model-specific heuristics, their ability to experiment with different search strategies remains limited. This paper introduces an extension to CODD that implements novel and classic search strategies, using the common modeling language of CODD. It also investigates an implicit diagram representation that reduces memory usage and improves performance. Experimental results on several classic combinatorial optimization problems demonstrate the importance of easily switching search strategies.

ABSTRACT. Research across all disciplines generates increasingly large and complex data that require sophisticated data analysis workflows (DAWs) for processing and interpretation. Constructing these workflows manually can be very challenging, especially given the growing numbers of computational tools and libraries that are available to implement the different steps in the workflows. The Automated Pipeline Explorer (APE) addresses this workflow composition challenge by synthesizing workflow candidates for a given specification, based on a semantic domain model that provides an ontology of terms and functional characterizations of the available workflow components. APE has successfully been used for workflow composition in different domains, including bioinformatics, geosciences and computational materials science. However, the current implementation of APE, which is based on creating a temporal finite automaton, faces extensibility and scalability issues that hinder its application to large scale domains. In this paper, we present an ASP-based architecture for automated workflow composition, framing the synthesis problem as a search for stable models that represent valid workflow candidates. Our approach uses multi-shot incremental solving to support future extendability and interactive configuration, combined with different optimizations motivated by domain-specific features. Our evaluation with diverse benchmarks shows that the ASP-based approach reaches semantic parity with the current implementation of APE, while providing a more scalable and more extensible foundation for further development and application.

ABSTRACT. We present a framework that specialises Temporal Here-and-There with Constraints (THTc) for declarative spatial reasoning (DSR). THTc provides the underlying nonmonotonic temporal semantics with constraints, while spatial objects and relations are represented following the DSR approach: geometric objects of different sorts are described analytically by parameters for their shape and position, and spatial relations are interpreted by constraints over these parameters. The resulting framework supports default assignments, declarative inertia via a uniform axiom schema, spatial ramification, and inductive definitions of spatial predicates under stable model semantics. Stable models determine qualitative spatio-temporal scenarios together with numerical witnesses, from which concrete diagrammatic representations can be constructed.

ABSTRACT. We present flaspland, an Answer Set Programming (ASP) testbed for tackling complex routing and scheduling problems within the Flatland railway simulation environment. To establish a solid theoretical foundation, we provide a rigorous formalization of the Flatland environment, detailing its grid-based topology and navigational dynamics. Building upon this, we propose and analyze three distinct graph-based representations to effectively encode the underlying constraints. Crucially, we introduce a twofold, path-driven ASP encoding scheme that decouples spatial routing from temporal scheduling. Our empirical results demonstrate that these specialized representations outperform off-the-shelf multi-agent pathfinding approaches. By providing a testbed for real-world railway scheduling, flaspland facilitates the evaluation of declarative approaches to qualitative and quantitative temporal constraints.

ABSTRACT. Reasoning about action and change is a fundamental challenge in Artificial Intelligence, yet dedicated action languages within Answer Set Programming (ASP) see significantly less adoption than plain ASP. In practice, the lack of a unified approach inhibits the creation of an expressive, sustainable framework that leverages ASP's rich modeling capabilities and efficient solvers. To bridge this gap, we introduce a non-monotonic modeling framework based on Dynamic Logic (DL) that is designed for direct implementation through modern ASP systems. By synthesizing and adapting variants of established methodologies, our approach, the Dynamic Equilibrium Logic with Actions and Fluents, unifies a rich two-sorted language with non-monotonic semantic foundations. As common in DL, it explicitly distinguishes between state variables (fluents) and action variables to facilitate intuitive knowledge representation, combining propositional logic for concurrent state transitions with DL-based path expressions for global constraints over complex trajectories. Furthermore, we demonstrate that despite its expressive two-sorted nature, our formalism can be entirely reduced to the simpler, one-sorted Dynamic Equilibrium Logic. This strict reduction paves the way for practical implementation, ultimately allowing these expressive dynamic problems to be seamlessly solved using the temporal ASP solver telingo.

ABSTRACT. Many important computational problems can be defined as modification problems. These problems provide an elegant framework for problem definitions and several Algorithmic Meta Theorems are known for them, providing a rich algorithmic toolbox. We study the expressive power of graph modification problems by providing non-expressibility proofs for particular problems and presenting foundational results that can be used as a basis for a more systematic study of the computational aspects of graph modification problems.

ABSTRACT. Polylogarithmic time delineates a relevant notion of feasibility on several classical computational models such as Boolean circuits or parallel random access machines. As far as the quantum paradigm is concerned, this notion yields the complexity class FBQPOLYLOG of functions approximable in polylogarithmic time with a quantum random access Turing machine. We introduce a quantum programming language with first-order recursive procedures, which provides the first programming language-based characterization of FBQPOLYLOG. Each program computes a function in FBQPOLYLOG (soundness) and, conversely, each function of this complexity class is computed by a program (completeness). We also provide a compilation strategy from programs to uniform families of quantum circuits of polylogarithmic depth and polynomial size, whose set of computed functions is known as QNC, and recover the well-known separation result FBQPOLYLOG ⊊ QNC.

ABSTRACT. Given a family of CNF formulas F, the size-width inequality in Resolution reduces the hard problem of proving strong (say exponential) lower bounds on the number of clauses needed to refute F in resolution to the easier problem of proving strong enough (say linear) lower bounds on the width of the clauses needed to refute F in resolution. Similar results connect the degree and size in the proof systems Polynomial Calculus, Sherali-Adams, Sum-of-Squares and Positivstellensatz. In this talk we present a simplified argument for the result on Sherali-Adams, Sum-of-Squares, in the special case when all input polynomials are monomials (or Boolean axioms).

ABSTRACT. We study Two-Variable Fragment of First-Order Logic, FO2, with certain semantic constraints that model hierarchical data. Our first logic extends FO2 with a linear order < and a chain of increasingly coarser equivalence relations E_1 ⊆ E_2 ⊆ ... . We show that its finite satisfiability problem is NExpTime-complete. We also demonstrate that the weaker variant of this logic without linear ordering posesses the exponential model property. Our second main contribution concerns FO2 extended with a chain of total preorders ⪯ 1 ⊆⪯ 2 ⊆ ... . We prove that it likewise admits an NExpTime-complete finite satisfiability problem. However, we show that the complexity increases to EXPSPACE-complete once access to the successor relations of the preorders is allowed.

ABSTRACT. This extended abstract summarizes our recent contribution, currently under double-blind review at IJCAI'26, in which we ask: Within a class of existential rules that supports decidable query entailment, do the usual abstract classes become concrete? We answer in the negative for classes based upon the termination of all classical chase variants and for the bts class. This explains the necessity of diverse, class-specific techniques for proving chase termination, as query entailment offers no systematic tool for this purpose.

ABSTRACT. Weighted model counting (WMC) has proven effective across computer science and physics, yet existing applications to quantum physics target only specific problem instances, lacking a general framework with formal guarantees. We present a framework that converts Dirac notation to WMC instances via a type system and denotational semantics, supporting general $q^n \times q^m$ matrix operations including multiplication, addition, and trace. We prove correctness of the encoding and provide a Python implementation. As applications, we compute partition functions of the transverse-field Ising model and the Potts model, demonstrating that heuristics from automated reasoning can be systematically brought to bear on quantum physics.

ABSTRACT. In this work, we introduce a framework for exact classical simulation in noisy quantum circuits based on weighted model counting (WMC), leveraging techniques from automated reasoning to enable efficient classical analysis of quantum computations by exploiting structure within the quantum circuit. Rather than reconstructing the full quantum state, this approach enables the direct computation of targeted quantities of interest, including exact output probabilities and selected density matrix elements even in the presence of general noise processes. To achieve this, we introduce a novel encoding of mixed quantum states within the WMC framework that explicitly represents the density matrix in the computational basis. This representation complements existing Pauli-basis encodings and is shown to be advantageous in specific regimes. Furthermore, we introduce a framework which allows for the translation of arbitrary linear super operators to the weighted model counting framework in both of these encodings. Among other maps, this allows for the formulation of any completely positive trace preserving map in terms of a logical formula. As a result, any physical map, be it unitary (e.g. quantum gates) or non-unitary (e.g. noise channels) can be translated to a weighted model counting problem. This provides a unified approach for simulating quantum dynamics under general discrete operations. We demonstrate the framework on several physically relevant noise channels commonly encountered in quantum hardware, including depolarizing, phase damping, and amplitude damping noise. We evaluate our approach by performing experiments on a benchmark set of randomly generated quantum circuits based on two universal gate sets: the Clifford+T set and the rotational gate set. The performance of the encodings for the universal gate sets and various noise channels are investigated, as well as compared to existing tensor network and decision diagram based simulators. Our results show that our tool generally outperforms these methods and we identify regimes where either encoding outperforms the other, providing guidance on how to select the most effective representation for a given circuit and noise model. Furthermore, the approach also outperforms with respect to weak simulation, i.e. sampling-based methods. This work demonstrates that automated reasoning techniques can serve as a powerful tool for noisy quantum verification, quantum error correction studies, …, providing exact analysis tools for noisy intermediate scale quantum hardware and fault-tolerant quantum computing.

ABSTRACT. In this talk I will report on my efforts of using LLMs to (auto)formalize intersection type systems. Starting from a solid Agda codebase, I have been able to formalize soundness and completeness of several variants of non-idempotent intersection types, including the characterization of space consumption of a sophisticated abstract machine. I did this with almost no previous experience with proof assistants.

ABSTRACT. Relational semantics is a simple and well-studied denotational model for the untyped lambda-calculus. It can be presented syntactically as a non-idempotent intersection type system and provides qualitative and quantitative information, such as the characterization of normalizing terms and their execution time (i.e., the number of steps to reach the normal form). We study the relational semantics for the simply typed lambda-calculus extended with the fixpoint combinator; we show that the interpretation of a simply typed term is nothing but the interpretation of the untyped term restricted to the non-idempotent intersection types refining the simple type. Our approach is based on merging a simply typed derivation with a non-idempotent intersection one, which is not trivial since simply typed terms do not enjoy subject expansion and may not be normalizing (because of the fixpoint combinator). We also show that some well-known qualitative and quantitative completeness results provided by relational semantics and non-idempotent intersection type derivations for the untyped lambda-calculus lifts to the simply typed lambda-calculus with fixpoint combinator nearly for free, thanks to our results.

ABSTRACT. Recent work in defeasible reasoning has seen notions of preferential semantics in the style of Kraus et al. applied in various modal logics. However, work in this field has focussed primarily on satisfiability checking, and monotonic notions of entailment which may be inferentially weak. One particular modal logic where this has been introduced, is propositional standpoint logics, where modalities can express the views of different viewpoints. This has resulted in the formalisation of propositional defeasible standpoint logic (PDSL). In this paper, we propose a means of lifting the class of (non-monotonic) rational entailment relations from traditional KLM-style reasoning to a fragment of PDSL. In order to do so, we extend the expressivity of PDSL via situated standpoint conditionals, allowing us to talk about a defeasible conditional holding in the context of a given standpoint. This allows us to the syntax of PDSL in terms of situated conditionals, and showing that a large fragment of PDSL is expressible as a set of situated conditionals. We then focus on characterizing non-monotonic entailment in this fragment, defining a method to transport any ranking-based entailment relation from the propositional case into the PDSL case. This is first described in the general case and then considered in the specific cases of rational and lexicographic closure, which provides a faithful translation of each inference to PDSL. We also show that entailment-checking in this fragment of PDSL can be done largely using algorithms from the propositional case, while preserving complexity bounds.

ABSTRACT. In this paper, we integrate the defeasible logic of Kraus, Lehmann and Magidor (KLM) with the standpoint logic framework of Gómez Álvarez and Rudolph. This is done with the goal of formally expressing knowledge taking into account multiple (possibly contradicting) viewpoints, which in turn may hold defeasible beliefs. In doing so, we utilize Defeasible Restricted Standpoint Logics (DRSL), introduced by Leisegang et al. Our work expands on previous work by providing a foundational representation result for DRSL semantics and systematically lifting several well-known entailment relations from the propositional case to the standpoint-enhanced setting. In particular, we characterize the semantics for DRSL through a set of KLM-style postulates adapted for the standpoints case. We furthermore provide a means to lift preferential entailment, and the class of entailment relations based on single ranking functions from the purely propositional to the standpoint-enhanced context, including rational and lexicographic closure. We show this can be done equivalently through semantic and algorithmic means. Furthermore, we show that, for each considered form of entailment, the complexity class of entailment checking does not change when moving from propositional KLM to DRSL.

ABSTRACT. The present contribution is framed in the context of probabilistic belief by analyzing two main approaches to the subject: the Lockean thesis, and Leitgeb’s notion of P-stable sets. More precisely, the present contribution puts forward an investigation that aims at establishing contact points between the deductive closure of Lockean belief sets, conformity to a characterization we obtained in terms of step probabilities, and the revision of belief sets that are defined in terms of P-stability. For the latter approach, in addition to the original ideas and results of Leitgeb from 2013, we will also follow a path recently studied by Delgrande, Lakemeyer, Pagnucco, and Sack. We find tight links between these two approaches in the setting of probabilistic epistemic change.

ABSTRACT. Dynamic Programming (DP) and Constraint Programming (CP) are well-established paradigms for solving combinatorial optimization problems. Usually, these two approaches are used separately. This paper aims to show that the two can be combined effectively and elegantly, providing an alternative way to address the problem, with DP serving as the primary search framework and CP used as a subroutine to leverage global constraint propagation. This paper presents such an approach for the Partial Shop Scheduling Problem (PSSP), for which a pure DP method has previously been proposed, and efficient CP filtering algorithms are available. The PSSP is a general scheduling problem where each job consists of a set of operations with arbitrary precedence constraints. The approach is flexible enough to accommodate anytime DP strategies, such as anytime column search, whereas the original DP algorithm operated in a strictly layer-wise manner. While not competitive with state-of-the-art pure CP solvers for this specific problem, our primary contribution is demonstrating the viability of this hybrid integration.

ABSTRACT. We study the Type-I assembly line balancing problem with human-robot collaboration (Type-I ALBP-HRC), which jointly requires task-to-station assignment, robot allocation, execution-mode selection (human, robot, or collaborative), and intra-station scheduling under precedence constraints. We develop and compare two independent exact approaches for this problem: a constraint programming (CP) model exploiting interval-based scheduling constraints and a dynamic programming (DP) approach built on a three-level nested dynamic program. Both approaches are benchmarked against a MIP reference model on standard instances. Results show that DP-based engines are strongly competitive for proof-oriented exact search, while CP methods provide tight optimality gaps on hard, large instances within time limits.

ABSTRACT. This paper establishes and proves complexity results for entailment for cumulative propositional dependence logic and for cumulative propositional logic with team semantics. As recently shown, cumulative logics are famously characterised by System C and exactly captured by the cumulative models of Kraus, Lehmann and Magidor. This gives rise to the entailment problem via relational models, which is specifically considered here.

ABSTRACT. There are a lot of varying results on the expressivity of transformers. Many of them even seem contradicting. This work aims to organize this body of results in a systematic way and consider a notion of uniformity in transformer models, as many expressivity results rely on the existence of a transformer for input length $n$ even though in practice, transformers are viewed as a model that works for variable input lengths up to a maximum input length $N$.

ABSTRACT. Answer Set Programming (ASP) is a mature formalism for non-monotonic reasoning, constraint satisfaction, and combinatorial problem solving, but its adoption beyond specialist circles is held back by the cost of writing and maintaining complete logic programs. Large Language Models (LLMs) are complementary in a specific operational sense: they are fluent at turning natural-language descriptions into candidate relational facts, but unreliable as exact symbolic reasoners. Hybrid systems such as LLMASP combine the two, yet in their standard form they keep extraction and reasoning strictly sequential—the oracle is queried for every target predicate, and ASP is consulted only afterwards, filtering a database in which hallucinated facts already mix with well-supported ones. LLMASP-LGX closes this loop through a lightweight YAML-based configuration: the user declares predicates, natural-language extraction prompts, admissibility guards with monotonicity flags, and small ASP knowledge-base fragments, and the LLMASP-LGX engine reads these declarations as an interaction policy between the LLM oracle and the ASP solver. The central claim of this extended abstract is that, despite its lightweight syntax, an LLMASP-LGX configuration specifies a constructive interaction between LLM and ASP: facts extracted so far, together with facts derived by ASP, decide which LLM queries are admissible at each step, and LLM responses update the logical state that drives subsequent reasoning. Reported experiments show that these lightweight annotations reduce oracle calls by more than 70% on a mixed-domain benchmark, while matching the quality of an a posteriori ASP filter and improving substantially over unguided extraction.

ABSTRACT. Constructing composite activity definitions for recognising activities over streams of low-level, symbolic events is a highly involved task: definitions often involve numerous spatio-temporal constraints, while labels for learning them automatically are hard to obtain. We propose a method that generates such definitions from natural-language descriptions using pre-trained Large Language Models (LLMs), together with a novel similarity metric that quantifies the human effort required to correct LLM-generated definitions. An experimental evaluation in the maritime domain demonstrates the effectiveness of our approach.

ABSTRACT. While Answer Set Programming (ASP) is a powerful tool for symbolic reasoning, its outputs (i.e., sets of ground atoms) are often impenetrable to non-experts. We propose a formal map–summarize framework that decouples the translation of symbolic facts into text from the linguistic refinement of the final explanation. By evaluating five distinct strategies, ranging from raw LLM prompting to deterministic template-based mapping, we highlight the trade-offs between faithfulness, readability, and computational cost.

ABSTRACT. Multi-Agent Systems (MAS) require formalisms capable of handling partial and evolving information. While imperfect-information extensions of Alternating-time Temporal Logic (ATL) are highly expressive, they typically make model checking undecidable. This paper summarises \emph{Intuitionistic ATL} (IATL), an extension of ATL that replaces classical propositional truth with intuitionistic truth, capturing a novel, computationally tractable notion of imperfect information based on \emph{information refinement}. We review IATL's syntax and semantics over \emph{birelational concurrent game structures} (BCGS), the truth-monotonicity characterisation, and the PTIME-completeness of model checking, matching the complexity of classical ATL.

ABSTRACT. Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs. CTLF adopts a counting worlds semantics where each world represents a possible output at a given step in the generation process and introduces modal operators that allow us to verify whether the current output series respects an intended probability distribution over a protected attribute, to predict the likelihood of remaining within acceptable bounds as new outputs are generated, and to determine how many outputs are needed to remove in order to restore fairness. We illustrate the framework on a toy example of biased image generation, showing how CTLF formulas can express concrete fairness properties at different points in the output series.

ABSTRACT. The expressive power of First-Order Logic (\FO) over infinite trees remains poorly understood. In particular, it is still an open problem whether one can decide if a given regular language of infinite (or finite) trees is definable in \FO. A common approach to better understand such formalisms is to provide alternative characterizations using, for example, automata or regular expressions; indeed, two automaton-based characterizations of \FO have recently been introduced. In this note, we return to a purely logical perspective to investigate the syntactic constraints required for the well-known modal $\mu$-calculus to precisely capture the expressiveness of \FO. We demonstrate that by employing the two-way modal $\mu$-calculus, we can identify the exact fragment corresponding to \FO. As a by-product, we obtain tight complexity results for the extension of the well-known logic \CTL with past operators. Conversely, eliminating past operators yields a significantly more intricate landscape. We present a specific fragment of the standard $\mu$-calculus that we conjecture to be expressively equivalent to \FO, and discuss the main challenges in establishing a formal proof for this claim. This underscores the complex nature of \FO over infinite trees and highlights how—unlike in word logics—past operators are crucial for expressiveness in tree logics.

ABSTRACT. Clinical reasoning requires weighing the quality of evidence, assessing its relevance to a particular patient, and reaching a judgement that accounts for both. Doctors perform this reasoning implicitly; it is difficult to articulate and impossible to audit. Large language models can extract structured information from the biomedical literature, but their outputs lack the transparency and traceability that clinical decision-making demands. This article proposes a neurosymbolic framework in which an LLM performs the extraction and a symbolic layer performs the reasoning. The symbolic layer combines three components: Toulmin's model for organising the evidence, epistemic commitments for identifying the beliefs that bear on the decision, and a reason-based reasoning architecture for weighing those beliefs through the hierarchy of evidence and the characteristics of the patient. The framework is non-monotonic (the same evidence yields different recommendations for different patients) and auditable (every recommendation traces back through explicit reasons to source evidence). A case study on semaglutide prescription illustrates how three patient profiles produce three outcomes (prescribe, undecided, withhold) from the same evidence base, with full provenance at every stage.

ABSTRACT. Agentic AI systems that use large language models (LLMs) to implement advanced applications are becoming more and more popular. However, such systems are known to be prone to hallucinations, opaque in the way they make decisions, and not offering any safety guaranties. This introduces the need for principled ways to analyze and design such systems, such that their behavior is verifiable against requirements specifications, and compliant and explainable according to predefined behavioral and decision making rules and strategies. We propose a requirements-driven neuro-symbolic approach to systematically developing such systems. Our approach uses agent-based goal models to represent the system requirements and allowable strategies for achieving them. Goal models are then translated into programs in the IndiGolog logic-based agent programming language to orchestrate agent behavior in compliance with the requirements. LLMs are integrated as components for pursuing specified tasks and rendering formalizable results, amenable to symbolic verification and explanation generation. In this paper, we introduce our approach and examine how it can be applied to the design of a meeting scheduling application.

ABSTRACT. Aggregating inconsistent judgments from multiple reasoners is a long-standing problem in artificial intelligence, with mature foundations in consensus theory, belief pooling, and epistemic logic. The topic has gained renewed significance with the rise of LLM ensembles, where the judgments of specialist LLMs, retrieval-augmented agents, and judge models often diverge even on factual matters. The core problem is that such divergent judgments usually reflect differences in the information sources accessed, not random noise. How can an aggregation rule recognize this distinction and reconcile beliefs without forcing agents that cannot represent the same fine-grained truth to converge? In this paper, we propose a symbolic-probabilistic framework that unites symbolic epistemic structure with probabilistic belief dynamics. Agents maintain probability distributions constrained by their epistemic partitions, while a critic agent computes a dynamic target belief and specialists shift only toward epistemic projections of that target. The framework supports a convergence guarantee and provides a diagnostic interpretation of the remaining disagreement. The contribution is a concise symbolic-statistical approach to feasible consensus in settings where agents cannot necessarily represent the same knowledge.

ABSTRACT. The growing adoption of symbolic knowledge-based decision systems highlights the need of principled methods to quantify their interpretability. While symbolic models are often considered inherently understandable, the cognitive effort required to interpret them varies significantly depending on both their structural properties and on user-specific factors. Existing approaches typically rely on coarse structural proxies, neglect the user perceptions and are often limited to specific representation formats. This work introduces a representation-agnostic and parametric framework for modelling the cognitive complexity of symbolic knowledge bases. First, a taxonomy is proposed to characterise structural and procedural elements of knowledge representations contributing to cognitive complexity, including size, depth, logical composition, and evaluation dynamics. Building on this taxonomy, a unified formal model is defined. The model decomposes cognitive complexity into micro-level components, capturing the internal structure of knowledge units, and macro-level components, accounting for their global organisation and evaluation process. The model also incorporates user-defined tolerance parameters, enabling a profiled assessment of perceived complexity. The proposed framework is validated through an experimental analysis on a set of knowledge bases with different structural properties. Results show that the model captures meaningful differences in cognitive effort across representations and user profiles, providing a flexible tool for designing, evaluating, and comparing interpretable symbolic models.

ABSTRACT. Frontier reasoning-tuned language models still fail on deductive tasks at depth, and the cost of improved performance through extended internal reasoning scales poorly. Symbolic delegation offers a complementary route: a language model translates the problem, while a solver performs the inference. However, current autoformalization pipelines for logic programming are typically bespoke integrations tied to particular tasks or agents. We introduce \textsc{PrologMCP}, a task-agnostic, open-source server that exposes Prolog as a stateful tool through the Model Context Protocol (MCP). Its compact tool interface, structured error reporting, and per-session isolation make the \emph{translate--run--inspect--repair} loop a reusable primitive for MCP-capable agents. We evaluate a formalizer agent enhanced with \textsc{PrologMCP} against standard and reasoning LLMs (Claude Sonnet 4.6, GPT-4.1, and o4-mini) on two subsets of \texttt{PARARULE-Plus}: a general-purpose sample and a more challenging one targeting a specific failure mode of natural-language reasoning. On the general sample, the formalizer matches or exceeds reasoning LLMs (accuracy 1.00 vs.\ 1.00 / 0.998), with the largest gains over standard models (0.762 for GPT-4.1). On the challenging subset, the formalizer remains near-perfect (1.00 / 0.99) while reasoning LLMs drop to 0.95 / 0.94. These results suggest that delegating inference to Prolog via MCP is a robust and inspectable alternative to extended natural-language reasoning.

ABSTRACT. Automatic translation of Natural Language (NL) sentences into logic representation – such as First-Order Logic (FOL) formulae – is a task of great interest for many communities, including Knowledge Representation (KR), Natural Language Processing (NLP), normative Artificial Intelligence (AI), and AI in general. Recently, an increasing number of works have explored the use of Large Language Models (LLMs) to translate NL into FOL, with promising results. However, existing works mostly focus on the translation of a single NL sentence at a time, resulting in independent formulae that do not share a common predicate and constant name space. This work presents a new framework – namely Natural Language to Uniform First Order Logic (NL2UNIFOL) – that leverages LLMs to translate NL sentences into a uniform FOL theory, where formulae share the same vocabulary. NL2UNIFOL is an end-to-end pipeline that: (i) translates NL sentences into preliminary FOL formulae; (ii) identifies and safely merges predicate and constant names to obtain a uniform vocabulary; (iii) finally generates the final FOL theory. We use NL-FOL pairs from the MALLS dataset to validate our framework. Results show that in the majority of cases NL2UNIFOL is able to correctly create clusters of predicate and constant names to be merged together, which allows to obtain a uniform FOL theory. We also recognise that there are still a numerous amount of cases in which the represented name and the representative name semantically diverge, which motivates future work to further improve the noun clustering process.

ABSTRACT. The analysis of gender stereotypes in Brazilian sexual violence judicial proceedings represents a critical yet computationally underexplored challenge given strict digital sovereignty requirements and the heterogeneous nature of Brazilian judicial documents. Existing neuro-symbolic frameworks for Knowledge Graph (KG) and Large Language Model (LLM) integration, while effective in controlled settings, have not yet been designed to address the constraints inherent to this domain. This work introduces FORGE (Framework for Ontology-grounded Retrieval and Graph Extraction), an on-premise framework applied to structured information extraction from sexual violence proceedings. FORGE combines (i) locally-hosted Vision-Language Models and Large Language Models for OCR and structured information extraction over heterogeneous scanned documents, (ii) ontology-grounded retrieval and extraction anchored in an established gender-bias ontology derived from Brazilian sociological research, and (iii) a Virtual Knowledge Graph layer, which exposes a relational backend through the ontology. Preliminary execution over 10 manually validated proceedings yielded a VKG of 926 triples, preserving the fine-grained taxonomy of the ontology, demonstrating the viability of an end-to-end neuro-symbolic framework that operates without dependence on proprietary generative models.

ABSTRACT. We investigate the combination of Knowledge Graphs (KGs) and Large Language Models (LLMs) as a means of grounding model responses in verified organizational data and reducing hallucinations. A domain ontology covering people, skills, positions, and projects was defined and instantiated in a Neo4j graph database. A GraphRAG pipeline was built on top of this graph: natural language questions are translated into Cypher queries, executed against the KG, and the retrieved structured data is supplied as context for LLM response generation. Three architectures were evaluated on a manually validated gold-standard corpus of 95 question–query–response triples: GPT-4 standalone, a locally-run quantized model fine-tuned for Cypher generation (text-to-cypherGemma-3-27B, referred to as HF 27B), and a hybrid combining both. HF 27B achieved a perfect 100% Cypher execution rate against 97.9% for GPT-4, but only 43.2% factual consistency in the generated answers. GPT-4 reached 68.4% consistency and the hybrid 52.6%. The gap between the hybrid and GPT-4 standalone reveals that a semantically incorrect Cypher query cannot be rescued by a better text generator, making query correctness the binding constraint of the whole pipeline. Results support GraphRAG as a viable and practical strategy for domains requiring factual traceability, such as strategic personnel planning and legal research.

ABSTRACT. Virtual Knowledge Graphs (VKGs) expose relational data through domain ontologies and declarative R2RML mappings, but constructing such mappings remains labor-intensive and requires expertise in databases, ontology engineering, and mapping languages. Existing LLM-based approaches often rely on context-overloaded prompts and provide limited support for grounding decisions across iterations. This paper proposes AgenticVKG, a vision for a memory-driven agentic framework for VKG mapping construction. The architecture combines an embedding-based Retriever, an LLM-based Matcher, and a persistent Memory organizing database context, mapping patterns, past decisions, and agent reports. Through iterative mapping rounds, AgenticVKG aims to ground each decision in a shared, cumulative context, providing a basis for more consistent and traceable R2RML mapping construction.

ABSTRACT. In this article, we take the operators that make up variable elimination in probabilistic graphical models and reinterpret them as forgetting operators in the vein of marginalisation for forgetting in logic. As such, we define the inference task of forgetting in probabilistic graphical models and provide operators to solve the task, discussing effects on complexity versus variable elimination for probabilistic inference. In addition, we consider different properties for forgetting in probabilistic graphical models, arguing whether variable elimination as forgetting fulfils them.

ABSTRACT. The conditions of trivial independence, symmetry, decomposition, and mixing are a well-established axiomatisation of independence. These are known to be sound and complete for the usual independence relation among random variables on probability distributions. We lift the semantic definitions needed to establish this result to the level of arbitrary structures of preference. As an example of this, we confirm that the same holds for ordinal conditional functions (OCFs): not only are independence statements over OCFs sound with respect to these axioms, but they are also complete. We also show that a faithful operator exists for OCFs, allowing us to deduce that, as for probability spaces, OCFs characterise these axioms.

ABSTRACT. Ranking functions, also known as ordinal conditional functions (OCFs), and total preorders on worlds (TPOs) are standard representations in belief change and nonmonotonic reasoning. In bounded unstructured spaces, we study how often these representations admit non-trivial syntax splittings, i.e., decompositions induced by partitions of the underlying propositional signature, and how the resulting splitting families are structured. For rank-bounded OCFs, coarsening closure makes the unique finest syntax splitting an exact counting handle. We derive exact counts, prevalence ratios, and finest-shape distributions. The resulting class is small relative to the ambient space and is strongly concentrated on coarse finest shapes. For depth-bounded TPOs, we report exact prevalence counts and analyze the subcorpus admitting non-trivial syntax splittings using Bell baselines, closure deficits, and relative splitting profiles. In the exhaustive |Σ| = 3 series, all such TPOs are Bell-complete up to depth 3, while closure-irregular families first occur at depth 4. A supplementary inspection interface connects these aggregate findings to concrete TPO instances by displaying splitting families, missing coarsenings, and bridge OCFs obtained from absolute marginal sums.

ABSTRACT. Models of High-level Computation (MHCs) provide effective means to describe complex real-world computing systems because they offer formal foundations for the specification of interacting computing devices, as opposed to describing individual ones, which has been the focus of classical models such as Turing machines or the lambda calculus itself. Despite numerous proposals over the past half century, there is still no canonical MHC akin to Turing machines for (compositionally) reasoning about computation in the large. One of the major drawbacks of state- and data-oriented MHCs is that they extensively neglect control flow, a well-know semantic property that defines computation order. Only control-oriented MHCs treat control explicitly at the expense of ignoring data flow or assuming that data follows control. Mixing data and control within the same framework leads to inefficient methods for formal analysis and verification. To address this, the computon model has recently emerged as a category-theoretic MHC that separates data and control and makes control explicit by supporting composition operators characterised as finite colimit constructions. Such constructions allow the formation of sequential, parallel, branching and iterative computing devices. Unfortunately, the computon model is still a generic reference rather than a concrete realisation. In this paper, we provide a variation of it to enable functional computing devices, introduce a new branching operator, discuss how to define synchronous parallelising out of sequencing and asynchronous parallelising, describe concrete operational semantics for computon execution and provide the first implementation of the model. The implementation yields an open-source programming environment that realises the underlying categorical semantics. This tool is publicly available and ready to build complex computing devices that are structurally correct by construction.

ABSTRACT. Prolog is traditionally thought of as an untyped logic programming language, although there are queries that result in a type error. Several attempts of statically introducing a type discipline in Prolog have been made but they have not been widely adopted. We use Maude to implement a typed unification algorithm and use it as the basis for an interpreter for Prolog called MaudeTypedLog. This interpreter follows the Typed SLD-resolution operational semantics for logic programming, that makes it is possible to detect type errors in both programs and queries dynamically.

ABSTRACT. We propose abstractions for exploiting symmetries in programming and reasoning based on the mathematical proof principle "without-loss-of-generality" (wlog). We decompose such arguments into three components. The first component makes the symmetry explicit by defining appropriate groups and their action on the input/assumptions and output/conclusions. The second component explicates how to canonise the input, by choosing appropriate symmetries for each input. The third component is a core function/proof that transforms canonical inputs into outputs. The proposed wlog construct combines these components: given an input, calculate its canonising symmetry, use the symmetry to canonise the input, apply the core function to the canonical input, and apply the inverse symmetry to the output. Here we develop the mathematical foundations for these abstractions. We illustrate the approach on running examples: sliding-tile merges in 2048, binary-tree insertion, and Schur's inequality as a mathematical instance of WLOG. We extend the framework to algebraic datatypes using initial algebra semantics, showing how a G-symmetry strength on a functor lifts group actions to inductive types and that the unique fold into an equivariant algebra is itself equivariant, allowing us to avoid using general recursion to define a symmetric version of tree insertion. Finally, we develop the theory of equivariant canonisers and explore the cases when the WLOG construction is guaranteed to produce an equivariant function.

ABSTRACT. I will present a recent result giving a very simple characterization of the Giry monad on (standard Borel) measurable spaces in terms of a (initial) universal property. In addition, I'll present some ongoing work on adapting this result to categories more suited for functional programming, such as elementary toposes.

ABSTRACT. Equality saturation is a powerful technique for program optimisation and reasoning, driven by the use of equivalence classes of terms under rewrite rules. These equivalence classes lie at the root of data structures called equality graphs (e-graphs). Despite their numerous advantages, until recently e-graphs lacked native support for variable binding, limiting their applicability to programming languages. We propose to address this problem from a categorical perspective by extending the interpretation of e-graphs as string diagrams, namely morphisms in symmetric monoidal semilattice-enriched categories which we additionally equip with a monoidal closed structure. We further define a concrete representation using hierarchical hypergraphs, and introduce a corresponding double-pushout (DPO) rewriting system. Finally, we establish the equivalence between term rewriting and DPO rewriting, with the combinatorial model inherently absorbing the equations of the symmetric monoidal structure. Our approach, specifically designed for lambda calculi, is compared and contrasted with slotted e-graphs --- an alternative method for incorporating variable binding within e-graphs.

ABSTRACT. The field of video anomaly detection has evolved towards more flexible approaches that increasingly leverage the semantic understanding capabilities of Vision-Language Models (VLMs). These models are particularly appealing as they enable reasoning about the high-level semantics of anomalous events, going beyond simple pattern deviations. However, despite their strong semantic capabilities, VLMs are often computationally expensive and may be unsuitable for deployment in high-risk domains. In this paper, we propose a neuro-symbolic agent that combines a YOLO-based perception model for object detection with a symbolic reasoning component capable of identifying anomalies formalized through explicit rules. The reasoning module also serves as a filtering mechanism, selecting ambiguous situations that require deeper semantic analysis according to user-defined criteria. Such cases are then delegated to VLMs, reducing unnecessary reliance on these costly models. Finally, we discuss the limitations of the proposed approach and illustrate its applicability through a representative real-world scenario.

ABSTRACT. Robotic assembly tasks require systems to interpret unstructured visual instructions, derive action sequences, and ensure physical feasibility. While Vision-Language Models (VLMs) excel at extracting semantic information from visual manuals, they cannot reliably solve complex combinatorial reasoning tasks, enforce action preconditions, or guarantee global consistency. To bridge this gap, we present ASPembly, a neuro-symbolic pipeline that instantiates a visual variant of the Logic-Guided Extraction (LGX) framework for image-based assembly manuals. Unlike baseline pipelines that query a model independently and validate the output post-hoc, ASPembly interleaves VLM-based extraction with non-monotonic Answer Set Programming (ASP) reasoning. In this architecture, the VLM reads visual instruction pages to propose candidate robot commands, while ASP acts as an active control mechanism rather than a passive checker. Guard conditions over the evolving symbolic state dynamically determine which predicates can be extracted, rejected, delayed, or logically inferred without additional model calls. By shifting logic from post-processing to active process control, ASPembly significantly improves the coherence of the generated assembly trace, mitigating spurious outputs and reducing unsupported commands during extraction.

ABSTRACT. We present a case study of declarative multi-robot coordination using DALI2, a SWI-Prolog reimplementation of the DALI agent-oriented logic programming language, integrated with the CoppeliaSim robot simulator as a digital twin. Three mobile rescuers must locate victims scattered among obstacles in an arena and bring them to a safe zone; victims marked as heavy can only be moved by two robots cooperating via a coordinator-mediated synchronisation protocol. Each robot carries a vision sensor whose images are periodically analysed by a two-phase pipeline: a fast green-pixel pre-filter that skips the LLM when no victim-coloured pixels are present, and a vision-capable LLM (local Qwen3 via JAN or OpenRouter gpt-4o) that returns structured JSON objects which the bridge parses into Prolog events driving the agent’s decision-making, including autonomous exploration and obstacle avoidance. We show how DALI2’s reactive rules, internal events, FIPA-style proposals, told/tell priority queues, multi-event synchronisation, and a built-in LLM oracle map naturally onto a layered cognitive architecture in which symbolic deliberation drives an embodied simulation through a thin Python bridge. Robots autonomously explore the arena via patrol waypoints, stop to photograph their surroundings, wait for the vision model’s analysis, and then decide whether to report a victim, avoid an obstacle, or continue exploring. The bridge translates DALI2’s Redis-based LINDA channel into CoppeliaSim’s ZeroMQ Remote API, preserving the framework’s distributed star topology and making the twin a first-class testbed: agents do not know whether their bodies are simulated or physical. The full source code, scene generator, agent specification, and reproducibility instructions are publicly available.

ABSTRACT. The Resource-Constrained Project Scheduling Problem (RCPSP) is a long-standing challenge problem in the area of constraint optimization. Its goal is to schedule partially ordered activities, each requiring specific resources, as effectively as possible while respecting the resources’ capacity limits. Previous approaches have utilized Constraint Programming or local search techniques for solving the RCPSP to exact or approximate optimality, respectively. While Answer Set Programming (ASP) along with its extensions by difference logic or finite domain constraints has been successfully applied to closely related scheduling problems, these declarative problem solving approaches have so far not been explored for the RCPSP. In this work, we elaborate on modeling approaches for encoding the RCPSP in plain ASP as well as its extensions by difference logic and finite domain constraints. Interestingly, formulating resource capacity limits is simpler in plain ASP due to the explicit representation of time points, while the use of difference logic or finite domain constraints incurs a certain modeling effort. Our empirical comparison on small- to medium-scale RCPSP instances shows that the simplicity of modeling promotes plain ASP and more than outweighs its larger problem representation size, which counteracts the performance trends typically observed on related scheduling problems.

ABSTRACT. Industrial product configuration often involves complex partonomic structures where the required number of components is unknown in advance since it depends on intricate, interdependent constraints. This paper addresses the challenge of determining minimal bounds for unbounded cardinalities within the CoomSuite workbench. While previous methods relied on a “naive” single-shot approach, requiring grounding and solving from scratch for every iteration, we introduce an extended workflow that leverages clingo’s multi-shot capabilities. We evaluate our approach across three benchmark domains demonstrating the efficiency of our incremental method compared to traditional single-shot strategies in scenarios with unbounded cardinalities.

ABSTRACT. Lower bounds against strong algebraic proof systems and specifically fragments of the Ideal Proof System (IPS), have been obtained in an ongoing line of work. All of these bounds, however, are proved only over large (or characteristic 0) fields,1 whereas finite fields form the more natural setting for propositional proof complexity. This work establishes lower bounds against fragments of IPS over constant-sized finite fields, resolving an open problem left by a series of prior works beginning with Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.’21), persisting with Behera, Limaye, Ramanathan, and Srinivasan (ICALP’25), and most recently posed by Forbes (CCC’24). We further highlight the importance of the constant-sized finite field regime in IPS by showing that any hard instance in this regime for a sufficiently strong proof system translates into a hard instance against AC0[p]-Frege, whose lower bounds remain a longstanding open problem. In particular, we show the following. Constant-depth multilinear IPS: We prove that a variant of the knapsack instance studied by Govindasamy, Hakoniemi, and Tzameret (FOCS’22) has no polynomial-size IPS refutation over finite fields when the refutation is multilinear and written as a constant-depth circuit. Our argument has two key ingredients: (i) the recent set-multilinearization result of Forbes, which extends the earlier result of Limaye, Srinivasan, and Tavenas (J. ACM’25) to all fields; and (ii) an extension of the techniques of Govindasamy et al. to finite fields, obtained by constructing a new knapsack variant and generalizing the degree lower bound used in their work. This improves on Behera et al. who obtained related results for fragments of IPS over fields of positive characteristic. Their result requires the field size to grow with the instance, whereas ours does not. Hence, in the constant positive characteristic setting, our IPS lower bound subsumes theirs as it also holds over constant-sized finite fields. Moreover, we separate our proof system from that of Govindasamy et al. by constructing a further knapsack variant and proving a new degree lower bound. Read-once ABP IPS: We present new lower bounds for read-once algebraic branching pro- gram refutations, roABP-IPS, in finite fields, extending results of Forbes et al. and Hakoniemi, Limaye, and Tzameret (STOC’24). Algebraic-to-CNF translation: We show that any lower bound against any proof system at least as strong as (non-multilinear) constant-depth IPS over finite fields for any instance, even a purely algebraic instance (i.e., not a translation of a Boolean formula or CNF), implies a hard CNF formula for the respective IPS fragment, and hence an AC0[p]-Frege lower bound by known simulations over finite fields (Grochow and Pitassi (J. ACM’18)).

ABSTRACT. We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and choiceless polynomial time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and depth. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.

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. The partial weighted MaxSAT problem is an important generalization of SAT, useful for expressing and solving a variety of constrained optimization problems. Efficient solving methods have been developed based on SAT and MIP, including core-guided search, the implicit hitting set approach, and branch-and-bound. The problem is naturally expressed as a graph, with vertices representing literals and clauses, while a set of edges connect literals to the clauses that contain them. In this paper we propose a graph neural network architecture that is trained to predict the truth value of each MaxSAT variable in an optimal solution (with a confidence score). The machine learning model is initially trained on small random MaxSAT instances, then fine-tuned for a particular class of MaxSAT instances. A model such as this could be used to warm-start a solver or to guide search in some way. We chose to apply the model as part of a learning-to-prune method, where some literals (the most confident predictions) are chosen to assign before applying a conventional solver. Using learning-to-prune, we demonstrate significant improvements in performance compared to a current branch-and-bound MaxSAT solver.

ABSTRACT. A neural clause selector sits in the hot path of a saturation-based theorem prover: the model is invoked on every generated clause and the prover blocks on each result. Whether the ML guidance pays off under a fixed wall budget depends on two axes, the model's selection quality and the per-call cost the integration imposes. This paper holds the first axis fixed -- a GCN encoder paired with a transformer scorer -- and isolates two engineering decisions on the second: whether clause embeddings are cached across iterations, and whether embed requests are fired one at a time (eager) or buffered to the selection boundary (batched). On 16 TPTP problems run to a 256-iteration cap, caching changes per-problem wall time by at least a factor of about 28x, and without it the prover routinely exhausts the 60-second wall budget; the batching decision is smaller and workload-dependent (eager wins by 1-40% on this set, where |Delta| <= 20 new clauses are generated per iteration; on heavier workloads the ordering reverses). The two decisions are independent and orthogonal to the model, so the same trade-off recurs in any encoder/scorer-shaped clause selector.

ABSTRACT. Differential privacy is considered to be the golden standard in private data analysis. However, verifying that programs satisfy this standard is notoriously hard. The purpose of this submission is to report on an ongoing work of translating the Fuzz type system into a higher order logic RHOL. Fuzz is a type system used to prove sensitivity of programs, which is a very important property in differential privacy. Type systems, like Fuzz, are very convenient, because they allow for automation of proofs. Their downside is that they are less expressive than logics. With our work, we would like to combine the advantage of automated reasoning using Fuzz with the expressivity of RHOL. We provide the translation of the deterministic part of Fuzz, while our future goal is to extend it to the probabilistic part.

ABSTRACT. Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID for mathematical induction, and LKID𝜔 and CLKID𝜔 for infinite descent. LKID𝜔 is an infinitary system, in which proofs are infinite trees, and CLKID𝜔 a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone definitions, while inductive definitions are generally non-monotone. The logic FO(ID) extends classical first-order logic with non-monotone inductive definitions. In previous work, we provided a formalization of the principle of mathematical induction for non-monotone definitions by extending LKID to a sequent calculus SCFO(ID) for FO(ID). In this work, we provide a formalization of the principle of infinite descent for non-monotone definitions by extending LKID𝜔 and CLKID𝜔 to sequent calculi SCFO(ID)∞ resp. SCFO(ID)⟲ for FO(ID). We extend several proof-theoretic results for LKID𝜔 and CLKID𝜔 to SCFO(ID)∞ and SCFO(ID)⟲ regarding soundness, completeness, cut-elimination and the relation with SCFO(ID).

ABSTRACT. Independence in nonmonotonic and probabilistic reasoning, in various forms, has long been an active area of study. At the same time, significant progress has been made in consolidating the study of independence in category theory. In particular, the notion of an independent product characterises independence or separability in a remarkable variety of contexts. This paper takes some first steps toward applying this theory to nonmonotonic and probabilistic reasoning. We detail several categories C of preference structures and introduce the notion of a preference functor 𝑃 : Sig → C, which assigns signatures to preference structures on possible worlds. We define a notion of semantic independence with respect to a preference functor 𝑃 in terms of independent products. For ordinal conditional functions, this corresponds to known notions of independence in nonmonotonic reasoning and belief revision. On the other hand, we show that the category of total preorders does not possess an independent product that corresponds to such established notions of independence. In doing so, we demonstrate how established definitions of independence for OCFs are in fact the same phenomenon as usual independence of random variables in probability theory, while also offering a reason why TPOs are not as well-behaved as OCFs in terms of independence. Our proposed framework allows for reasoning about independence in nonmonotonic and probabilistic reasoning at a new level of generality. Furthermore, this opens the door to apply theories of independence from diverse contexts to our setting.

ABSTRACT. Input/Output (I/O) logic provides a flexible framework for representing conditional norms without reducing them to truth-functional implications. Among its variants, constrained Input/Output logic refines the applicability of norms by introducing constraints that limit when obligations may be detached, enabling a fine-grained account of defeasible normative reasoning. In this paper, we present a formal embedding of I/O logic in Higher-Order Logic (HOL), building on the algebraic approach based on subordination structures and slanted algebras. The embedding is based on the algebraic characterization of input/output operations with intermediate translations into slanted modal algebras. We formalize constrained input/output operations within the algebraic framework and embed them in HOL. We then implement the translation in the Isabelle/HOL proof assistant, enabling automated reasoning within the system. Our approach generalizes previous embeddings of standard I/O logic and provides a foundation for the analysis and verification of defeasible normative systems.

ABSTRACT. Quantum circuit synthesis is an essential part of developing efficient programs for quantum computers. Designing efficient quantum algorithms is a highly complex and non-intuitive process. At the same time, many classes of quantum circuits do not yet have optimal solutions and can potentially be further optimized. The development of quantum computers is an ongoing and important area of research, with various architectures emerging. Each of these architectures, however, supports only a specific set of gates. All of the aforementioned points demonstrate the importance of and demand for efficient, automatic quantum circuit synthesis that enables the creation of circuits with a parametric set of supported gates. Specifically, we consider the creation of new circuits from a specification, as opposed to classical optimization approaches that rewrite an existing circuit. This is a problem with an enormous state space, and many synthesis approaches fail to achieve the required scalability. In this talk, we will present an approach to quantum circuit synthesis that describes the given problem using first-order logic formulae, which are then discharged using SMT or MILP solvers. An important aspect of this work is the use of various representations of complex numbers. Beyond the classical representation using two real numbers, we also support a subset of complex numbers that allow precise algebraic representation using quintuples of integers. This representation allows for more efficient encoding of quantum gates and a formulation using only linear expressions. Among other things, the implemented tool supports various methods of circuit search based on a defined optimization function. Using incremental encoding, we are able to find depth-optimal circuits. We focus on the class of repeat-until-success (RUS) quantum circuits, which can compute unitaries more efficiently than standard techniques using ancillas and measurements. Using the implemented tool, we demonstrate that some RUS circuits from the literature can be further optimized and reduced. The implemented tool is further compared with the state-of-the-art quantum circuit synthesis tool Quokka#. The comparison results show comparable performance between the two approaches.

ABSTRACT. While quantum hardware remains limited, hybrid quantum-classical algorithms with complex control structures, including unbounded loops, are emerging, posing new challenges for program analysis: the accurate estimation of resource consumption of a given program is needed. In this work, we answer this challenge with the first static analysis solution for reasoning about the resources — termination or cost — of hybrid quantum programs with unbounded loops. Towards that end, we introduce integer hybrid path-sums, a symbolic representation of possible executions of a quantum program. A generic strategy for determining termination and expected resource consumption via loop invariants is also proposed. Finally, a prototype of this solution is implemented in Haskell. This work is the first step toward the design of a complete static resource analysis tool for hybrid quantum programs with unbounded loops, essential for the development of real-world quantum computing. This extended abstract illustrates fully developed results without expanding on the technicalities.

ABSTRACT. We study the minimum number of clauses required to encode a boolean function $f$ into a CNF formula with auxiliary variables. This problem is practically relevant to SAT solving and also of theoretical interest due to its connections with other complexity measures such as nondeterministic circuit size. We first show that any function $f \colon \{0,1\}^n \to \{0, 1\}$ can be encoded with $O(\sqrt{2^n})$ clauses, which is information-theoretically tight. Next, we show a connection between space- and time-efficient data structures and compact CNF encodings. Namely, modeling preprocessed data structures as computation with advice, we obtain the following result: if a boolean function $f$ can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice, then it admits a CNF encoding with $\widetilde{O}(\sqrt{mt} + t)$ clauses. This constitutes a non-uniform generalization of Robson's variant of the Cook--Levin theorem, which encodes RAM computations with runtime $t$ (without advice) using $\widetilde{O}(t)$ clauses. By derandomizing a data structure devised by Larsen and Williams for evaluating $k$-CNF functions, we use our non-uniform Cook--Levin result to show that every $k$-CNF function on $n$ inputs can be encoded with $\frac{n^k}{2^{\Omega_k(\sqrt{\lg n})}}$ clauses. This is notable because if we restrict our attention to encodings that are themselves $k$-CNF, it is known that the minimum number of clauses required to encode $k$-CNF functions is $\Theta_k(n^{k}/\lg n)$ in the worst case. Thus, perhaps surprisingly, clauses of unbounded width are helpful for encoding $k$-CNF functions.

ABSTRACT. At the lower end of the hierarchy of complexity classes we find, represented by the word problem of the Dyck language D1 and the boolean formula value problem, respectively, the complexity classes TC0 and NC1, which are still not known to coincide or to be different. Aim of this note is to “approximate” the boolean formula value problem by TC0-computable predicates. This is done by using the string representation of trees instead of using pointers. This allows for the quantification along the nodes of a path which usually requires logspace-complete techniques. Now it could be tempting to believe the boolean formula value problem to be TC0, Which would have surprising consequences like the collapse of the counting hierarchy and its equality with PSPACE! We introduce the TC0-computable predicates Pos and Neg which share many symmetries and dualities of the boolean case and shed some light on this possibility.

ABSTRACT. About ten years ago, we explained in a widely circulated manuscript how to extend tensorial logic with algebraic effects. Our main illustration was the algebraic theory of mnemoids introduced by Plotkin and Power in order to equip an object of a cartesian category with update and lookup operations on a global store. In this talk, we will give an explicit proof-theoretic and game-theoretic description of the free dialogue category D with finite sums, whose tensorial pole bot is moreover equipped with the algebraic structure (operations and equations) of a mnemoid. This work provides a first and elementary step towards the design of a functorial game semantics integrating local stores and visible strategies.

ABSTRACT. This presentation provides an overview of the ongoing work of the author's PhD project supervised by Pierre Clairambault, Giulio Manzonetto and Alexis Saurin. The presentation focuses on the connections between a polarized proof system and game semantics. In particular, we introduce a hypersequentialized proof system we designed which may be used to provide a syntactic presentation of strategies as in game semantics for MALL (multiplicative addidtive linear logic with least and greatest fixed points).

ABSTRACT. We provide the first formal connection between G¨odel’s Dialectica interpretation and Berry-Curien’s sequential algorithms model, via a parameterized version of G¨odel’s Dialectica inter- pretation which allows us to recast both the Diller-Nahm variant of the interpretation and Berry-Curien’s sequential algorithms model. This illustrates that the Dialectica interpretation has a strong intensional flavour, as the reverse component of the Dialectica interpretation of a function (from environments in the output to environments in the input) corresponds pre- cisely to the computation indices of sequential algorithms (which specify what is needed in the input in order to produce a given output). While a straightforward instanciation gives the usual Diller-Nahm variant of the Dialectica inerpretation, a more involved instanciation provides exactly the sequential algorithms model. We believe that this is a first step towards a convergence between Dialectica-style computational interpretations of logic on one hand, and game semantics flavoured denotational models of various programming languages on the other hand.

ABSTRACT. Answer Set Programming excels at combinatorial search: generating models, solving constraints, and optimizing over discrete choices. SQL-based evaluation excels at data analysis: aggregation, joining, and transforming large datasets. Many real-world problems require both a search phase that explores a combinatorial space, followed by an analytical phase that examines the results, or a pipeline where data preparation feeds into constraint solving and the solutions are analyzed further. We present an integration of ASP into Logica, an open-source logic programming language that compiles to SQL. We introduce \texttt{couldbe}, \texttt{cantbe}, and \texttt{shouldbe} decorators that extend Logica's expressive power with choice rules, integrity constraints, and optimization objectives, respectively. The programmer writes a single Logica program and the system compiles the deterministic fragment to SQL (executed by DuckDB) and the non-deterministic fragment to an ASP program (solved by Clingo). Solutions returned by Clingo are materialized as SQL tables, available within the same program for further analysis using Logica's full analytical power: aggregation, recursive evaluation, and functional composition. The program may contain an arbitrary number of non-deterministic fragments. We illustrate the integration through three examples that combine search and analysis in ways that neither paradigm handles well alone: detecting and neutralizing cliques in a social network via PageRank, identifying strategically essential companies in a supply chain, and analyzing adversarial robustness of graph coloring. The integration is implemented and publicly available as part of the Logica system.

ABSTRACT. Refactoring is a common practice to improve code quality and maintainability while preserving external behavior. In Answer Set Programming, the anthem system supports this process by verifying the external equivalence of two encodings through a translation into first-order formulas, which are subsequently processed by automated theorem provers. However, while theorem proving is often successful for established equivalences, it frequently fails to terminate when programs are non-equivalent, leaving developers without actionable feedback during iterative refactoring. In this paper, we address this shortcoming by developing an approach for the automated generation of counterexamples for external equivalence. We extend an existing transformation for propositional programs to a first-order setting that covers a substantial subset of the clingo language, including non-tight encodings and recursive aggregates. Furthermore, we generalize the transformation to handle private predicates through a novel guess-and-check formulation. Our approach is implemented as an integrated component of the anthem framework, providing developers with concrete witnesses of non-equivalence to facilitate the rapid identification of logical flaws in ASP encodings.

ABSTRACT. This paper focuses on answering “why-not" questions in Answer Set Programming, with an emphasis on user-oriented explanations. Such questions ask why a user’s expectations are not met within an answer set or why a program is unsatisfiable. We address these questions using contrastive explanations, which explain an outcome by contrasting a reference program and, when available, one of its models, with an alternative program–model pair that satisfies the query. The alternative program is obtained through a controlled process of rule addition and removal. Our approach emphasizes flexibility, adapting to different domain settings and supporting preference-based selection among possible explanations. To improve interpretability, we propose a graph-based representation that highlights contrasts while leveraging domain knowledge captured by integrity constraints. These ideas are realized in asplain, a system that computes contrastive explanation graphs via meta-programming in clingo, allows users to configure explanation generation through a tagging mechanism, and supports interactive exploration of the explanation space through a user-friendly interface. Finally, we present a preliminary experiment using large language models to generate natural language explanations from contrastive explanation graphs.

ABSTRACT. We present Strategy Logic as a formalism for reasoning about strategies in multi-agent systems, and survey its main extensions, including imperfect information, epistemic reasoning, quantitative and probabilistic aspects, counting strategies, and hyperproperties.

ABSTRACT. We examine one particular dimension of AI governance: how to monitor and audit AI-enabled products and services throughout the AI development lifecycle, from pre-deployment testing to post-deployment auditing. Combining principles from formal methods with SoTA machine learning, we propose techniques that enable AI-enabled product and service developers and evaluators to perform offline auditing and online (runtime) monitoring of behavioral constraints such as safety constraints, norms, rules and regulations with respect to black-box advanced AI systems, notably LLMs.

ABSTRACT. Nonmonotonic reasoning with conditional belief bases aims at answering the question “Given a belief base Δ and two formulas 𝐴 and 𝐵, does formula 𝐴 entail formula 𝐵 in the context of Δ?”. Answering these inference tasks is usually quite complex as their semantics involve structures that often grow exponentially in signature size. As a means of localizing such inferences tasks, safe conditional syntax splitting has been introduced in order to split conditional belief bases into smaller subbases, allowing to take only the relevant parts of a given belief base into account. Recently, the kinds of splittings that can be exploited for inductive inference have been refined in two ways: Generalized safe splittings broaden the number of splittings exploitable while genuine splittings identify those splittings that can be meaningfully used for inductive inference. While the theoretical aspect of splittings has been investigated in some detail, their implementation has received far less attention. We present algorithms for computing the different kinds of conditional syntax splittings of a given belief base. These algorithms are capable of computing all conditional syntax splittings and finding all safe, generalized safe, and genuine splittings of a belief base. A modular approach ensures that any combination of safe, generalized safe, and genuine, e.g., the genuine and generalized safe splittings, can be easily computed as well. We evaluate an implementation of these algorithms with respect to the number of splittings computed for each kind and the runtime of each algorithm, analyzing in particular the differences between safe and generalized safe splittings, as well as the benefits of genuine splittings.

ABSTRACT. (We submit a (dense) Extended Abstract) We present a general framework and postulates for defaults and default inference. One issue here is the Exceptional Inheritance Paradox, which reveals a serious conflict between well-recognized axioms for default conditionals and natural desiderata for default inference. Reacting to the trichotomy induced by an impossibility result centered on Splitting, we will identify default formalisms exemplifying each branch, including two new ones.

ABSTRACT. The problem of conditional inference is the problem of establishing which conditional statements ("if A, then normally B") should be said to follow from a finite knowledge base of such statements. A recent solution proposed by Booth and Varzinczak is that we should take the disjunctive rational closure (DRC), which is based on the well-known rational closure construction of Lehmann and Magidor, but which returns, in general, a consequence relation which is representable by an interval order over the set of valuations rather than a total preorder, as usually assumed in the literature. Although the DRC has been shown to satisfy several reasonable properties, there are some properties that fail. In particular, it does not satisfy Cut at the level of conditional inference, i.e., adding to the knowledge base a conditional which is already inferred can lead to additional inferences. It also fails the Relevance property, according to which reasoning under syntactically disjoint knowledge bases should be possible to do in a modular way. In this paper, we propose an alternative interval-order based construction, called the trans-rational closure, which addresses, albeit only partially, these deficiencies.

ABSTRACT. The connection between linear logic and process calculi has been studied for decades and is now well-established. In ongoing work, we have developed a new type system for the asynchronous pi-calculus based on linear logic, which enforces deadlock and lock freedom without imposing any determinism, termination or acyclic conditions coming from proofs. We introduce fixpoint replication, a new process construct that expresses recursion with simple types, like the fixpoint combinator in PCF. Fixpoint replication is justified by a natural generalization of the promotion rule in linear logic. Our work provides a unifying view on approaches to concurrency based on session types and on differential linear logic, in which logical features (cocontraction, fixpoints, logical correctness) correspond to behavioral features (non-determinism, non-termination, acyclicity) and may be modularly combined.

ABSTRACT. Linear logic admits a wide range of semantic presentations. One well-known example is phase semantics: an algebraic semantics in which formulas are interpreted in phase spaces, consisting of a commutative monoid and a fixed subset, with respect to which an orthogonality relation is defined. A rather different and much more recent approach is given by base-extension semantics, which defines validity by inductively extending a provability relation on a base -- a set of inference rules over atomic propositions. We establish an equivalence between the two semantics by first defining bidirectional maps between bases and phase spaces, and then constructing an isomorphism between a phase space (resp. base) and its image under the composition of these maps.

ABSTRACT. It is folklore that there is a tight link between biorthogonal-closure constructions, familiar to practitioners of linear logic, and logical relations, as they appear in, for instance reducibility-candidate flavoured proofs of normalisation for typed lambda calculi. One manifestation of this is in the technique of adapted pairs, due to Krivine [17], which weakens the extensionality condition defining a logical relation to facilitate the required induction over types [18]. In this technique, the full logical-relation condition appears as a kind of fixed-point of the adapted-pair condition. We aim to reformulate the duality underlying the definition of adapted pairs using linear logic, and connect this duality to techniques for proving denotational completeness (or definability) in models of the same [20].

ABSTRACT. Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.

ABSTRACT. We discuss the concurrent monads of Rivas and Jaskelioff, a structure axiomatizing effectful notions of computation supporting not only sequential, but also parallel composition. We have previously analyzed accessible concurrent monads on given monoidal ordered category as lax duoid objects in a certain duoidal ordered category. Here we explain the different perspective that concurrent are monads in a certain 2-category and what this entails.

ABSTRACT. Selecting the right variable ordering heuristic to solve a given constraint satisfaction problem (CSP) instance can dramatically influence solver efficiency. Yet, no single heuristic universally outperforms others across all instances. Recent works have shown that interleaving multiple heuristics during search can significantly improve performance. In this paper, we introduce a formal definition to quantify the degree of complementarity between pairs of heuristics. To validate this concept, we solved instances from the XCSP competition using every possible combination of modern heuristic pairs. Our results reveal a strong correlation between the complementarity score of a pair of heuristics and the performance improvement achieved by interleaving them in the search strategy. Even complementary heuristics with poor standalone performance can, when combined, deliver surprisingly good results. These findings suggest that our notion of complementarity represents a critical step forward in understanding why and how alternating heuristics enhances CSP solving.

ABSTRACT. We present KissatEvolve, an LLM-based framework for fully automatic, scalable, and controllable synthesis of SAT solver heuristics. Modern CDCL solvers such as Kissat employ a large ensemble of tightly coupled heuristic components whose joint configuration space is prohibitively large to search exhaustively. Existing LLM-based approaches explore only a narrow slice of this space, confining search to a single solver or a small set of heuristic functions, and optimize exclusively for aggregate PAR-2 without regard for targeted problem subcategories. KissatEvolve is the first framework to address both limitations simultaneously. For scalability, KissatEvolve combines a self-adaptive agentic workflow with a fully parallelized generation-and-evaluation pipeline that spans multiple solver families and heuristic functions concurrently, substantially reducing the wall-clock time required to cover the design space while minimizing human intervention. For controllability, KissatEvolve maintains a densely annotated memory bank that records both high- and low-performing heuristic variants, each enriched with solver analyses, search statistics, and code-diff traces. Selectively retrieved examples condition subsequent LLM generations toward targeting user-specified subcategories (SAT, UNSAT, easy, or hard problems), enabling fine-grained steering of solver behavior. Using KissatEvolve, we conduct a comprehensive study of 17 heuristic functions across 6 SAT solvers, finding improved heuristics for 3 solvers that reduce PAR-2 by 12.80% on average over their respective baselines. We also find that controlled retrieval reduces PAR-2 by up to 43.76% relative to uncontrolled retrieval.

ABSTRACT. Despite the progress observed in machine learning, its successful application to SAT is still very modest. One of the reasons for this is probably the lack of clear challenges and datasets for the ML community to focus on. This would stimulate the community to propose, for example, new neural network architectures that are well suited for SAT search. We propose a methodology and a dataset for training machine learning systems to solve satisfiable formulas. Our dataset consists of random formulas of relatively small size (250 variables) at the threshold, all of which are satisfiable. The task to be predicted is to identify, given an overall assignment, the set of variables that must be flipped to make the formula satisfiable. Our dataset consists of hundreds of thousands of examples (each on a different random formula) with the minimum number of flips that need to be performed, given a total assignment. One of our result is to show that, despite impressive predicting qualities of a Graph Neural Network predictive model on them, a pure machine learning method based solely on the prediction failed on 100\% of the benchmarks while they are trivial for local search SAT solvers from the late 90's. We think that this unveils a key missing piece of current ML approach that could be identified by focusing on our proposed dataset.

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.

ABSTRACT. In this paper, we present CoSP-TL, a two-level architecture that combines tacit reasoning knowledge from Large Language Models with formal symbolic planning to address temporally constrained planning problems expressed in natural language. Our approach employs a hierarchical planner composed of a High-Level Planner, which iteratively refines a natural-language plan until it satisfies a Linear Temporal Logic formula encoding the problem constraints, and a Low-Level Planner, which translates the high-level plan into executable PDDL with extensive validation and error-recovery mechanisms. We evaluate our framework on the recent and challenging LexiCon benchmark across three IPC domains, Blocksworld, Logistics, and Sokoban considering an increasing number of temporal constraints over domain fluents. Results show that our approach significantly outperforms standard LLM-based planning, achieving strong performance on unconstrained problems and maintaining robust results as the number of constraints increases, highlighting the scalability of CoSP-TL in handling temporally constrained planning tasks at which standard LLM planners exhibits substantial performance degradation.

ABSTRACT. An assistive AI agent often has to collaborate with previously unseen agents and humans. Methods considered state of the art for such ad hoc teamwork use a large labeled dataset of prior observations to model the behavior of other agents and to determine the ad hoc agent's behavior. These approaches are resource-hungry, and do not support rapid incremental revisions or transparency, with the necessary resources (e.g., training examples, computation) not readily available in practical domains. Our architecture for ad hoc teamwork embeds the principles of refinement, ecological rationality, and interactive learning, leveraging the complementary strengths of knowledge-based and data-driven methods. For any given goal, an ad hoc agent determines its actions through non-monotonic logical reasoning with: (a) prior domain-specific commonsense knowledge; (b) models learned rapidly to predict the behavior of other agents; and (c) anticipated abstract future tasks based on generic knowledge of similar situations. Further, the agent processes natural language descriptions and observations of other agents' behavior, incrementally acquiring and revising its existing knowledge. We evaluate the capabilities of our architecture in VirtualHome, a realistic 3D simulation environment.

ABSTRACT. We study quadrangular properties of binary relations on a set $X$--i.e., properties defined on configurations of four elements—within an agonistic interpretation, where $xRy$ is interpreted as $x$ ``attacks''~$y$. Such relations induce a suitable notion of ``protection,'' and we provide necessary and sufficient conditions for this notion to be consistent. We characterize the balance property in signed frames in terms of a specific quadrangular property, namely collusivity. In this way, we generalize a classical result in balance theory by offering an alternative method for determining whether a network is polarized. That is, one can identify well-formed groups of agents that agree with one another within the same group (a set of allies) while disagreeing with, or attacking, agents outside the group. Furthermore, we extend the balance theorem to non-symmetric relations, thereby relaxing a condition required in standard balance theory. We conclude by giving a modal characterization of collusive frames, together with corresponding rules in a labeled sequent calculus, and we show that previous modal characterizations of balance are derivable within this system.

ABSTRACT. In this work we explore the use of communication actions in a logic aimed to verify authenticity and safety in cryptographic protocols. We extend a Dynamic Logic with Parallel operator by introducing some concepts based on the Dolev-Yao model. The former has a complete axiomatization which yields a complete axiomatization for new the logic being presented. Finally, we also present a tableaux calculus for this logic, proving its termination, soundness and completeness.

ABSTRACT. Cardinality constraints are one of the most widely used high-level constraints in SAT-based reasoning. Recently, it has been observed experimentally that the input ordering of cardinality encodings can significantly affect the performance of SAT solvers, sometimes even more than the choice of the encoding itself. In this paper, we study this phenomenon from a proof-complexity perspective, showing that encoding the contradictory pair of constraints $x_1+\cdots+x_n \geq k+1$ and $x_1+\cdots+x_n \leq k$, with totalizers and different input orderings, gives rise to exponentially hard formulas for Resolution.

ABSTRACT. In this work we examine the strength of various cutting planes-like proof systems, where we replace the division rule with other inference rules, such as the saturation rule or a (lifted) cover cut rule, which include rules that can derive implied clauses or implied cardinalities and the rounding and index cover cuts. In particular, we show implicational separations between increasingly strong lifted cover cuts, and between cover cuts and saturation. We also show that the index cover cut can be simulated using the rounding cover cut, but that any such simulation requires a linear number of steps.

ABSTRACT. We compare the complexity of a range of new cutting planes (CP) subsystems that exploit cardinality constraints. We show CP paired with cuts from linear programming and mixed integer programming can be powerful especially when considering such cardinality constraints. Through this investigation we re-examine the power of saturation and find an exponential refutation separation between it and these new subsystems.

ABSTRACT. We present a first formal model of ranking-based human–AI aggregation. We represent both human and AI judgments by ranking functions over possible worlds and study how AI advice affects the epistemic quality of a collective decision. To obtain probabilistic guarantees, we introduce a top-choice abstraction that translates ranking aggregation into a voting problem and connects our setting to a recent model from the voting literature. This allows us to model a specific interaction setting that we refer to as AI-follow assistance with concurrent panel revision. The resulting analysis yields a formal account of when AI influence can be epistemically harmful by inducing dependence among human agents.

ABSTRACT. In this work we study offline reinforcement learning (RL) under temporally extended task constraints expressed in Linear Temporal Logic over finite traces (LTLf). Recently, transformer-based approaches such as Trajectory Transformers and Decision Transformers have been adopted to address RL as a sequence modeling problem. However, these methods optimize purely for reward and do not account for high-level temporal requirements. Here, we introduce a neurosymbolic framework that injects LTLf background knowledge into such transformer-based RL policies. Our approach compiles LTLf formulas into deterministic finite automata (DFAs) and integrates them into the learning process through a differentiable representation and a logic-based loss function. In particular, we derive differentiable satisfaction signals from DFA progression and use them as a regularization term during training. The resulting method is architecture-agnostic across different models. We evaluate the proposed framework on navigation environments with specification suites covering combinations of safety and reachability temporal properties. Experimental results show that incorporating background knowledge not only improves constraint satisfaction, but also maintains competitive return compared to vanilla baselines.

ABSTRACT. Retrieval-Augmented Generation is as a paradigm that integrates the parametric knowledge of a Large Language Model with external non-parametric information through a retrieval component. While RAGs have shown strong performances on several tasks, their answers may still be prone to errors as of the approximate nature of the retrieval process they utilize. In this paper, we argue that the output of a dense retriever can be interpreted as a set of noisy samples that could be retrieved via a query that it is implicitly executed over the data. A symbolic representation of this latent intention can then be reconstructed from the samples and used to compute the final retrieval result. We instantiate this idea in a concrete retrieval architecture, which we call Symbolic-Assisted Dense Retriever, and present a preliminary use case scenario and experimental evaluation.

ABSTRACT. Temporal logics and their automata-based counterparts have risen as languages for reasoning about processes and verifying their properties. Increasingly, though, the events in a process refer to observations perceived and classified by a neural network, calling for a mixed formalism capable of dealing with the uncertainty of these classifications. We propose Deep Weighted Finite Automata, a new neuro-symbolic architecture combining formal temporal specifications and neural classifications. We also show how to make probabilistic inferences and compute the most likely execution given a sequence of perceptions.