ABSTRACT. Temporal Synthesis studies the automatic synthesis of interactive programs (technically called strategies) from declarative specifications expressed in temporal logic. In this talk, we show how Temporal Synthesis provides a principled foundation for strategic reasoning in autonomous AI systems, leading to what we may call Symbolic Coding Agents. Symbolic Coding Agents use temporal synthesis to generate symbolic code, including strategies, guard rails, and decision-making monitors, thereby grounding deliberative behavior in logical specifications. The key to this research path lies in the rich body of concepts developed in reasoning about actions and planning, combined with a precise treatment of nondeterministic environments and temporal objectives. In such settings, plans must be treated as strategies rather than being blurred with individual execution traces, and goal satisfaction evolves during execution rather than being reducible to reaching states with fixed properties. These features are naturally captured within the temporal synthesis framework underlying Symbolic Coding Agents. Technically, we focus on synthesis from Linear Temporal Logic on finite traces (LTLf). LTLf specifications compile into deterministic finite automata (DFAs), which can be viewed as two-player game arenas, yielding efficient and scalable synthesis procedures. We then lift these finite-trace results to infinite traces through the Manna–Pnueli hierarchy, introducing LTLf+ and its obligation fragment while largely preserving algorithmic simplicity. Finally, we move beyond synthesizing individual strategies to analyze the space of all strategies satisfying a specification. By characterizing the set of compliant execution traces, without assuming individual strategies to be analyzable, we provide formal foundations for Symbolic Coding Agents to synthesize guard rails and decision-making monitors, as well as tools for responsibility attribution in agentic AI systems composed of multiple agents that make decisions independently.

ABSTRACT. Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL → DPA → COCOA), where the first step ignores natural colors and requires intricate constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid these complex constructions and obtain a more direct translation from LTL to COCOA. In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new route from LTL to DPA and avoids the aforementioned intricate constructions. It relies on standard operations on weak alternating automata, Miyano-Hayashi's breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.

ABSTRACT. We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that for layered automata both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences.

ABSTRACT. We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains, ie, given a formula that refines a relation between subsets of the input model, we are interested in the existence of a formula that defines a function that selects for all sets in the domain of the relation a unique set such that the pair of the two is in the relation. It is known that uniformisation of MSO is not possible over the class of countable ordinals. We show in this work that the maximal uniformisation degree is reached if we add to the logic a new predicate that selects in each set, if possible, a cofinal subset of a of order-type $\omega$. Said differently, all formulas of MSO can be uniformised over the class of countable ordinal chains by using a formula of this extended logic.

ABSTRACT. Rabin's Tree Theorem says that the MSO theory of the infinite binary tree $2^*$ is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to $2^{\leq \omega}$, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in $2^{\leq \omega}$ by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin's Theorem can be extended to the new framework. The only missing part is a conjecture about finite memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.

ABSTRACT. We propose a simple space-cost measure for the lambda-calculus, that extends the natural model measuring the size of the terms by also taking into consideration their origin. This new model is able to capture sublinear space complexity and we prove that, in the context of weak reduction, it is reasonable with respect to standard complexity theory. Precisely, we show that the weak lambda-calculus and Turing machines can simulate each other with a constant-factor space overhead, for any computation of logarithmic or higher space complexity. This implies that the weak lambda-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including LOGSPACE and PSPACE.

ABSTRACT. Semantic notions in programming language theory are commonly specified by syntax-based systems, and their metatheory --- including congruence of bisimilarity, determinacy of evaluation, confluence of reduction, and type safety --- is typically developed syntactically, relying heavily on termwise reasoning. This leads to representation-dependent results and to a systematic duplication of metatheoretic effort across different calculi and syntactic presentations. This paper proposes a pointfree, algebraic approach to the metatheory of syntax-based systems. Rather than reasoning about terms, inference mechanisms, or other syntactic notions --- or about their abstract structure --- we shift attention to the algebra of semantic predicates induced by syntax and treat such predicates as first-class objects. This algebra is defined abstractly, without reference to any underlying term structure. Term-based rules and manipulations are recast as algebraic operations, while metatheoretic properties are formulated algebraically --- typically as quasi-equations --- and established once and for all at the algebraic level, independently of any particular syntactic representation. As a first step towards a systematic algebraization of metatheory, we prove a collection of abstract metatheorems, including confluence of reduction, determinacy of evaluation, and congruence of applicative bisimilarity.

ABSTRACT. Friedman-Simpson’s original program of reverse mathematics, as is also the case for most of standard mathematics, has been developed in classical subsystems of second-order arithmetic. As such, (classical) reverse mathematics presents various limitations from a constructive point of view, since for instance they are unable do distinguish between a statement and its contrapositive (e.g. dependent choice and the bar induction principles). The case of (Weak) König Lemma (WKL) and Fan Theorem (FT) is particularly interesting in that regard: while KL is well-known to imply FT, and if constructivists like Brouwer rejected the former while admitting the latter, the converse implication has not been much studied for years. It is only recently that a growing enthusiasm for constructive reverse mathematics pushed towards a finer-grained analysis of the connection between such principles. In addition to intuitionistic reverse mathematics, the realizability approach to logical principles adds a computational meaning to purely logical statements. We follow this path to investigate the computational meaning to Brouwer's Fan Theorem: building on recent work by Lubarsky and Rathjen, we first construct a realizability interpretation of higher-order logic validating FT while refuting WKL. This interpretation relies on a λ-calculus extended with oracles while preserving a notion of continuity for realizers. We then push this approach a step further to show the robustness of this realizability interpretation by identifying, in the abstract and general setting of evidenced frames, sufficient computational conditions entailing FT.

ABSTRACT. Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as $\lambda$-terms. One distinguishing feature of the presheaf-based perspective is its abstract syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, modelling substitution in the spirit of Fiore~et.~al.'s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from an action. We then demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories, but also yields novel notions of substitution tensor for nominal sets and their relatives, such as renaming sets. Our results also shed new light on the relation between presheaves and nominal sets, in which we establish novel correspondences between different versions of nominal sets and suitable (pre-)sheaf categories.

ABSTRACT. We introduce \emph{Backtrackable Inprocessing} (BI), a framework that enables applying inprocessing under the current trail at any decision level, at any point during incremental SAT solving. Our approach lifts the long-standing restriction that inprocessing must be performed only at the global decision level, thereby substantially increasing its potential effectiveness. We focus on three highly efficient core techniques: subsumption, self-subsuming resolution, and Bounded Variable Elimination (BVE). We show how to ensure sound backtracking in the presence of inprocessing, and demonstrate that applying BI for incremental preprocessing after propagating assumptions yields significant performance improvements on Bounded Model Checking (BMC) benchmarks from the Hardware Model Checking Competition 2017. Implemented in the Island SAT solver (IntelSAT's fork), BI enables solving ~1.5X as many difficult bounds as the baseline global-level incremental preprocessor.

ABSTRACT. We present several novel encodings for cardinality constraints, which use fewer clauses than previous encodings and, more importantly, introduce new generally applicable techniques for constructing compact encodings. First, we present a CNF encoding for the $\textsf{AtMostOne}(x_1,\dots,x_n)$ constraint using $2n + 2 \sqrt{2n} + O(\sqrt[3]{n})$ clauses, thus refuting the conjectured optimality of Chen's product encoding. Our construction also yields a smaller monotone circuit for the threshold-2 function, improving on a 50-year-old construction of Adleman and incidentally solving a long-standing open problem in circuit complexity. On the other hand, we show that any encoding for this constraint requires at least $2n + \sqrt{2n} - 3$ clauses, which is the first nontrivial unconditional lower bound for this constraint and answers a question of Ku{\v c}era, Savick{\'{y}}, and Vorel. We then turn our attention to encodings of $\textsf{AtMost}_k(x_1,\dots,x_n)$, where we introduce grid compression, a technique inspired by hash tables, to give encodings using $2n + o(n)$ clauses as long as $k = o(\sqrt[3]{n})$ and $4n + o(n)$ clauses as long as $k = o(n)$. Previously, the smallest known encodings were of size $(k+1)n + o(n)$ for $k \le 5$ and $7n - o(n)$ for $k \ge 6$.

ABSTRACT. Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with $n$ variables into an equivalent 2-CNF formula with $(\tfrac{\lg(3)}{4}+o(1))\,\tfrac{n^2}{\log n}$ clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from $\tfrac{\lg(3)}{4} \approx 0.396$ to $1$, and that no reencoding method can achieve a constant below $0.25$. On the other hand, for the at-most-one constraint on $n$ variables, we prove that idealized BVA cannot reencode this constraint using fewer than $3n-6$ clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses $2n+o(n)$ clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.

ABSTRACT. Approximation semantics capture the observable behaviour of {\lambda}-terms, with Böhm Trees and Taylor Expan- sion standing as two central paradigms. Although conceptually different, these notions are related via the Commutation Theorem, which links the Taylor expansion of a term to that of its Böhm tree. These notions are well understood in Call-by-Name {\lambda}-calculus and have been more recently introduced in Call-by-Value settings. Since these two evaluation strategies traditionally require separate theories, a natural next step is to seek a unified setting for approximation semantics. The Bang-calculus offers exactly such a framework, subsuming both CbN and CbV through linear-logic translations while providing robust rewriting properties. However, its approximation semantics is yet to be fully developed. In this work, we develop the approximation semantics for dBang, the Bang-calculus with explicit substitu- tions and distant reductions. We define Böhm trees and Taylor expansion within dBang and establish their fundamental properties. Our results subsume and generalize Call-By-Name and Call-By-Value through their translations into Bang, offering a single framework that uniformly captures infinitary and resource-sensitive semantics across evaluation strategies.

ABSTRACT. We study invertibility of lambda-terms modulo lambda-theories. Here a fundamental role is played by a class of lambda-terms called finite hereditary permutations (FHP) and by their infinite generalisations (HP). More precisely, FHPs are the invertible elements in the least extensional lambda-theory lambda-eta and HPs are those in the greatest sensible lambda-theory H*. Our approach is based on inverse semigroups, algebraic structures that generalise groups and semilattices. We show that FHP modulo a lambda-theory T is always an inverse semigroup and that HP modulo T is an inverse semigroup whenever T contains the theory of Böhm trees. An inverse semigroup comes equipped with a natural order. We prove that the natural order corresponds to eta-expansion in FHP/T, and to infinite eta-expansion in HP/T. Building on these correspondences we obtain the two main contributions of this work: firstly, we recast in a broader framework the results cited at the beginning; secondly, we prove that the FHPs are the invertible lambda-terms in all the lambda-theories lying between lambda-eta and H+. The latter is Morris' observational lambda-theory, defined by using the beta-normal forms as observables.

ABSTRACT. Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm. We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with eta-equality (Scott, Park, etc.). Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

ABSTRACT. ASP(Q) extends Answer Set Programming (ASP) with Quantifiers over answer sets. In this paper we focus on the class of ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASP(Q)^w. 2-ASP(Q)^w is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class \Delta^P_3. On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP(Q)^w programs, including tight completeness results and the analysis of nontrivial cases that have not been addressed in previous works. On the practical side, we introduce novel strategies for computing (optimal) quantified answer sets in the casper system, that rely on a Counterexample-Guided Abstraction Refinement (CEGAR) technique tailored to ASP(Q). An experimental evaluation on hard benchmarks from different application domains shows that the proposed techniques are effective in practice.

ABSTRACT. In this paper, we explore the concept of modularity in first-order answer set programming (ASP). We introduce a new formalism called parametric modular logic programs, which allows defining subprograms with parameters and intensionality statements. We demonstrate how this formalism can capture the semantics of clingo-programs with collective control, a feature that enables structuring and instantiating subprograms. We provide theoretical foundations for modular ASP, illustrate its usefulness, and connect to traditional non-modular ASP.

ABSTRACT. Constraint Answer Set Programming (CASP) is a hybrid paradigm that enriches Answer Set Programming (ASP) with numerical constraint processing, something required in many real-world applications. The usual specification of constraints in most CASP solvers is closer to the numerical back-end expressiveness and semantics, rather than to standard specification in ASP. In the latter, numerical attributes are represented with predicates, and this allows declaring default values, leaving the attribute undefined, making non-deterministic assignments with choice rules, or using aggregated values. In CASP, most (if not all) of these features are lost once we switch to a constraint-based representation of those same attributes. In this paper, we present the flingo language (and tool) that incorporates the aforementioned expressiveness inside the numerical constraints, and we illustrate its use with several examples. Based on previous work that established its semantic foundations, we also present a translation from the newly introduced flingo syntax to regular CASP programs following the clingcon input format.

ABSTRACT. We explore a fuzzy modal logic that can formalise probabilistic reasoning about actions and knowledge. In particular, we deal with contexts involving statements about events expressed via modal formulas, e.g., ‘after doing~a, the probability of A~knowing that p holds increases / decreases / is equal to 0.25’, ‘according to A, p is equally likely to happen after doing a or b’, etc. We define the semantics of the logic on Kripke frames equipped with probability measures. We analyse the complexity of deciding the satisfiability of formulas of our logic over finitely branching models for the cases of the full language and its fragments of various expressivity.

ABSTRACT. We study the problem of explaining observations about the probabilities of events such as ‘it rains 20% of the time’, ‘rain and snow are equally likely’, etc. We explain these statements with a probability distribution or a statement about probabilities of (other) events that are consistent with our knowledge and entail the observation. We formalise this problem in a fuzzy probabilistic logic FP. We define and motivate the notions of abduction problems and their solutions. We analyse the complexity of solution recognition and existence for a given abduction problem in FP for the case of full language and its disjunctive-clause fragments. We also obtain a translation of classical probabilistic abduction (finding the most likely explanation of a given event) to FP.

ABSTRACT. Goal recognition aims to infer an agent’s goal from observations of its behaviour. In realistic settings, recognition can benefit from exploiting hierarchical task structure and reasoning under uncertainty. Planning-based goal recognition has made substantial progress over the past decade, but to the best of our knowledge no existing approach jointly integrates hierarchical task structure with probabilistic inference. In this paper, we introduce the first planning-based probabilistic framework for hierarchical goal recognition over Hierarchical Task Networks (HTNs). We instantiate the framework by exploiting an HTN planner with a three-stage generative model for likelihood estimation, yielding posterior distributions over goal hypotheses. Empirical results show improved recognition performance over the existing HTN-based recognizer on HTN benchmarks. Overall, the framework lays a foundation for probabilistic goal recognition grounded in hierarchical planning structure, moving goal recognition toward more practical settings.

ABSTRACT. Recent work by Chatzi et al. and Ravfogel et al. has developed, for the first time, a method for generating counterfactuals of probabilistic Large Language Models. Such counterfactuals tell us what would - or might - have been the output of an LLM if some factual prompt x had been x* instead. The ability to generate such counterfactuals is an important necessary step towards explaining, evaluating, and eventually improving, the behavior of LLMs. We argue, however, that the existing method rests on an ambiguous interpretation of LLMs: it does not interpret LLMs literally, for the method involves the assumption that one can change the implementation of an LLM's sampling process without changing the LLM itself, nor does it interpret LLMs as intended, for the method involves explicitly representing a nondeterministic LLM as a deterministic causal model. We here present a much simpler method for generating counterfactuals that is based on an LLM's intended interpretation by representing it as a nondeterministic causal model instead. The advantage of our simpler method is that it is directly applicable to any black-box LLM without modification, as it is agnostic to any implementation details. The advantage of the existing method, on the other hand, is that it directly implements the generation of a specific type of counterfactuals that is useful for certain purposes, but not for others. We clarify how both methods relate by offering a theoretical foundation for reasoning about counterfactuals in LLMs based on their intended semantics, thereby laying the groundwork for novel application-specific methods for generating counterfactuals.

ABSTRACT. Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting (#SAT), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation.Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers.

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 \emph{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. Non-monotonic reasoning is essential for drawing plausible conclusions from incomplete information. Many approaches model changing belief states using Ordinal Conditional Functions (OCFs), which assign degrees of surprise to possible worlds. This paper demonstrates how OCFs are ideally suited for the knowledge compilation paradigm, particularly with Binary Decision Diagrams (BDDs). We introduce a compilation pipeline for System Z, a prominent ranking-based semantics, which pre-compiles a conditional knowledge base into a set of materialized theories represented by BDDs. This compilation enables polynomial-time conditional entailment and efficient, incremental updates, avoiding costly re-computation. We further extend this approach using Algebraic Decision Diagrams (ADDs) to directly compile the entire ranking function, facilitating direct and efficient implementation of complex belief revision operations such as Spohn conditioning.

ABSTRACT. We present a knowledge compilation approach for existential and universal quantification in alternating automata. Knowledge compilation transforms formulas into normal forms with special properties that enable efficient answering of questions of interest. For Boolean formulas, several normal forms that have proven effective for existential/universal quantification, and even for functional synthesis, have been studied in the literature. For infinite word automata, quantification is a fundamental operation in verification tasks such as QPTL satisfiability checking and HyperLTL model checking. Existing algorithms rely on nondeterministic infinite word automata, where existential projection can be efficiently performed state-wise, but universal projection requires complementation. Complementing nondeterministic infinite word automata, however, is expensive in practice, making existing algorithms infeasible for automata in practice. Towards addressing this problem, we propose novel knowledge compilation techniques for existential and universal quantification on alternating safety automata. Our approach compiles alternating automata into normal forms where projection can be applied uniformly and efficiently to each state's transition function. Using the compilations for each type of quantification, we can effectively eliminate a sequence of alternating quantifiers in formulas without complementation. Our BDD-based prototype demonstrates the practical effectiveness of our algorithms on a suite of QPTL satisfiability benchmarks.

ABSTRACT. We present a new approach for computing complete, stable and preferred extensions of abstract argumentation frameworks. Unlike existing approaches that reduce these problems to the propositional satisfiability problem and solve them with the help of SAT-solvers, our approach solves them directly by making use of the fact that the mentioned extensions are contained in certain closure systems. Our algorithms enumerate these closed sets and filter the searched extensions. Experimental results show that our approach outperforms the existing approaches for a large number of the test cases.

ABSTRACT. In Dung-style abstract argumentation, various semantics capture notions of acceptability of arguments. The admissibility semantics capture the notion that an argument can be consistently defended from any potential counterargument. Weak semantics often relax the demands of admissibility by restricting which counterarguments must be taken seriously (e.g., discounting self-defeating or otherwise incoherent attacks). Many prominent proposals for weak semantics remain extension-based in a stronger sense. While these semantics discount attacks from arguments which are considered unreasonable, they still require a uniform defense against all reasonable arguments, even if they are collectively incoherent. This uniformity can be too demanding when defensibility is inherently strategic, and thus the appropriate reply depends on the opponent’s line of attack. We introduce tenability, a family of dialogue-based semantics that formalize when a designated argument (or a set of arguments) can be maintained in debate by a proponent against any coherent (conflict-free) attack which the opponent may present. The approach is motivated by three natural benchmark patterns—self-defeating attack, floating assignment, and disjunctive reinstatement—on which tenability behaves differently from all weak semantics previously considered in the literature. We define three variants--static tenability, tenability, and strong tenability--via monotone commitment games over finite conflict-free moves, differing in the obligations imposed on the disputants. We establish the relative strength of these notions, prove implications and separations with previously studied weak semantics, and % (including admissibility) we analyze computational complexity on finite frameworks: deciding static tenability is $\Pi^P_2$-complete, while deciding tenability and strong tenability is PSPACE-complete.

ABSTRACT. Argumentation theory provides a formal framework to represent and analyse debates where participants propose arguments that attack or support others and assign scores expressing their opinions. Quantitative Bipolar Argumentation Frameworks model such debates by assigning initial weights to arguments and using semantics to compute final scores that reflect attackers’ and supporters’ influence. One of the major challenge is setting appropriate initial weights when debaters’ opinions are uncertain. In this paper, we introduce a formal approach to uncertainty propagation in Quantitative Bipolar argumentation frameworks by representing initial weights as belief mass functions over a discretized unit interval. We introduce two new propagation models: (i) an exact model that computes final mass functions by combining focal elements of initial weights with parent arguments via bipolar gradual semantics; (ii) a practical approximation that projects the exact mass onto a user-specified partition and reconstructs masses using the Moebius inverse. We prove mathematical properties of the projection and show that the baseline, while computationally efficient, can be overconfident by failing to preserve expectations. Our approximation reduces the exponential complexity of the exact model while satisfying Epistemic Cautiousness, yielding acceptability intervals that contain true theoretical expectations and balancing tractability with theoretical soundness.

ABSTRACT. Contestable AI requires that AI-driven decisions align with given preferences. Various types of argumentation frameworks have been shown to support forms of contestability. In this paper we focus on the little-studied Edge-Weighted Quantitative Bipolar Argumentation Frameworks (EW-QBAFs), where arguments have a base score as in QBAFs but attacks and supports (edges) are weighted. After generalising gradual semantics and properties thereof from QBAFs to EW-QBAFs, we introduce the contestability problem for EW-QBAFs, which asks how to modify edge weights to achieve a desired strength for a specific topic argument. To address this problem, we propose gradient-based relation attribution explanations (G-RAEs), which quantify the sensitivity of the topic argument's strength to changes in individual edge weights, thus providing interpretable guidance for weight adjustments towards contestability. Building on G-RAEs, we develop a heuristic algorithm that progressively adjusts the edge weights to attain the desired strength. We evaluate our approach experimentally on synthetic EW-QBAFs that simulate the structural characteristics of personalised recommender systems and multi-layer perceptrons, demonstrating that it can support contestability effectively.

ABSTRACT. The logic of bunched implications (BI), introduced by O’Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the $\{\land, \lor, \neg, \mimp\}$-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then $\mimp$ splits into two divisions $\backslash, \slash$). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

ABSTRACT. Substructural logics selectively omit structural rules from classical or intuitionistic proof calculi, providing a framework to formalize resource-sensitive reasoning. For logics with contraction or weakening admitting cut-free sequent calculi, proof search had been analyzed in the literature using well-quasi-orders on N^d (Dickson’s lemma), yielding Ackermannian upper bounds via controlled bad-sequence arguments. For hypersequent calculi, that argument lifted the ordering to the powerset, since a hypersequent is a (multi)set of sequents. From the perspective of the fast-growing hierarchy, this induced a jump from Ackermannian to hyper-Ackermannian complexity. This suggested that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FLec/FLew) inherently entail hyper-Ackermannian upper bounds. We show that this intuition does not hold: every extension of FLec and FLew admitting a cut-free hypersequent calculus has an Ackermannian upper bound on provability. The key technical insight is avoiding the powerset. For this, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case also introduces a Karp-Miller style acceleration. Our Ackermannian upper bound is optimal (realized by the logic FLec), and it improves the upper bound for the fundamental fuzzy logic MTL.

ABSTRACT. Subtyping in programming languages can be analysed as an entailment relation by means of proof theory. We look at two main families of systems: intersection types and polymorphic subtyping. We introduce a restriction IS of the Lambek calculus which is stable under cut-elimination and conservatively extends these two subtyping relations. IS is an intuitionistic non-commutative linear sequent calculus which provides a natural logical setting for the study of subtyping. We recover sequent calculi from the literature as restrictions of IS (thanks to a proof-theoretical analysis: admissibility, invertibility, focusing, etc.), so that IS appears as a unifying logic. We also develop translations relating IS with relevant logic, (unconstrained) Lambek or cyclic linear logic.

ABSTRACT. History-deterministic automata, often also known as good-for-games, are an intermediate model between deterministic and nondeterministic automata, which are particularly well-suited for applications in verification and reactive synthesis. We show that deciding whether a parity automaton is history-deterministic is in NP. Our result matches an NP-hardness lower bound (Prakash 2024) and builds on insights from a fixed-parameter tractable algorithm (Lehtinen and Prakash 2025). This settles the complexity of the problem, which has been open since 2006.

ABSTRACT. We consider a large family of product operations of formal power series in noncommuting indeterminates, the classes of automata they define, and the respective equivalence problems. A \emph{$P$-product} of series is defined coinductively by a \emph{polynomial product rule $P$}, which gives a recursive recipe to build the product of two series as a function of the series themselves and their derivatives. The first main result of the paper is a complete and decidable characterisation of all product rules $P$ giving rise to $P$-products which are bilinear, associative, and commutative. The characterisation shows that there are infinitely many such products, and in particular it applies to the notable Hadamard, shuffle, and infiltration products from the literature. Every $P$-product gives rise to the class of \emph{$P$-automata}, an infinite-state model where states are terms. The second main result of the paper is that the equivalence problem for $P$-automata is decidable for $P$-products satisfying our characterisation. This explains, subsumes, and extends known results from the literature on the Hadamard, shuffle, and infiltration automata. We have formalised most results in the proof assistant Agda.

ABSTRACT. We provide general criteria ensuring the existence of minimal canonical models of streaming transducers, namely, devices that read an input word and produce a corresponding output value by iteratively updating an internal memory. This abstract model of transducer subsumes classical (sub)sequential transducers (Schützenberger), streaming string-to-string transducers (Alur-Černý), polynomial automata (Benedikt et al.), and variants of streaming string-to-tree transducers (Alur-D'Antoni). We then instantiate our criteria to minimize variants of the latter transducers, where outputs are terms that are constructed incrementally, by extending (tuples of) terms either at the leaves or at the roots.

ABSTRACT. Modern SAT solvers are based on the conflict-driven clause learning (CDCL) paradigm, which can be simulated by the resolution proof system. This limits solver effectiveness on instances known to be hard for resolution. Certain approaches, such as parity reasoning, have been shown to be effective in this context, but are hard to integrate with CDCL, in particular, with mainstream proof certificates. The powerful yet simple Extended Resolution (ER) proof system provides an alternative but is not widely used in SAT solving despite having proof certificates for decades and using it effectively remains an open challenge. This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL. We further propose a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally. Previous work on bounded variable addition focused on AND gates and original clauses only. Our experimental evaluation shows substantial improvements on hard combinatorial benchmark families without performance degradation on the SAT Competition.

ABSTRACT. We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in $n$, where $n$ is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.

ABSTRACT. State-of-the-art SAT solvers increasingly use techniques beyond resolution. For instance, adding redundant clauses allows the solver to reduce the solution space, i.e., to break symmetries. We investigate the strength of relatively weak redundancy reasoning: conditional autarkies, Set-Blocked Clauses (SBC) with no new variables and no deletions. We show that adding conditional autarkies (as SBC clauses) on top of resolution allows efficient refutations of a number of natural combinatorial principles that may occur in SAT benchmarks. In particular, we give efficient proofs of the perfect matching on a grid, the mutilated chessboard, and the relativized pigeonhole principle.

ABSTRACT. Since their introduction by Atserias, Kolaitis, and Vardi in 2004, proof systems where each line is represented by an OBDD have been intensively studied as they allow to compactly represent Boolean functions. We extend this line of work by considering representation formats that can be even more succinct than OBDDs and have gained a lot of attention in the area of knowledge compilation: sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs). We show that both variants can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. Furthermore, we investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed. Here we obtain several separations and identify interesting open problems. To streamline our proofs we establish a sat-to-unsat lifting theorem that might be of independent interest: it turns satisfiable CNFs that are hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs that are hard to refute in the corresponding proof system.

ABSTRACT. Autonomous agents acting in realistic Multi-Agent Systems (MAS) should be able to adapt during their execution. Standard strategic logics, such as Alternating-time Temporal Logic (ATL), model agents' state or history-dependent behaviour. However, the dynamic treatment of agents' available actions and their knowledge of required actions is still rarely addressed. In this paper, we introduce ATL with Dynamic Actions (ATL-D), which models the process of granting and revoking actions, and its extension ATEL-D, which captures how such updates affect agents’ knowledge. Beyond the conceptual contribution, we provide several technical results: we analyse the expressivity of our logic in relation to ATL, study its relation to normative systems, and provide complexity results for relevant computational problems.

ABSTRACT. We study an Agentic AI setting where we have only partial control over the strategic actions of a set of autonomous agents with independent sequential decision-making capabilities, building on LTL synthesis originally studied in formal methods. Specifically, we assign to each agent individually a task expressed in LTL, and assumptions on the strategies employed by its peers and that the agent can exploit while synthesizing a strategy to realize its task. While we can solve the synthesis problem under assumptions for each such agent we are not only interested in (1) synthesizing strategies for individual agents. Indeed, assumptions in turn are recursively defined through these strategy spaces. Importantly, we do not assume the ability to access or analyze an agent's internal strategy, as we make no assumptions about the nature of the decision makers, which may be, for example, ML-based. Instead, we focus on (2) characterizing the set of traces that are generated by strategies that realize the specification assigned to each agent. Using this characterization, we are able to (3) verify that the whole system, when in execution, satisfies a global objective, regardless of the strategies chosen by the agents from their allowed spaces. Moreover, by observing the evolution of the execution trace, we can (4) identify whether an agent makes a move that violates its specification and assign precise responsibility for the violation. Technically, we present automata-theoretic techniques to solve these problems, and show that each of them is 2EXPTIME-complete, matching the complexity of classical LTL synthesis.

ABSTRACT. Bisimulation is a crucial tool for investigating and understanding the semantic properties of labeled transition systems (LTSs) and relational models in general. In particular, it plays a fundamental role in characterizing model equivalence with respect to a given logical language and in guiding the construction of minimal models. In this paper, we study bisimulation in the context of a logic for expressing knowing-how assertions, which are related to an agent's ability to achieve a given goal. We begin by revisiting an existing notion of bisimulation for this logic and reformulating it using purely semantic clauses. We then establish adequacy results for this new notion. Next, we provide a computational analysis of the problem of checking whether two models are bisimilar. In particular, we show that this problem is \PSPACE-complete. We also investigate two approaches to model minimization in this setting, each exhibiting different computational properties. Along the way, our systematic study of bisimulation yields additional by-product results, w.r.t., for example, the complexity of the definability problem for this logic.

ABSTRACT. In streaming applications, it is often required to detect situations of interest, by means of temporal pattern matching, with minimal latency. In the maritime domain, e.g., where it is crucial to prevent activities that are harmful to the environment, we need to report illegal fishing activities, based on streams of low-level vessel actions, as soon as possible. Streams often include events with delayed effects. In multi-agent voting protocols, e.g., a proposed motion may be seconded at the latest by some time in the future. In simulations of biological systems, a signal may lead to the deactivation of the functions of a gene after a time delay. We propose a formal computational framework that handles streams including events with delayed effects. We present the syntax, semantics and reasoning algorithms of our proposed framework, and demonstrate its correctness and complexity. Furthermore, we present a reproducible analysis on large synthetic and real data streams, from the fields of composite event recognition, multi-agent systems and biological feedback processes, and compare the efficiency of our approach with state-of-the-art systems that can perform stream reasoning in these domains. Our results demonstrate that our framework is capable of reasoning over very large streams, including events with delayed effects, while outperforming the state-of-the-art, often by orders of magnitude.

ABSTRACT. Abduction in knowledge representation is often framed as “ex- plaining away” inconsistencies between a background theory and observations by hypothesizing missing facts or exceptions. Despite decades of KR work on abduction, there are few mod- ern benchmarks that (i) require genuine first-order relational reasoning, (ii) admit unambiguous, solver-checkable verifica- tion, and (iii) produce informative error analyses rather than binary right/wrong judgments. We introduce ABD, a family of default–exception abduction tasks over small finite relational worlds. Each instance provides (a) a set of finite structures with observed facts, and (b) a fixed default-like first-order theory that may be violated by those observations. A model must output a first-order abnormality rule α(x) that defines an exception predicate Ab(x) ↔α(x), restoring satisfiability while keeping exceptions sparse. We formalize three observation regimes with distinct comple- tion semantics. ABD-Full assumes closed-world observation. ABD-Partial allows unknown atoms under existential com- pletion: α is valid if some completion makes the repaired theory satisfiable, with cost optimized in the best case. ABD- Skeptical uses universal completion: αis valid only if the repaired theory is satisfiable under every completion, with cost measured in the worst case. Because domains are finite, validity and costs are computed via SMT (Z3), enabling exact verification and controlled difficulty. We evaluate eight frontier LLMs on 600 instances spanning all three scenarios and seven default theories. The best models achieve over 90% training validity, but parsimony gaps of∼1– 1.6 extra exceptions per world remain. Holdout evaluation reveals distinct generalization profiles: in ABD-Full and ABD- Partial, the dominant failure is parsimony inflation; in ABD- Skeptical, it is validity brittleness—rules that work on training often break on holdouts—while survivors show smaller gap inflation.

ABSTRACT. Abductive expansion is an AGM-style belief-change operation that accommodates new information by adding explanatory hypotheses rather than incorporating the input outright. In contrast to belief sets, belief bases are finite and non-deductively closed, allowing a distinction between explicit and implicit beliefs. We extend abductive belief-change operations to belief bases relative to a hypothesis space, treating the base as firm beliefs and maintaining a separate space of tentative hypotheses that is conditioned on new inputs. We present constructive methods and an axiomatic characterization, and prove representation theorems for the resulting class of operators.

ABSTRACT. Given a knowledge base (KB) with a non-entailed fact, the ABox abduction problem asks for possible extensions of the KB that would entail this fact. This problem has many applications, ranging from diagnosis to explainability and repair. ABox abduction has been well-investigated for consistent KBs and classical semantics, but little is known for the case of inconsistent KBs which can be caused by erroneous data. In this paper we define suitable notions of abduction in this setting and propose criteria that guide abduction towards "useful" hypotheses. To regain meaningful reasoning in the presence of inconsistencies, we use well-established repair semantics. We provide a comprehensive landscape of the complexity of ABox abduction under repair semantics treating different variants of the abduction problem for the light-weight description logics DL-Lite and EL with bottom.

ABSTRACT. This is an extended abstract of the manuscript ’On Validating Propositional Logic System Descriptions for Fault Diagnosis’ (Diedrich, Moddemann, and Niggemann, 2026) that was published in the journal Engineering Applications of Artificial Intelligence in January, 2026.

ABSTRACT. Inspired by revealed preference in economics, we study revealed epistemic trust: an agent’s (dis)trust in an information source is typically hidden, while her accept/reject behavior leaves observable traces. We model such traces by an acceptance function that maps each reported set of formulas to the subset the agent accepts. We develop two complementary models: a white-list mode, where acceptance is supported by trusted information in the report, and a black-list mode, where acceptance avoids distrusted patterns via a cautious remainder-set/full-meet construction. For both modes, we provide postulate-based representation theorems and show how canonical ``revealed'' trust and distrust cores can be reconstructed from the acceptance function itself.

ABSTRACT. We study belief contraction for multi-agent systems in the framework of ‘soft’ (AGM-friendly) Dynamic Epistemic Logic. We look at three different kinds of belief contraction proposed in the Belief Revision literature (severe withdrawal, conservative contraction and moderate contraction), considering them as operations on epistemic plausibility models. We provide sound and complete axiomatizations for logics having dynamic operators for these forms of contraction, in the presence of known static operators such as conditional belief, infallible knowledge and defeasible knowledge.

ABSTRACT. In this paper, we investigate the belief revision problem in epistemic planning, i.e., what will be the beliefs of all agents in a multi-agent system after one agent gains the belief in some fluent formula. We expand the standard logic of belief revision to the dynamic, multi-agent setting in order to be able to assess approaches to epistemic planning. Based on the standard representation in epistemic planning of agents’ beliefs via a single Kripke model, we develop a generalization of the classical AGM belief revision postulates as a formal evaluation instrument for dynamic epistemic reasoning frameworks in which the beliefs of all agents as the result of actions are computed. We provide an example of a simple, generalized ``full-meet'' multi-agent belief revision operator and prove that it satisfies all of the generalized AGM postulates. We moreover define a generalization of the standard postulates for *iterated* revision, present an event model based belief operator, and discuss the potential issues in defining an epistemic operator on Kripke models that can satisfy these properties as well.

ABSTRACT. We consider the problem of modifying a description logic concept in light of models represented as pointed interpretations. We call this setting \emph{model change}, and eviction, which consists of only removing models; incorporation of models in a single operation. introduce a formal notion of revision and argue that it does not reduce to a simple combination of eviction (removing models) and reception (adding models), contrary to intuition. We provide positive and negative results on the compatibility of eviction and reception for $\EL_\bot$ and \ALC description logic concepts and on the compatibility of revision for \ALC concepts.

ABSTRACT. The propositional abduction problem is a well-known form of non-monotonic reasoning where we are asked to find an explanation of a given manifestation. Recently, there has been an influx of results for other problems on not only finding one solution, but asking more refined questions on the solution space as a whole. For example, we might be interested in finding two solutions that are sufficiently far from each other (diverse solutions) in the solution space. In this paper we consider a related representation question where we ask if a given set of explanations S can represent any other explanation (whether their symmetric difference is smaller than a given k). We first study this problem from classical complexity and obtain a complete classification. While we only obtain a handful of tractable cases the blowup in complexity when compared to the classical abduction problem is often smaller than what one might expect. We continue with a parameterized complexity study (with several different parameters) and obtain new tractable and hard cases. Interestingly, a full parameterized complexity classification would simultaneously need to resolve the parameterized complexity of the covering radius problem from coding theory.

ABSTRACT. Inductive Logic Programming (ILP) originated within the Logic Programming community in the Nineties as a framework for combining symbolic learning with declarative knowledge representation. Nowadays, mature ILP frameworks exist that are capable of learning complex, non-monotonic hypotheses, thus broadening both the modeling capabilities and the scope of real-world applications of ILP. This work is primarily based on the FastLAS2 framework and aims to generate simple, interpretable hypotheses to help clarify the weather bulletins issued by OSMER FVG, the Regional Meteorological Observatory of the Italian region of Friuli Venezia-Giulia. In this paper we present a pipeline which, starting from simulated meteorological raw data and from OSMER's bulletin (used as ground truth) extracts data as ASP facts and generates ILP examples. From such examples an explanatory hypothesis is then inferred via FastLAS2. Such a hypothesis (translated into natural language) explains the weather forecast issued by human experts, and in particular the rationale behind experts’ choices of specific symbols in the bulletin pictogram (the symbol-annotated meteorological map of the forecast). The proposed approach is general, not specific to any particular region, it can equally be applied to bulletins from other sources and to different regions.

ABSTRACT. Neurosymbolic (NeSy) systems integrate neural networks with logical reasoning to achieve both generalization and interpretability, but recent work has shown they are susceptible to shortcut reasoning behaviors. We propose a novel method using matrix-based differentiable logic programming to mitigate reasoning shortcuts in two phenomena: \textit{constraint satisfaction shortcuts}, where constraints are satisfied without achieving the intended task, and \textit{cognition shortcuts}, where biased data leads to semantically incorrect concept mappings despite logically sound inference. Building on recent matrix-based logic programming semantics, we introduce design elements to mitigate shortcuts, including a unified encoding of rules and constraints in a single matrix. We also establish theoretical connections to fuzzy logic t-norms and empirically compare their gradient flow properties. Through carefully designed experiments on MNIST variants, we show that one-to-one grounding of neural outputs to logical atoms significantly reduces both shortcut types compared to previous methods that rely on soft probability distributions. We then confirm that architectural choices in coupling symbolic knowledge with neural learning play a critical role in shortcut mitigation.

ABSTRACT. We model in intuitionistic implicational logic the key enabler of today’s GenerativeAI: the next-token pre- diction in autoregressive causal neural networks. In our framework, next-token prediction corresponds to modus ponens, and sequence processing be- comes constructive proof extension under the Curry–Howard correspondence. Our Prolog-based special- ized theorem provers validate fundamental properties of the neural models, among which relations between commutative vs. non-commutative sequencing and single-token vs. multi-token prediction choices. We derive a neural architecture equivalent to multiplicative RNNs that arises naturally from a proof- theoretic interpretation of next-token prediction as nested intuitionistic implication and position the model relative to transformers, state-space models and recursive LLMs. Keywords: logic-based derivation of neural architectures, intuitionistic implicational logic, token-as- operator neural models, alternatives to transformer-based foundational models.

ABSTRACT. We present the interactions with a LLM (Large Language Model) aiming at proving that sqrt(2) is not a rational number in a LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system written by Robert Stark for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of sqrt(2). Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by a LLM and fully proof-checked by LPTP.

ABSTRACT. The Single Constant Multiplication problem is a fundamental NP-hard optimization task in hardware design, which seeks to decompose a fixed constant using only additions, subtractions, and bit-shifts. Although dynamic programming methods can produce near-optimal SAT encodings for SCM, their encoding cost remains high for large constants. We propose a neuro-symbolic framework that accelerates SCM SAT encoding by identifying good rules for guiding operator selection during decomposition. Our approach employs a graph neural network model to predict promising operator types from constant decompositions, and exploits the resulting confidence scores to prune no-good choices in the symbolic search. Experimental results on unseen 17--32 bit constants demonstrate one to two orders of magnitude reductions in encoding time, over 97\% reduction in memory usage, and an order-of-magnitude decrease in branching, while preserving near-optimal encoding quality in terms of additions. These results show that learning-guided symbolic strategies can significantly improve the scalability and efficiency of SCM encoding. Our codes and data are public available at: https://github.com/Chufeng-Jiang/SCM_MLDP

ABSTRACT. Deduction and static equivalence are central knowledge problems in the formal analysis of security protocols and are known to be undecidable for general equational theories. Several decidable classes have been identified through structural restrictions, including subterm convergent theories, shallow permutative theories, contracting theories and some are implemented in tools such as ProVerif and DeepSec. We identify two recurring themes: symbol preservation, where symbols are maintained across axioms, and symbol contraction, where symbols decrease in depth or number from left to right. For symbol-preserving systems, we introduce measure-invariant (MI) and separate measure-invariant (SMI) theories, generalizing permutative classes and providing new decidable fragments for deduction and static equivalence. Depth-sensitive refinements, including depth-preserving permutative (DPP) and depth-preserving variable-permuting (DPVP) theories, are case studies to understand whether the depth of occurrences of symbols matter. For symbol-contraction systems, we define depth-decreasing (DD) and variable-preserving function-decreasing (VBFD) theories, capturing some simple relaxations of term contraction; while deduction is undecidable in general, these restrictions highlight potential decidable fragments. Overall, our results show that controlling symbol dynamics in rewrite rules provides a unifying perspective on the decidability of knowledge problems, offering conceptual clarity on what makes these problems hard for different equational theories.

ABSTRACT. In this work we prove the undecidability (and Sigma1-completeness) of several theories of semirings with fixed points. The generality of our results stems from recursion theoretic methods, namely the technique of effective inseperability. Our result applies to many theories proposed in the literature, including Conway mu-semirings, Park mu-semirings, and Chomsky algebras.

ABSTRACT. We provide new proofs of two important theorems for proving termination of term rewrite systems (TRSs), including a full formalization in Isabelle/HOL. We first consider Dershowitz' theorem that termination starting from arbitrary terms is equivalent to termination starting from all right-hand sides of the set of right-forward closures, provided that the TRS is right-linear or orthogonal. Our new proof deviates from the original one in that no reorderings of steps in infinite derivations are required, making it more precise in its argumentation. It also subsumes a later result that one can weaken orthogonality to locally confluent overlay TRSs. The second theorem is about matrix interpretations. These were introduced by Hofbauer and Waldmann for proving termination of string rewrite systems (SRSs), internally using the concept of a core. Subsequently, Endrullis, Waldmann and Zantema developed matrix interpretations for TRSs without using the idea of a core. Whereas matrix interpretations for TRSs have already been formalized several times, so far this was not the case for core SRS matrix interpretations. We not only provide such a formalization, but also extend core SRS matrix interpretations to TRSs. These new core matrix interpretations for TRSs generalize previous approaches.

ABSTRACT. The determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-constructive arguments. Our contribution in this work is twofold: first, we present the first complexity bound for this problem, showing it is primitive recursive. Second, our techniques introduce a versatile framework to analyse runs of weighted automata in a constructive manner. In particular, this significantly simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.

ABSTRACT. In this paper we introduce the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata (over a field) by allowing the transition weights to be rational functions of the tree size. Whereas the class of generating functions of weighted tree automata coincides with the class of algebraic power series, our main result is that that the class of generating functions of differential tree automata coincides with the class of differentially algebraic power series. As a corollary, we obtain a decision procedure for determining equivalence of differential tree automata. In the course of proving our main result we identify a class of recurrences that characterises the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. We further identify a natural syntactic subset of differential tree automata whose generating functions are given by rational dynamical systems, that is, as components of the solution of a system of differential equations $\boldsymbol{y}' = F(\boldsymbol y)$, where $F$ is a vector of rational functions that is defined at $\boldsymbol y(0)$. We further show that this class of power series can be characterised in terms of the classical notion of weighted tree automata by using a labelled generating function on trees.

ABSTRACT. Hofmann (1999) introduced the functional programming language LFPL to characterize the functions computable in polynomial time using an affine type system. LFPL enables a natural programming style, including nested recursion, and has inspired the development of type systems for automatic cost analysis, linear dependent type theories, and efficient memory management in functional programming languages. Despite its prominence, there does not exist a self-contained presentation, let alone a full mechanization, of LFPL and its core metatheory. This article presents a modern account and mechanization of LFPL and its metatheory with the goal of being self-contained and accessible while streamlining the strongest-known soundness and completeness results. The soundness proof works with the language LFPL+, which extends LFPL with additional language features. The proof is novel, adapting a technique by Aehlig and Schwichtenberg (2002) to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics. The completeness proof shows that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists. It has the same structure as the original proof by Hofmann (2002) but greatly simplifies the core argument with a novel stack-like data structure that is implemented with first-class functions and lists. The mechanization includes the full soundness and completeness proofs, and serves as one of the first case studies of mechanized metatheory in the recently developed proof assistant Istari.

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 Layered Modal ML (LMML), \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 LMML, 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. Hard industrial planning, timetabling or scheduling instances for SAT typically have many high-level constraints, each generating a possibly large number of clauses. When a given instance is reported unsatisfiable by the SAT solver, the user normally needs an \emph{explanation} why: a (hopefully small) subset of the constraints causing it. Our industrial applications require \emph{fast} explanations, preferrably faster than the orginal SAT run. For this, we leverage the original solver's work through its unsatisfiability proof. Previous such group-oriented MUS tools had quite different intended uses and were either based on substantial internal modifications of (now somewhat outdated) SAT solvers or on assumption-based incremental solvers that frequently need very long runtimes on our instances, even for 1-minute original SAT runs. Here we introduce WhyUnsat, and explain why it is fast and robust. In WhyUnsat one can always plug in the best current SAT solver and proof trimmer, without any modification, by simply indicating the path to their executables. WhyUnsat is also fast because it exploits, via MPI, the -progessively cheaper- shared-memory and distributed computing resources. Another requirement we had is that the tool should be anytime and user-friendly; indeed, it quickly shows a human-readable presentation of (an over-approximation of) the explanation, which is then progressively reduced until minimality (unless interrupted by the user). Finally, and not less importantly, here we explain how and why the WhyUnsat approach is now also directly applicable, at no impementation cost, to IPASIR-UP-based constraint programming by Lazy Clause Generation (LCG) as well as to SAT Modulo Theories (SMT).

ABSTRACT. We address the problem of attributing responsibility to individual clauses for the unsatisfiability of a propositional formula. Recent work adopted the Shapley-Shubik power index, proposing a probabilistic approximation algorithm. However, despite polynomial, the required number of SAT solver calls becomes impractical when the input formula is not easy to solve. In such cases, it is often possible to enumerate a partial set of minimal unsatisfiable subsets (MUSes) and minimal correction subsets (MCSes). In this paper, we demonstrate that these subsets can be leveraged to efficiently bound and approximate the Shapley-Shubik index. We introduce a framework that exploits the structural information provided by the available sets to derive useful attribution explanations.

ABSTRACT. Many communities within Combinatorial Optimization (CO) maintain benchmark sets in heterogeneous formats, often tied to specific competitions and solver technologies. Whilst this diversity is of practical and historical importance, it also creates barriers to use and compare methods from different communities. Inspired by the more unified software ecosystem from the ML community, we propose a programmatic abstraction for CO benchmark sets. A unified programmatic interface for downloading, reading and converting datasets across formats. This includes solver-oriented benchmarks such as XCSP3, MIPLib, PB, MaxSATEval, SAT and application-oriented benchmarks such as Nurse rostering, PSPLib (RCSP), and JSPlib. To enable cross-formalism conversions, we provide loaders that bring these dataset instances into CPMpy, a modelling library for constraint programming. CPMpy provides a transformation stack; an extensive set of rewrite operations such as constraint decomposition, linearization, and Boolean encodings, that allow transforming between different constraint formalisms. Based on this, we implement file writers to multiple solver-oriented formats, including FlatZinc, LP file format (ILP), OPB, and DIMACS (W)CNF ((Max)SAT). We demonstrate that this unified abstraction facilitates cross-community access to benchmarks and systematic comparisons of solvers across paradigms.

ABSTRACT. Solvers for NP-hard problems from areas such as automated reasoning or optimisation are complex systems in which many different components interact. The performance of these solvers is the result of an intricate interplay between implementation details, algorithmic concepts and heuristics. This, alongside the complexity of the problem instances to be solved, makes it challenging to assess the effect of a single idea on the overall performance of a given solver. It is therefore not only crucial, but also challenging to evaluate the performance impact of new ideas. Existing reliable evaluation methods require large sets of diverse benchmark instances and considerable amounts of computing resources. This makes empirical evaluation a bottleneck for solver development, as it is time-consuming and energy-intensive, often requiring several CPU years of computation to evaluate the impact of a single idea. In recent years, this bottleneck has led to the development of data-driven approaches that can dynamically select a smaller number of instances that provide sufficient statistical evidence to evaluate the relative performance of a given set of solvers. However, these methods are typically not easily accessible. In this work, we present a tool that implements these methods and makes them readily accessible to solver developers, thus enabling them to obtain swifter feedback on their ideas.

ABSTRACT. Industrial automated reasoning demands the rapid, repeated extraction of insights from complex formulas. Knowledge compilation into the Deterministic Decomposable Negation Normal Form (d-DNNF) addresses this by reducing natively intractable tasks to polynomial-time operations. We present decdnnf_rs, a performant framework for executing advanced reasoning queries directly on d-DNNF circuits. The library provides unified support for Satisfiability, Model Counting, Disjoint Model Enumeration, Direct Access, and Uniform Sampling. Crucially, decdnnf_rs handles dynamic contexts through implicit conditioning via weight propagation, avoiding the computational overhead of explicit graph modification. It also incorporates dynamic smoothness tracking to maintain a compact memory footprint. Bridging theoretical advancements with robust software engineering, decdnnf_rs offers an optimized toolset for exact and stochastic reasoning.

ABSTRACT. The Traveling Salesperson Problem (TSP) is a very well-known problem in computer science. Many real-world instances belong to the class of Euclidean TSP, in which the nodes to be visited lie on the Euclidean plane, and additional information is available with respect to the generic TSP, i.e. the coordinates of the nodes to be visited are known. In previous publications, we showed that the additional available information can be exploited to speedup the search, both in Constraint Logic Programming (CLP) and in Answer Set Programming (ASP). Constraint Answer Set Programming is a framework that joins CLP and ASP, and it aims at combining the features of both languages. In this article, we address the (Euclidean) TSP in Constraint Answer Set Programming, and more specifically in the clingo[DL] language and solver. We propose new encodings for the TSP in clingo[DL]; the new encodings are applicable to the general TSP (also to instances which are not Euclidean) and show a speedup of several orders of magnitude with respect to previous encodings. A further speedup can be obtained in Euclidean instances by exploiting geometric reasoning.

ABSTRACT. From the moment of their inception, languages for relational data have been described as sublanguages embedded in a host programming language. Rel is a new relational language whose key design goal is to go beyond this paradigm with features that allow for programming in the large, making it possible to fully describe end to end application semantics. The core of Rel is Datalog with first-order queries in rule bodies; this is the principal relevance to ICLP. It is then extended with features that let it model the entire application semantics: variables that range over tuples and sets of tuples; abstraction, and application. With the new approach, we can model the semantics of entire enterprise applications relationally, which helps significantly reduce architecture complexity and avoid the well-known impedance mismatch problem. This paradigm shift is enabled by 50 years of database research, making it possible to revisit the sublanguage/host language paradigm, starting from the fundamental principles. The paper presents the main features of Rel: those that give it the power to express traditional query language operations and those that are designed to grow the language and allow programming in the large. The original paper on Rel appeared in SIGMOD 2025 under the title "Rel: A Programming Language for Relational Data". After receiving a SIGMOD Research Highlights Award, a shorter version under the current title was published in SIGMOD Record. For convenience we include this shorter version here. The URLs for the conference and the SIGMOD Record papers (both open access) are below: - https://dl.acm.org/doi/10.1145/3722212.3724450 - https://sigmodrecord.org/2026/04/01/relational-programming-in-rel Viktor Leis and Thomas Neumann wrote a short technical perspective on the paper: https://sigmodrecord.org/2026/04/01/technical-perspective-rel.

ABSTRACT. The extended abstract, for the recently published research track, introduces a novel approach to the Contrast Sequential Pattern Mining (CSPM) task, which is based on Answer Set Programming (ASP). The MASS-CSP framework provides a concise and versatile ASP encoding that addresses the basic CSPM task as well as several advanced extensions. The framework is implemented in two distinct phases: first, extracting frequent sequential patterns, and second, verifying if they satisfy specified constraints, such as the minimum support and contrast rate thresholds. The research demonstrates the power of ASP modelling features such as choice rules for pattern generation, integrity constraints for filtering, and aggregates for calculating the support of patterns. Furthermore, the framework addresses the practical challenges of Logic Programming, including the grounding phase, which can lead to memory explosion if not carefully managed. The practical utility of the framework is further validated by successfully identifying attack patterns in 4G-LTE cellular network logs, proving its effectiveness for anomaly detection and intrusion prevention.

ABSTRACT. Automating the translation of natural-language specifications into logic programs is a challenging task that affects neurosymbolic engineering. We present ASP-Bench, a benchmark comprising 128 natural language problem instances, 64 base problems with easy and hard variants. It evaluates systems that translate natural-language problems into Answer Set Programs (ASPs), a prominent form of logic programming. It provides systematic coverage of ASP features, including choice rules, aggregates, and optimization. Each problem includes reference validators that check whether solutions satisfy the problem specification. We characterize problems along seven largely independent reasoning aspects (optimization, temporal reasoning, default logic, resource allocation, recursion, spatial reasoning, and quantitative complexity), providing a multidimensional view of modeling difficulty. We test the benchmark using an agentic approach based on the ReAct (Reason and Act) framework, which achieves full saturation, demonstrating that feedback-driven iterative refinement with solver feedback provides a reliable and robust approach for modeling natural language in ASP. Our analysis across multiple agent runs enables us to gain insights into what determines a problem’s modeling hardness. -- This paper is to appear in the Proceedings of the 2nd International Workshop on Neuro-Symbolic Software Engineering (NSE 2026), affiliated with ICSE 2026. https://conf.researchr.org/home/icse-2026/nse-2026

ABSTRACT. Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunction and infinite disjunction. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr's theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.

ABSTRACT. DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.