ABSTRACT. In type theory, an oracle may be specified abstractly by a predicate whose domain is the type of queries asked of the oracle, and whose proofs are the oracle answers. Such a specification induces an oracle modality that captures a computational intuition about oracles: at each step of reasoning we either know the result, or we ask the oracle a query and proceed upon receiving an answer. We characterize an oracle modality as the least one forcing the given predicate. We establish an adjoint retraction between modalities and propositional containers, from which it follows that every modality is an oracle modality. The left adjoint maps sums to suprema, which makes suprema of modalities easy to compute when they are given in terms of oracle modalities. We also study sheaves for oracle modalities. We describe sheafification in terms of a quotient-inductive type of computation trees, and describe sheaves as algebras for the corresponding monad. We also introduce equifoliate trees, an intensional notion of oracle computation given by a (non-propositional) container. Equifoliate trees descend to sheaves, and lift from sheaves in case the container is projective. As an application, we give a concrete description of all Lawvere-Tierney topologies in a realizability topos, closely related to a game-theoretic characterization by Takayuki Kihara.

ABSTRACT. Extensional ESO is a fragment of existential second-order logic (ESO) that captures the following family of problems. Given a fixed ESO sentence $\Psi$ and an input structure $\mathbb A$ the task is to decide whether there is an \emph{extension} $\mathbb B$ of $\mathbb A$ that satisfies the first-order part of $\Psi$, i.e., a structure ${\mathbb B}$ such that $R^{\mathbb A}\subseteq R^{\mathbb B}$ for every existentially quantified predicate $R$ of $\Psi$, and $R^{\mathbb A} = R^{\mathbb B}$ for every non-quantified predicate $R$ of $\Psi$. In particular, extensional ESO describes all pre-coloured finite-domain constraint satisfaction problems (CSPs). In this paper we study the computational power of extensional ESO; we ask, \emph{for which problems in NP is there a polynomial-time equivalent problem in extensional ESO?} One of our main results states that extensional ESO has the same computational power as \emph{hereditary first-order logic}. We also characterize the computational power of the fragment of extensional ESO with monotone universal first-order part in terms of finitely bounded CSPs. These results suggest a rich computational power of this logic, and we conjecture that extensional ESO captures NP-intermediate problems. We further support this conjecture by showing that extensional ESO can express current candidate NP-intermediate problems such as Graph Isomorphism, and Monotone Dualization (up to polynomial-time equivalence). On the other hand, another main result proves that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESP (unless E=NE).

ABSTRACT. The logic MMSNP is a well-studied fragment of Existential Second- Order logic that, from a computational perspective, captures ex- actly finite-domain Constraint Satisfaction Problems (CSPs) modulo polynomial-time reductions. At the same time, MMSNP contains many problems that are expressible as 𝜔-categorical CSPs but not as finite-domain ones. We initiate the study of Promise MMSNP (PMMSNP), a promise analogue of MMSNP. We show that every PMMSNP problem is poly- time equivalent to a (finite-domain) Promise CSP (PCSP), thereby extending the classical MMSNP-CSP correspondence to the promise setting. We then investigate the complexity of PMMSNPs aris- ing from forbidding monochromatic cliques, a class encompassing promise graph colouring problems. For this class, we obtain a full complexity classification conditional on the Rich 2-to-1 Conjecture, a recently proposed perfect-completeness surrogate of the Unique Games Conjecture. As a key intermediate step which may be of independent interest, we prove that it is NP-hard (under the Rich 2-to-1 Conjecture) to properly colour a uniform hypergraph even if it is promised to admit a colouring satisfying certain technical conditions. This proof is an extension of the recent work of Braverman, Khot, Lifshitz and Minzer (Adv. Math. 2025). To illustrate the broad applicability of this theorem, we show that it implies most of the linearly-ordered colouring conjecture of Barto, Battistelli, and Berg (STACS ’21).

ABSTRACT. The Bodirsky-Pinsker conjecture asserts a P vs. NP-complete dichotomy for the computational complexity of Constraint Satisfaction Problems (CSPs) of first-order reducts of finitely bounded homogeneous structures. Prominently, two structures in the scope of the conjecture have log-space equivalent CSPs if they are pp-bi-interpretable, or equivalently, if their polymorphism clones are topologically isomorphic. The latter gives rise to the algebraic approach which regards structures with topologically isomorphic polymorphism clones as equivalent and seeks to identify structural reasons for hardness or tractability in topological clones. We establish that the equivalence relation of pp-bi-interpretability underlying this approach is reasonable: On the one hand, we show that it is decidable under mild conditions on the templates; this improves a theorem of Bodirsky, Pinsker and Tsankov (LICS'11) on decidability of equality of polymorphism clones. On the other hand, we show that within the much larger class of transitive $\omega$-categorical structures without algebraicity, the equivalence relation is of lowest possible complexity in terms of descriptive set theory: namely, it is smooth, i.e., Borel-reduces to equality on the real numbers. On our way to showing the first result, we establish that the model-complete core of a structure that has a finitely bounded Ramsey expansion (which might include all structures of the Bodirsky-Pinsker conjecture) is computable, thereby providing a constructive alternative to previous non-constructive proofs of its existence.

ABSTRACT. In this paper, we propose a unifying algebraic framework which allows us to connect circuit complexity classes to the properties of finite algebraic structures. Our work is inspired by branching programs and nonuniform deterministic automata introduced by Barrington, as well as by their generalization proposed by Idziak et al. In particular, we characterize language classes recognized by circuits over simple algebras and over algebras from congruence modular varieties.

ABSTRACT. Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about $(\infty,1)$-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of $\infty$-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the $\infty$-category of spaces. We complete this process by constructing the $\infty$-category of $\infty$-categories, recovering one of the main foundational results of $\infty$-category theory (straightening--unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle, the structure homomorphism principle.

ABSTRACT. In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for a Brouwer ordinal α, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that α-decidable propositions are closed under binary conjunction, and discuss for which α they are closed under binary disjunction. We prove that if each P(i) is semidecidable, then the countable meet ∀i∈ℕ.P(i) is ω²-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in cubical Agda.

ABSTRACT. Cubical type theories are designed around an abstract unit interval from which types of paths are defined; varying the operations available on this interval yields different type theories. A reversal is an involutive unary operator on the interval that swaps its two endpoints. We show that for cubical type theories with self-dual interval theories, such as the minimal theory of two endpoints or the theory of a bounded distributive lattice, the extension of the theory with a reversal that internalizes the duality is a conservative extension. The key observation is that the product of an interval and its dual is again an interval with a reversal given by swapping coordinates. Our conservativity result applies to "idealized" cubical type theories without equations for evaluating the filling operator at concrete type formers. Using the same basic observation, however, we also construct models of full cubical type theories with reversals in categories of cubical sets without reversals. In so doing, we give the first models of these theories whose homotopy theory corresponds to that of topological spaces.

ABSTRACT. We give a new syntax-independent account of finitely-presented generalized algebraic theories (GATs) as finite cell complexes in the category of categories with families (CwFs), in which GATs are constructed by successive pushouts along the CwF morphisms generically postulating a sort, an operation, or an equation. Inspired by the fat small object argument of Makkai, Rosick\'{y}, and Vok\v{r}\'{i}nek, we introduce fat GAT presentations, thereby allowing infinite presentations with non-linear dependency structure. Then, motivated by wanting our GATs to self-describe, we extend presentations to admit infinitary arities, including infinitely deep dependency chains. Finally, we verify that these generalized GATs satisfy expected semantic properties including Frey's Gabriel–Ulmer duality.

ABSTRACT. Stochastic Satisfiability Modulo Theories (SSMT) has traditionally focused on the interplay between existential and randomized quantifiers, typically relying on numerical sampling or approximations. We present a generalized SSMT framework that integrates universal quantification, lifting the formalism to a robust stochastic game-theoretic setting. By treating universal quantifiers as the adversarial infimum of satisfaction probabilities, our framework enables the exact modeling of competitive interactions under uncertainty. Our approach leverages Cylindrical Algebraic Decomposition (CAD) to derive exact symbolic probability expressions for Nonlinear Real Arithmetic (NRA) formulas, moving beyond the limitations of linear constraints and point-value estimations. Central to our contribution is a recursive quantifier elimination algorithm designed to handle variable-dependent domains and non-algebraic expressions through a variable reparameterization technique. Experimental evaluation across baseline synthetic formulas, strategic economic models, and probabilistic program verification benchmarks demonstrates that our framework consistently computes exact piecewise-polynomial solutions. By providing a level of symbolic precision and expressiveness unattainable by traditional numerical solvers, this work establishes a new baseline for exact reasoning in stochastic adversarial environments.

ABSTRACT. In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries. In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. We have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the feasibility and the effectiveness of the approach.

ABSTRACT. The theory of uninterpreted functions is a key modeling tool for systems with unknown or abstracted components. Some domains such as systems biology impose further restrictions regarding monotonicity on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand. We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.

ABSTRACT. Assumption-Based Argumentation (ABA) is a well-established formalism for modelling and reasoning over debates, with a wide range of applications. However, the high computational complexity of core reasoning tasks in ABA poses a significant challenge for its applicability. This issue is further aggravated when ABA frameworks (ABAFs) are instantiated into graph-based argumentation formalisms, such as Dung's Argumentation Frameworks (AFs) and Argumentation Frameworks with Collective Attacks (SETAFs). In knowledge representation and reasoning, a key strategy to address computational intractability is to optimise reasoning over a given knowledge base through divide-and-conquer algorithms. A paradigmatic example of this approach is splitting, where extensions of a given framework are computed incrementally, by restricting the search space to sub-frameworks only, and then combining the obtained results. This approach has been successfully applied to AFs, for which also a parametrised version has been introduced under stable semantics. However, the exponential growth produced by the instantiation might undermine the usefulness of splitting on the argument graphs induced by ABAFs. To address this issue, our work investigates the concept of splitting on the knowledge base rather than on its graph-based instantiation. Furthermore, we generalise splitting to its parametrised version for ABAFs.

ABSTRACT. Timed Argumentation Frameworks (TAFs) allow taking into account the availability of arguments and attacks in abstract argumentation. We propose a new reasoning approach for TAFs, where a standard Dung-style AF can be associated with each timepoint. We show that, although this framework is more expressive than Dung's framework, our approach does not lead to an increase in computational complexity for most reasoning problems and classical extension-based semantics.

ABSTRACT. This work proposes novel splitting techniques for argumentation formalisms that incorporate supports between defeasible elements. We base our studies on Bipolar Set-Based Argumentation Frameworks (BSAFs), which generalize argumentation frameworks with collective attacks (SETAFs), as well as Bipolar Argumentation Frameworks (BAFs), by incorporating both collective attacks and supports. Notably, BSAFs establish a crucial link to structured argumentation as they naturally capture general (potentially non-flat) assumption-based argumentation. The increase in expressiveness calls for diverse forms of splitting. We consider splits over collective attacks (thereby generalizing the recently proposed splitting techniques for SETAFs), splits over collective supports, as well as splits over both collective attacks and supports. We establish suitable splitting schemata and prove their correctness for the most common argumentation semantics.

ABSTRACT. To better understand, and analyse, natural language arguments, it is desirable to represent them as logical arguments. However, most real-world arguments are enthymemes (i.e. some of the premises and/or claims are implicit), and therefore, there is a need to identify these implicit aspects. A ramification of this is that we may then need to edit some of the explicit premises and/or claim to remove redundant aspects and/or to allow the newly identified implicit formulae to work correctly with the explicit formulae. Furthermore, we may need to edit the claim so that it correctly attacks or supports other arguments as predicted by argument mining or as required by the user. To address these requirements, we propose a logic-based framework, based on classical propositional logic, for representing enthymemes, and manipulating them through a range of logical operations. We introduce meta-level rules to manipulate arguments (e.g. to add or delete premises, to edit claims, to split an argument into two arguments, and to merge two arguments into one). In order to direct the use of meta-level rules, we also introduce gain measures. When choosing a sequence of meta-level rules to apply, we can choose those that increase gain. This meta-level reasoning framework provides some clarity on the nature of enthymemes, and on how agents might elucidate them through a transparent and incremental process.

ABSTRACT. Logical argumentation uses calculi to generate arguments and counter-arguments to capture defeasible reasoning. In this paper, we introduce modular proof-search procedures for a large class of such argument calculi developed to capture two core forms of defeasible reasoning: normative reasoning, formalized via input/output logics, and doxastic reasoning, formalized via normal default logic. Our approach relies on modular, rule-based, and terminating decomposition trees via step-by-step decomposition of norms and defaults. When successful, a terminated decomposition trees certifies derivability of a given argument in its corresponding calculus, including arguments for obligations and beliefs, as well as defeating arguments concluding inapplicability of norms and defaults. We show how rule-based decomposition of norms and defaults is used to determine nonmonotonic inference for credulous reasoning with maximal consistent sets of norms and defaults and stable extensions of arguments in formal argumentation.

ABSTRACT. We study the problem of fitting a description logic (DL) ontology to a given set of positive and negative examples that take the form of an ABox and a Boolean query. While previous work has investigated this problem for the expressive DLs ALC and ALCI, we here focus on the Horn DLs EL and ELI, as well as their extensions with the bottom concept. As the query language, we consider atomic queries (AQs), rooted conjunctive queries (rooted CQs), and unions thereof (rooted UCQs). We provide characterization of the existence of a fitting ontology based on simulations, use them to develop decision procedures, and clarify the exact computational complexity. For AQs, the problem is in PTime for both EL and ELI. For rooted CQs and UCQ, it is Sigma_P^2-complete for EL and ExpTime-complete for ELI. Adding the bottom concept does not change any of these complexities. Interestingly, moving from ALC and ALCI to EL and ELI introduces additional technical challenges rather than simplifying the matter.

ABSTRACT. We present a probably approximately correct algorithm for learning the terminological part of a description-logic knowledge base via subsumption queries. The axioms we learn are concept inclusions between conjunctions of concepts from a specified set of concept descriptions. By varying the distribution of queries posed to the oracle, we adapt the algorithm to improve the recall when using the resulting TBox for ontology-mediated query answering. Experimental evaluation on OWL 2 EL ontologies suggests that our approach helps significantly improve recall while maintaining a high precision of query answering.

ABSTRACT. Expressive power is a recurring theme in Knowledge Representation and Reasoning and has recently become a bridge connecting neural and symbolic representations. Notably, in the domain of graph representation learning, prior work has either established lower bounds on the logical expressive power of graph neural networks (GNNs) or exact correspondences between GNNs and non-standard logics. In this paper, we propose GNN architectures that correspond precisely to prominent fragments of first-order logic (FO), including various modal logics as well as more expressive two-variable fragments. Our results provide a unifying framework for understanding the logical expressiveness of GNNs within FO.

ABSTRACT. Light-weight description logics like EL have been successfully used to represent the terminological knowledge of many application domains. Yet, identifying the characteristics of instances often requires sub-symbolic approaches. We introduce a neuro-symbolic extension of EL which allows for (neural) perception and classification of properties, accompanied by formal (symbolic) reasoning based on these perceptions. Through a prototypical implementation, based on a reduction to logic programming, we show that inferences and learning are effectively achievable.

ABSTRACT. Knowledge base (KB) embeddings aim at combining the capability of classical knowledge graph embeddings to generalize the information present in facts, the ABox, with conceptual knowledge represented in an ontology language, the TBox. Several authors have recently explored the idea of mapping concepts to convex regions in a vector space. This is useful to represent hierarchies, typically present in TBoxes, since more general concepts can be mapped to larger regions, containing those regions associated with more specific concepts. However, the power of convexity is rarely leveraged during the actual learning tasks. Here, we introduce BoxLitE, a KB embedding model for DL-Lite that allows for convex optimization. We show that for any satisfiable DL-Lite KB, there is a BoxLitE embedding that is a weakly faithful model. As a proof of concept, we show how to formulate the KB embedding task as a convex optimization problem and how to obtain embeddings with such desirable faithfulness properties.

ABSTRACT. A fundamental challenge in neurosymbolic systems is applying continuous gradient-based optimization to discrete logical domains. While fuzzy relaxations provide differentiability, they often lack a formal structural alignment with classical logic. In this work, we show that Gödel semantics addresses this limitation through a homomorphism that maps its continuous interpretations to Boolean ones, allowing discrete variables to be encoded while maintaining full differentiability. Building on this foundation, we show that gradient-based optimization on Gödel logic instantiates a discrete local search for Boolean satisfiability. Our formal analysis proves that each optimization step identifies and modifies a single variable within an unsatisfied clause, precisely mimicking the steps of a discrete solver. We identify local optima as the primary limitation of such dynamics and introduce the Gödel Trick, a stochastic reparameterization technique designed to improve the exploration of the solution space. We further show a formal connection between this approach, probabilistic inference, and the Gumbel-Max trick. Experimental results on SAT benchmarks and the Visual Sudoku task validate our theoretical findings, demonstrating that our approach effectively navigates complex combinatorial landscapes and provides a solid foundation for differentiable discrete search.

ABSTRACT. Neurosymbolic integration (NeSy) blends neural‐network learning with symbolic reasoning. The field can be split between methods injecting hand-crafted rules into neural models, and methods inducing symbolic rules from data. We introduce Logic of Hypotheses (LoH), a novel language that unifies these strands, enabling the flexible integration of data-driven rule learning with symbolic priors and expert knowledge. LoH extends propositional logic syntax with a choice operator, which has learnable parameters and selects a subformula from a pool of options. Using fuzzy logic, formulas in LoH can be directly compiled into a differentiable computational graph, so the optimal choices can be learned via backpropagation. This framework subsumes some existing NeSy models, while adding the possibility of arbitrary degrees of knowledge specification. Moreover, the use of Gödel fuzzy logic and the recently developed Gödel trick yields models that can be discretized to hard Boolean-valued functions without any loss in performance. We provide experimental analysis on such models, showing strong results on tabular data and on two NeSy tasks with a perceptual component.

ABSTRACT. Neurosymbolic systems can satisfy logical constraints during learning without achieving the intended concept-label correspondence; this is a problem known as reasoning shortcuts. We formalize reasoning shortcuts as a constraint satisfaction problem and investigate under which conditions concept mappings are uniquely determined by the constraints. We prove that a discrimination property (requiring that no valid concept mapping can be transformed into another valid mapping by swapping two concept values) is necessary for shortcut-freeness under bijective mappings, but demonstrate via a counterexample that it is insufficient even when the constraint graph is connected. We develop an ASP-based algorithm that verifies whether a given constraint set uniquely determines the intended concept mapping, with proven soundness and completeness. When shortcuts are detected, a greedy repair algorithm eliminates them by augmenting the constraint set, converging in at most $k$ iterations, where $k$ is the number of alternative valid mappings. We further provide a complexity classification: deciding shortcut-freeness is coNP-complete, counting shortcuts is \#P-complete, and finding minimal repairs is NP-hard. We also establish sample complexity bounds showing that a logarithmic number of label queries suffices for disambiguation in favorable cases, while querying all ambiguous positions suffices in the worst case. Experiments across eight benchmark domains validate our approach.

ABSTRACT. The use of deep learning to solve fundamental AI problems such as Boolean Satisfiability (SAT) has been explored recently to develop robust and scalable reasoning systems. This work advances such neural-based reasoning approaches by developing a new Graph Neural Network (GNN) to differentiably solve (weighted) Maximum Satisfiability (MaxSAT). To this end, we propose SAT-based Graph Attention Networks (SGATs) as novel GNNs that are built on t-norm based attention and message passing mechanisms, and structurally designed to approximate greedy distributed local search. To demonstrate the effectiveness of our model, we develop a local search solver that uses SGATs to continuously solve any given MaxSAT problem. Experiments on (weighted) MaxSAT benchmark datasets demonstrate that SGATs significantly outperform existing neural-based architectures, and achieve state-of-the-art performance among continuous approaches, highlighting the strength of the proposed model.

ABSTRACT. In real-world scenarios, reinforcement learning (RL) agents must not only maximize reward but also behave safely, including during training. This has led to growing interest in Safe RL, where the objective is to learn an optimal policy among those satisfying given safety constraints. Most existing approaches focus on constraints expressed either as expected costs or as avoidance properties. However, safety in dynamical systems is often expressed using rich temporal languages, such as Probabilistic Computation Tree Logic (PCTL). In this paper, we address the Safe RL problem under constraints expressed in CPCTL, a fragment of PCTL that generalizes avoidance constraints and enables the specification of complex, nested behaviours. To this end, we leverage Shielding, a technique that restricts the agent’s actions during both training and deployment to enforce safety over an infinite horizon. We first introduce a general framework based on an augmentation method and provide its theoretical foundations. Building on this framework, we propose an algorithm that is provably safe at all times, including during training, while remaining optimal among all safe policies. Finally, we present an experimental evaluation demonstrating the effectiveness of our approach.

ABSTRACT. Prolog is a well-known declarative programming language commonly used in introductory courses on logic and reasoning. However, many students find Prolog challenging because it lacks the familiar debugging mechanisms found in imperative languages. In large classes, this difficulty is exacerbated by the challenge of providing timely and personalized feedback to students. In this work, we introduce ProDebug, the first tool to combine Large Language Models (LLMs) with spectrum-based and mutation-based techniques for automated debugging of Prolog assignments. ProDebug automatically identifies faults and proposes bug repairs for student Git submissions. Faults are detected using three approaches—spectrum-based, mutation-based, and LLM reasoning—while repairs are generated using mutation-based techniques and LLMs. Our evaluation on 1499 buggy student submissions from a bachelor's level programming class demonstrates the potential of automated, LLM-augmented feedback systems to scale support for declarative programming education.

ABSTRACT. Logic rules allow analysis of complex relationships to be expressed easily, especially for transitive relations in critical applications. However, understanding and predicting the efficiency of different inference methods remain challenging, even for simplest rules given different kinds of input data. This paper analyzes the efficiency of all three types of well-known inference methods---query-driven, ground-and-solve, and fact-driven---along with their respective optimizations, and compares with optimal complexities for the first time, for analyzing transitive graph relations. We also experiment with rule systems widely considered to have the best performance. We analyze all well-known rule variants and widely varying input graphs. The results include precisely calculated optimal time complexities; comparative analysis across different inference methods, rule variants, and graph types; confirmation with performance experiments; as well as discovery of a performance bug.

ABSTRACT. Logica is an open-source logic programming language that compiles to SQL and runs on platforms including DuckDB, SQLite, PostgreSQL, and BigQuery. Unlike classic Datalog, Logica permits free combination of recursion and aggregation, enabling concise formulations of algorithms from shortest paths to PageRank. This expressiveness introduces fundamental semantic challenges: aggregate predicates are updated by replacement rather than accumulation, evaluation is sensitive to rule scheduling, and programs may converge to meaningful results without ever reaching a fixpoint, placing them outside the scope of traditional fixpoint semantics. We address these challenges with \emph{Defendant--Opponent (DO) semantics}, a stabilization-based framework for nonmonotonic logic programs. Program evaluation is modeled as a rewrite system over derivation states. A ground atom is true if, from every reachable state, there exists a continuation after which the atom persists in all further derivations. This notion admits two equivalent characterizations: (1)~game-theoretically, truth is what a Defendant can defend against any Opponent in a three-turn derivation game; and (2)~modally, a formula~$t$ is a theorem precisely when the condition $\bdb\,t$ holds in the derivation graph viewed as a Kripke structure. We show that DO semantics coincides with classic least fixpoint semantics for positive Datalog programs and is compatible with both the Well-Founded Semantics (the two never disagree on definite answers) and the Stable Model Semantics (every stable model is a DO interpretation). For programs that converge without reaching a fixpoint, we introduce $\omega$-limit interpretations, giving rigorous meaning to iterative computations such as PageRank. DO semantics thus offers a coherent framework that complements existing logic programming semantics while supporting recursive aggregation.

ABSTRACT. Distributed applications increasingly support local-first collaboration over shared data, allowing multiple users to perform updates concurrently without global coordination. Such collaboration requires careful design to capture the intended semantics of the concurrent interactions. We introduce a declarative framework for specifying and reasoning about the semantics of conflict-free replicated data types (CRDTs) and CRDT-based applications in Datalog. The framework models CRDT semantics as executable logic programs over operation contexts, making concurrency explicit and compositional, and thus amenable to automated analysis. As one application, we use property-based testing to compare implementations. To the best of our knowledge, this is the first work to systematically use Datalog as a foundation for prototyping and analyzing complex CRDTs and their compositions. We evaluate our methodology using a collaborative graph data editing case study and report experimentation results assessing correctness validation and scalability with an increasing number of operations and replicas.

ABSTRACT. To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity. An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.

ABSTRACT. The axiom of choice (AC) states that every total relation contains a function. It enjoys a pivotal role in both classical and constructive dialects of mathematics. In the former, it is seen as a useful closure property invoked especially in set-theoretic contexts, in the latter it is seen either as a tautology, following from a constructive reading of totality proofs, or as a taboo, as by an extensional reading of totality proofs it enforces full classical logic. It has therefore been debated how much of AC should be accepted in constructive foundations and authors like Richman argued for ``Constructive mathematics without choice'' where even countable choice, not immediately jeopardising constructive reasoning, is avoided. With this paper, we propose a continuation of Richman's programme of more radical extent and systematically study constructive foundations absent of countable, unique, or quantifier-free choice principles as well as the spurious fragments of (the actual) AC in form of extensionality principles:``Constructive mathematics without \textit{any} choice'' We argue that such a minimalistic setting is advantageous, for instance for studies in constructive reverse mathematics and synthetic computability theory. Apart from these programmatic considerations and a careful encyclopedia of choice principles, we revisit and refine several results from the literature: We show that already the partition principle (a consequence of AC of unknown strength) implies the excluded middle, that already decidable equality of propositions implies proof irrelevance, and that function inversion principles such as the Cantor-Bernstein theorem not only rely on the excluded middle but also on unique choice. To the best of our knowledge, the latter is the first reverse mathematics result regarding the full axiom of unique choice, enabled by our minimal setting. Implementing such a minimalistic foundation, the proofs of all our results have been mechanised with the Rocq prover.

ABSTRACT. The correctness of type-checking implementations for proof assistants based on dependent type theory relies on metatheoretical properties that ensure the decidability of typing, some of which require substantial logical strength. Recent mechanizations of such algorithms have highlighted the importance of separating the algorithmic components of the proof---often intricate but requiring relatively low logical strength---from the logical components, which depend on stronger metatheoretical properties, such as normalization or the injectivity of type constructors. In this work, we revisit the logical relations technique and show how it can be used to derive these metatheoretical properties in a direct and uniform way for a core dependent type theory featuring Pi-types, nat, empty and a universe. Our presentation yields a compact and conceptually simplified argument that isolates the logically strong reasoning from the algorithmic core. We argue that this approach scales smoothly to richer type theories, and demonstrate this by extending our construction to Exceptional Type Theory (ExcTT), obtaining the first mechanized canonicity proof for this theory.

ABSTRACT. We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP is included P/poly. The reduction also holds for Craig interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or Goedel-Loeb logic GL we obtain the following dichotomy: tabular logics have "propositionally sized" interpolants while for non-tabular logics an unconditional exponential lower bound holds.

ABSTRACT. Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig Interpolation Property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in quadruple exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.

ABSTRACT. We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is $P^{NP[O(log^2 n)]}$-complete in combined complexity. Our result implies $P^{NP[O(log^2 n)]}$-completeness for both UNTC and UNFO^{reg}, which were left open in previous works.

ABSTRACT. We study the Guarded Fragment of first-order logic over models that interpret a family of distinguished binary predicates $E_1,E_2,\dots$ as nested equivalence relations, that is, such that $E_{k+1}$ is coarser than $E_k$ for all $k \geq 1$. We show that the equality-free Guarded Fragment with nested equivalence relations retains the finite model property and that its satisfiability problem is decidable, albeit of non-elementary complexity. When the number of distinguished predicates is fixed to~$K$, the complexity becomes $(K{+}2)$-\ExpTime{}-complete. In contrast, we show that decidability is lost as soon as the nesting condition is dropped or equality is admitted.

ABSTRACT. There have recently been several developments in synthetic mathematics, using extensions of dependent type theory with univalence: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. The goal of this paper is to provide a foundation of constructive higher sheaf models of type theory in a constructive meta theory, and in particular, to build constructive models of these formal systems. The main technical tools are the use of internal language for simplifying proofs of intermediate lemmas and the notion of descent data operations, which already played an important role in models of directed univalence. Even classically, we think this work can be interesting, since these models are developed in a proof theoretically weak meta theory (in particular it is predicative).

ABSTRACT. Under the homotopy hypothesis, higher dimensional groups are defined as pointed homotopy types whose homotopy groups vanish outside a certain range. In particular, a 2-group is a pointed connected homotopy 2-type. Classically, 2-groups have two equivalent algebraic descriptions: one in terms of weak monoidal categories and the other in terms of group cohomology. We present these two classifications of pointed connected 2-types in homotopy type theory, thereby providing internal, constructive counterparts to the traditional classifications of 2-groups. Our first classification (in terms of monoidal categories) takes the form of a bicategorical equivalence, while our second is a type equivalence that extends to n-groups for all n >= 2. We have mechanized our results in Agda.

ABSTRACT. In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Due to their good categorical properties, CW complexes have become the main object of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject -- perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes. In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result is a theorem (the `Hurewicz approximation theorem') which shows that a classical definition of $n$-connected CW complexes agrees with the, in HoTT, usual definition of $n$-connected types -- a theorem which is far from obvious from a constructive point of view. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.

ABSTRACT. Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear to be almost completely random---an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1953, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT)---an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented -- and constructively so. Prior to this proof, HoTT had only had been used to compute low-dimensional homotopy groups of spheres. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion's proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavor of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.

ABSTRACT. We explore the use of answer set programming (ASP) and its extension with quantifiers, ASP(Q), for inconsistency-tolerant querying of prioritized data, where a priority relation between conflicting facts is exploited to define three notions of optimal repairs (Pareto-, globally- and completion-optimal). We consider the variants of three well-known semantics (AR, brave and IAR) that use these optimal repairs, 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, optimizations, and encodings.

ABSTRACT. Answer Set Programming (ASP) is a mature and widely used framework for modeling and solving problems in AI, knowledge representation and reasoning, and combinatorial search. Counting answer sets is of growing importance for analyzing search spaces, navigating ASP programs, and enabling probabilistic reasoning. While Truszczynski established a complete hierarchy for the computational complexity of ASP decision and reasoning problems (skeptical and credulous), a corresponding systematic treatment of counting problems has been missing so far. We close this gap by providing an almost complete characterisation of the counting complexity landscape for ASP. A remaining gap arises between Krom and Horn programs, caused by the minimality of disjunctions in Krom rule heads for guessing. To address this issue, we replace disjunctions with choice rules and introduce a controlled fragment in which choices are allowed and every rule is simultaneously Horn and Krom (Choice-Horn-Krom). We show that this fragment does not admit an polynomial-time approximation scheme (FPRAS) under standard complexity-theoretic assumptions. However, we prove that counting answer sets of an arbitrary ASP program can already be done by counting answer sets of two Choice-Horn-Krom programs. This result demonstrates the expressive power of ASP and yields a conceptually simpler alternative to Valiant's classical reduction from #SAT to #Krom-SAT, which a very well-known result in propositional logic.

ABSTRACT. The ASP(Q) language extends Answer Set Programming (ASP) with Quantifiers that operate over answer sets. Thus, ASP(Q) facilitates a more natural encoding of problems whose complexity exceeds $NP$ within the ASP framework. In this paper we focus on ASP(Q) programs with two quantifiers, i.e., 2-ASP(Q) programs, which can be used to model problems in the second level of the Polynomial Hierarchy. In particular, we propose an approach for evaluating 2-ASP(Q) programs that is inspired by Counterexample Guided Abstraction Refinement (CEGAR). Unlike existing state-of-the-art ASP(Q) solvers, which are typically based on QBF solvers, our new approach leverages ASP solvers, and suffers no overhead due to the effects of translating ASP(Q) in QBF. Experimental results demonstrate that our technique consistently outperforms state-of-the-art ASP(Q) solvers, across benchmark problems located at the second level of the polynomial hierarchy.

ABSTRACT. In this paper, we develop a novel logic-based approach to detecting high-level temporally extended events from timestamped data and background knowledge. Our framework employs logical rules to capture existence and termination conditions for simple temporal events and to combine these into meta-events. In the medical domain, for example, disease episodes and therapies are inferred from timestamped clinical observations, such as diagnoses and drug administrations stored in patient records, and can be further combined into higher-level disease events. As some incorrect events might be inferred, we use constraints to identify incompatible combinations of events and propose a repair mechanism to select preferred consistent sets of events. While reasoning in the full framework is intractable, we identify relevant restrictions that ensure polynomial-time data complexity. Our prototype system implements core components of the approach using answer set programming. An evaluation on a lung cancer use case supports the interest of the approach, both in terms of computational feasibility and positive alignment of our results with medical expert opinions. While strongly motivated by the needs of the healthcare domain, our framework is purposely generic, enabling its reuse in other application areas.

ABSTRACT. Answer Set Programming (ASP) is a declarative formalism widely used in knowledge representation and reasoning for modeling and solving combinatorial problems, yet current Large Language Models (LLMs) often struggle to generate correct programs from natural language specifications. This difficulty stems both from the limited presence of ASP in training corpora and from the strict syntactic and semantic constraints imposed by stable model semantics. We introduce ALM–ASP (Agentic Loop for Modeling in ASP), a multi-agent architecture for automatic ASP modeling grounded in a functional model of language agents equipped with tools and persistent state. ALM–ASP instantiates this model via two interacting agents: a Modeler, which incrementally constructs candidate ASP programs, and a Validator, which assesses their alignment with the original specification and provides feedback for refinement. The agents interact through a shared ASP execution environment backed by the CLINGO engine, yielding an iterative construct–validate loop. An empirical evaluation on a challenging subset of CP–Bench and on problems from recent LP/CP Programming Contests shows that ALM–ASP significantly improves both syntactic validity and end-to-end correctness over general-purpose LLM baselines, and also achieves improved instance coverage compared to the closest agentic alternative, CP–Agent.

ABSTRACT. Model counting (#SAT) is a fundamental yet #P-complete problem central to probabilistic reasoning. In this work, we address incremental model counting, where sequences of structurally similar formulas must be counted. We propose an approach that amortizes computation via a persistent caching mechanism, retaining component data across solver calls to avoid redundant search. Additionally, we investigate branching heuristics adapted for this setting. We focus on the problems of argumentation and soft core, for which incremental model counting is natural. Experiments demonstrate that our method improves performance compared to current model counters, highlighting the capability of structure-aware reuse in dynamic environments.

ABSTRACT. Boolean hedonic games are a class of cooperative games involving multiple agents in which agents aim to form coalitions based on individual agents' preferences. In this work, we provide complexity results and exact algorithms for the task of forming Nash stable coalitions under different membership rights in the dichotomous setting where agents specify preferences for which coalitions they are happy/unhappy to join. The membership rights specify veto rights for coalitions, allowing a coalition to forbid an individual agent from moving (exiting the current coalition or entering another coalition) even if the agent themself would become more happy to move. We establish that various problem variants and their refinements in this setting are often situated on the second level of the polynomial hierarchy, complete for $\Sigma_2^p$. Building on the complexity results, we develop Boolean satisfiability (SAT) based counterexample-guided abstraction refinement algorithms for the $\Sigma_2^p$ problem variants and empirically evaluate a first-of-kind implementation of the approaches.

ABSTRACT. We present BAss (BDD-based ADF symbolic solver), a novel analysis tool for Abstract Dialectical Frameworks (ADFs) based on Binary Decision Diagrams (BDDs). It supports the fully-symbolic computation of all admissible, complete, and preferred interpretations, as well as two-valued and stable models of an ADF. Our approach is inspired by the recently discovered equivalence between Boolean Networks (BNs) and ADFs by Heyninck et al. (2024) and Azpeitia et al. (2024), significantly extending current BDD-based tools bioLQM, aeon, and adf-bdd. We conducted experiments on a large-scale collection of real-world models from both the BN and ADF communities. Our results show that BAss dramatically outperforms previous BDD-based tools and is competitive (even significantly better in some cases) with state-of-the-art SAT/ASP-based methods, particularly in scenarios involving large solution spaces. Notably, BAss is able to enumerate all fixed points or minimal trap spaces of certain biological networks beyond the reach of existing tools, thereby enabling new analysis and case studies in systems biology. These results highlight the practical relevance of symbolic reasoning for complex real-world applications, particularly in systems biology and formal argumentation.

ABSTRACT. Determining the validity of a quantified Boolean formula (QBF) is a PSPACE-complete problem with rich expressive power. Despite interest in efficient solvers, there is, compared to problems in NP, a lack of positive theoretical results, and in the parameterized complexity setting one often has to restrict the quantifier prefix (e.g., bounding alternations) to obtain fixed parameter tractability (FPT). We propose a new parameter: the number of variables in clauses that has to be removed before reaching a tractable class (a clause covering (CC) backdoor). We are then interested in solving QBF in FPT time given a CC-backdoor of size k. We consider the three classical, tractable cases of QBF as base classes: Horn, 2-CNF, and linear equations. We establish W[1]-hardness for Horn but prove FPT for the others, and prove that in a precise, algebraic sense, we are only missing one important case for a full dichotomy. Our algorithms are non-trivial and depend on propagation, and Gaussian elimination, respectively, and are comparably unexplored for QBF.

ABSTRACT. Hierarchical data is common in many domains like life sciences and e-commerce, and its embeddings often play a critical role. While hyperbolic embeddings offer a theoretically grounded approach to representing hierarchies in low-dimensional spaces, current methods often rely on specific geometric constructs as embedding candidates. This reliance limits their generalizability and makes it difficult to integrate with techniques that model semantic relationships beyond pure hierarchies, such as ontology embeddings. In this paper, we present RegD, a flexible Euclidean framework that supports the use of arbitrary geometric regions---such as boxes and balls---as embedding representations. Although RegD operates entirely in Euclidean space, we formally prove that it achieves hyperbolic-like expressiveness by incorporating a depth-based dissimilarity between regions, enabling it to emulate key properties of hyperbolic geometry, including exponential growth. We establish the faithfulness of our approach. Furthermore, extensive empirical evaluations on diverse real-world datasets demonstrate consistent performance improvements over state-of-the-art methods, highlighting RegD’s potential for broader applications, including ontology embedding tasks that extend beyond hierarchical structures.

ABSTRACT. We present a new approach for distilling boosted trees into decision trees, in the objective of generating an ML model offering an acceptable compromise in terms of predictive performance and interpretability. We explain how the correction approach called rectification can be used to implement such a distillation process. We show empirically that this approach provides interesting results, in comparison with an approach to distillation achieved by retraining the model.

ABSTRACT. Knowledge Representation (KR) formalisms provide precise specifications of algorithmic structure, yet it remains unclear whether gradient-trained neural networks implement these specifications even when they are theoretically expressible. Recent formal language theory tells us what Transformers \emph{can} express---masked hard-attention Transformers recognize the star-free regular languages, equivalent to first-order logic with linear order (FO[<]) and linear temporal logic (LTL)---but not what gradient-trained Transformers \emph{will} learn. We ask whether trained networks actually implement the logical circuits that theory predicts, and propose KR-Guided Mechanistic Verification to find out. The idea is to compile a B-RASP specification into a Structural Causal Model whose variables correspond to prescribed logical operations, then use Distributed Alignment Search to obtain quantitative, falsifiable causal evidence for or against each operation's presence in the trained network. We instantiate this framework on binary increment, a task for which B-RASP prescribes an explicit three-stage circuit implementable by a two-layer Transformer with O(poly(n)) parameters---exponentially fewer states than any fixed-precision recurrent or state space baselines require. The answer is affirmative: all three prescribed operations are faithfully encoded in dedicated neural subspaces, with wrong-specification controls at chance; Sparse Autoencoder decomposition independently recovers the same logical structure without supervision. Moreover, this structure is not acquired gradually: it emerges as a sharp phase transition during grokking, providing a specification-aligned progress measure that reveals \emph{what} changes during the generalization transition, not merely \emph{that} something changes. These results demonstrate that KR formalisms can serve not only as prescriptive specifications of what networks should compute, but as falsifiable causal hypotheses that mechanistic interpretability tools can rigorously test---bridging the gap between symbolic KR and neural computation.

ABSTRACT. We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for quantized GNNs with readout are (co)NEXPTIME-complete. This result implies that the verification of quantized GNNs is computationally intractable, prompting substantial research efforts toward ensuring the safety of GNN-based systems. We also experimentally demonstrate that quantized ACR-GNN models are lightweight while maintaining good accuracy and generalization capabilities with respect to non-quantized models.

ABSTRACT. Acquiring correct action theories from informal specifications remains a central challenge in KR. Large Language Models can generate plausible domain models from natural language, but the resulting theories frequently contain missing preconditions, incorrect effects, or superfluous actions. Existing refinement approaches either require human experts to correct these errors or assume that the input specification is itself correct. We present a fully automated framework that iteratively refines LLM-generated action theories using formal explanations grounded in SAT-based verification. Each candidate theory is encoded as a bounded SAT problem and tested against solvable tasks, which must admit a valid plan, and unsolvable tasks, which must be correctly rejected. When a test fails, we extract a formal explanation that pinpoints the specific theory constraints responsible for the failure, and feed this explanation back to the LLM to guide its next revision. Our initial evaluation across various planning domains shows that our framework can converge to correct theories.

ABSTRACT. While the integration of linear constraints has significantly expanded the reach of Answer Set Programming (ASP), existing hybrid solvers often rely on disparate semantic underpinnings that lack a unified logical foundation. We address this gap by introducing a many-sorted variant of the Bound-founded Logic of Here-and-There (HTB), providing a versatile framework capable of characterizing equilibrium models across a wide spectrum of alternative semantics for extensions of ASP with linear constraints. We apply this framework to the setting of difference constraints, focusing on the semantic characterization of clingodl. Central to our approach is the formalization of foundedness for numeric variables. By investigating how different hybrid systems---such as clingodl, clingcon, and flingo---justify constraint atoms, we uncover the semantic roots of their varying behaviors. This investigation results in a single, consistent framework that not only formalizes the foundations of current systems like clingodl but also facilitates the rigorous study of program simplifications and the future integration of diverse semantic principles.

ABSTRACT. Hybrid MKNF knowledge bases under the well-founded semantics integrate Description Logics with Logic Programming \citep{Knorr2011LocalCW}; however, they do not support classical negation in the rule component, which limits their ability to represent explicit negative knowledge. This limitation is particularly problematic for applications in which conclusions must be justified by explicit evidence rather than default assumptions. We introduce $\hybridmknf$, an extension of hybrid MKNF that supports classical negation in the rule component. Based on the notion of stable partitions from \cite{LIU2017123}, we provide a semantic characterisation of three-valued MKNF models for $\hybridmknf$ and define the well-founded partition as the unique stable partition that is minimal with respect to the number of true and false modal atoms. Finally, we propose a general procedure for computing the well-founded partition of a $\hybridmknf$ knowledge base.

ABSTRACT. Description logic programs are a powerful formalism for combining rules with ontologies. The well-supported semantics for description logic programs ensure that no answer sets rely on cyclic dependencies. Most popular semantics for logic programming have this property of well-supportedness. We recognize two limitations of the current well-supported semantics for DL programs: its increased computational complexity and its lack of a reduct transformation characterization. In this work, we present a new semantics which evaluates ontological atoms more strictly than the current semantics. This change makes the complexity NP-complete, rather than increasing it to the second level of the polynomial hierarchy. Additionally, we identify a syntactic class of description logic programs for which our new semantics is equivalent to the current semantics. We characterize our semantics using a fixpoint operator and a reduct-based transformation. Our new semantics is a strict subset of the current well-supported semantics, so it maintains the prior notion of well-supportedness while inducing its own stricter notion. We prefer our new notion of well-supportedness due to its similarities with logic programming.

ABSTRACT. We present chrKanren, a dialect of the purely relational constraint logic programming language miniKanren which includes support for Constraint Handling Rules (CHR), a language for writing rule–based programs such as constraint solvers. We show how to integrate CHR’s constraint propagation mechanism into the language of miniKanren search streams such that both processes remain complete. We also use chrKanren to illustrate novel applications of constraints in miniKanren, such as semantic unification of user-defined data-structures and example propagation in relational interpreters in the style of MYTH.

ABSTRACT. The formal analysis of real-time systems must address two dimensions of infiniteness: an unbounded number of agents and messages, and a potentially infinite state space induced by dense time. We present a novel narrowing-based verification method that deals with both dimensions. Technically, our approach integrates (i) rewriting modulo SMT for symbolic representation of timing constraints, (ii) narrowing with logical variables to reason about systems with a unknown number of agents, and (iii) a constraint store over partially instantiated terms, in the style of constraint logic programming. We further introduce a folding mechanism that, under certain conditions, ensures termination of the symbolic analysis. The method has been implemented as an extension of the Maude rewriting engine. We evaluate the approach by verifying the correctness of a timed mutual exclusion protocol without imposing bounds on the number of participating processes. Moreover, we show that the framework uniformly supports the analysis of other real-time models, including parametric timed automata with unspecified components that our method is able to synthesize. Our results suggest that the proposed framework provides a sound and expressive basis for the symbolic verification of real-time rewrite theories.

ABSTRACT. This paper presents Constraints as Verifiers and Emitters (CaVE), a constraint storage approach for handling integrity constraints in stableKanren. stableKanren is a normal logic-program solver based on extended unification and resolution. Integrity constraints control the outcomes of goals in normal logic programs, which is critical for non-monotonic reasoning. There is no resolution-based algorithm for handling integrity constraints that can be used in stableKanren. Therefore, we design Constraints as Verifiers and Emitters (CaVE), a constraint storage that works with resolution to support integrity constraints. We prove the soundness and completeness of CaVE with respect to the integrity constraints. We implement CaVE using Scheme in stableKanren and show a series of example normal programs written in stableKanren with integrity constraints.

ABSTRACT. The stabiliser fragment of quantum theory is a foundational building block for quantum error correction, and hence for the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal, and complete denotational semantics for stabiliser operations, including measurement, classically controlled Pauli operators, and affine classical computation; supporting an explicit treatment of quantum error-correcting codes. We interpret stabiliser operations as \emph{affine relations} over finite fields, yielding a semantics that reflects the algebraic structure underlying stabiliser quantum error correction. Because stabiliser quantum mechanics has a well-behaved algebraic structure, our relational semantics is conceptually transparent and computationally tractable when compared to standard denotational models for general quantum programs. We demonstrate the resulting semantics by describing a small, low-level assembly language for stabiliser programs with fully-abstract denotational semantics.

ABSTRACT. Equational reasoning is central to quantum circuit optimisation and verification: one replaces subcircuits by provably equivalent ones using a fixed set of rewrite rules viewed as equations. We study such reasoning through finite equational theories, presenting restricted quantum gate fragments as symmetric monoidal categories (PROPs), where wire permutations are treated as structural and separated cleanly from fragment-specific gate axioms. For six widely used near-Clifford fragments: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits), CNOT-dihedral, we transfer the completeness results of prior work into our PROP framework. Beyond completeness, we address minimality (axiom independence). Using uniform separating interpretations into simple semantic targets, we prove minimality for several fragments (including all arities for qubit Clifford, real Clifford, and CNOT-dihedral), and bounded minimality for the remaining cases. Overall, our presentations significantly reduce rule counts compared to prior work and provide a reusable categorical framework for constructing complete and often minimal rewrite systems for quantum circuit fragments.

ABSTRACT. We introduce a family of diagrammatic equational theories unifying two research programs: categorical quantum mechanics and graphical linear algebra. We prove their completeness with respect to denotational semantics described in terms of relations between vector spaces equipped with symplectic structure. This provides versatile graphical languages encompassing both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser and Gaussian quantum circuits. Terms are described by labelled graphs with input and output interfaces, and the languages are equipped with equational theories amenable to standard graph rewriting techniques. In order to reason about large composite systems, we introduce a compact scalable notation where the vertices are themselves labelled by graphs. This notation allows us to state new and powerful rewrite rules which operate on diagrams at a large scale. We also show how this notation neatly captures some important constructions, such as graph states of quantum computing and the impedance and admittance matrices of electrical networks

ABSTRACT. Deep Learning techniques are nowadays pervasive in AI. However, these approaches suffer from a lack of transparency for justifying their output and for helping users in believing in their decisions. For these reasons alternative approaches to learning deserve to be explored either for developing new tools with autonomous learning capability or for explaining the results of black-box predictors. Among them an important role is assumed since the Nineties by Inductive Logic Programming and, in particular, recently by the approaches of Learning from Answer Sets (LAS). Computing inductive solutions for LAS tasks is known to be Sigma P2 hard. In this work, we tackle this problem using a single-shot disjunctive ASP encoding based on the saturation technique originally proposed by Eiter and Gottlob. We prove that, when the background knowledge and hypothesis space form a tight program (a syntactical property) our encoding is linear in the size of the task. This approach contrasts with the state-of-the-art ILASP system, which relies on multiple iterative calls to an ASP solver. As a result, it can be directly evaluated by modern disjunctive ASP solvers, leveraging decades of research and optimization in the ASP community. We implement our method in a system named LASCO. Experimental results on a diverse set of benchmarks demonstrate that LASCO outperforms all versions of ILASP on many instances and it scales if run on multi-threaded machines.

ABSTRACT. The automated reconstruction of patient family history is a common challenge in genetic counseling for disease prevention. Such a family history is usually determined for a particular subset of diseases that are Mendelian, i.e. monogenic, and classififed into three categories depending on the chromosome the gene is located: autosomal, X-linked or Y-linked. Mendel’s inheritance laws allow for simple probabilistic modeling of the genetic transmission of monogenic disorders. Genetic counsellors use knowledge about the patient’s family history and Mendelian laws for assessing risks of transmitting or inheriting congenital conditions. We present mendelprob.pl, a probabilistic logic programming algorithm in ProbLog for deriving probabilities of inheritance of genotypes and phenotypes for genes with two alleles through multiple generations. In particular, the user can input genotypes and phenotypes for a patient and its family, and automatically determine the most probable genetic family history. We illustrate the ProbLog model on practical examples of patient pedigrees from the literature and from a genetic counseling handbook. We show that our method correctly infers probability of individual genotypes from knowledge about familial genotypes, yielding the same results as concurrent tool pedprobR. However, unlike pedprobR, our approach can exploit knowledge about familial phenotypes. It can also directly distinguish between autosomal, X-linked, and Y-linked disorders, using its intuitive logical modelling. We provide our ProbLog tool for free and open-source on GitHub, making it easily available for genetic counsellors. We conclude on the importance of providing explainable formal methods for a task that clinicians might want to perform using proprietary software.

ABSTRACT. Pearl famously argues that causal knowledge enables the prediction of intervention effects. By contrast, purely descriptive knowledge supports only conclusions drawn from observations. His theory of causality, however, is developed exclusively within Bayesian networks and causal models. Consequently, it is largely restricted to acyclic causal relationships, and transferring its ideas to other formalisms risks misinterpretation or inconsistency. This paper brings Pearl’s approach to causality into probabilistic logic programming (PLP). To this end, such programs are aligned with philosophical foundations established in prior work that do not rely on temporal notions; that is, all relevant events are assumed to occur simultaneously. A formal causal semantics for these programs, together with a notion of intervention and an implementation, is proposed. It is shown that this semantics coincides with the P-log semantics for stratified ProbLog programs, while the two may differ in the non-stratified case and for other PLP formalisms.

ABSTRACT. Motivated by challenging modelling issues in the life sciences, we investigate the relationship between logic programming semantics and the eventual states of causal processes compatible with those logic programs. More precisely, we show that while stable models of positive logic programs correspond to the eventual states of processes commencing from a neutral state and continuing undisturbed indefinitely, supported models describe the eventual states reachable from arbitrary starting points. This also contributes to the discussion of the appropriate semantics for logic programming as a causal rule language, adding a temporal perspective to recent interpretations of the stable and supported model semantics from an explanatory viewpoint of causality.

ABSTRACT. Perhaps the most popular modern formulation of actual causality is the HP account by Halpern and Pearl. Recent advancement has focused on extension of HP account to lift its limited expressiveness, in particular, Batusov and Soutchanski proposed a notion of actual achievement cause in the situation calculus, a rich first-order formalism of actions and changes. Among other things, the first-order nature allows for determining the cause of quantified effects in a given action history therein. While intuitively appealing, Batusov and Soutchanski's account is not defined in a counterfactual perspective. In this paper, we propose a notion of cause based on counterfactual analysis. In the context of action history, we show that our notion of cause generalizes naturally to a notion of achievement cause. We analyze the relationship between our notion of the achievement cause and the achievement cause by Batusov and Soutchanski. Finally, we relate our account of cause to Halpern and Pearl's account of actual causality. Particularly, we note some nuances in applying a counterfactual viewpoint to disjunctive effects, a common thorn in definitions of actual causes.

ABSTRACT. In the field of Artificial Intelligence, an agent is a system which is able to autonomously make decisions in order to reach a desired goal. As these systems grow more prevalent in our day-to-day lives, there has been an increased need to add explainability features which can provide an account for an agent’s behavior. We therefore propose a framework that outlines how to produce comprehensible explanations for policy-aware agents, or agents which have rule-enforcing policies incorporated in their decision-making framework. This framework is designed using insights from the social sciences on how to produce good explanations. It is implemented in the Answer Set Programming language while using Python to assist with information extraction and natural-language translation. Because these agents incur penalties when violating policies, we are able to leverage these penalties to detect undesirable events in scenarios that are counterfactual to the agents’ original actions. This lends itself to creating contrastive explanations (e.g., “the agent performed this action because, had it not, undesirable event X would have occurred.”), which formulate the core component for our explainability framework. The framework is evaluated using a survey wherein human participants provide feedback on our program-generated explanations.

ABSTRACT. Existing approaches to multi-agent belief combination have established mature foundations for combining uncertain beliefs under common assumptions: consensus methods use iterative averaging, logic-based methods resolve conflicting knowledge bases, and epistemic logic analyzes agents' information states. Typically, these approaches assume that the structure determining what each agent can represent remains fixed. However, in many scenarios, agents gain or lose observational capacity during execution, and what was once admissible may become structurally impossible. This paper presents a formal framework for handling such runtime changes in epistemic partitions over continuous belief profiles. A hybrid approach exploits the advantages of answer set programming in elaboration tolerance, declarative integrity constraints, and explanations, with the numerical flexibility of Python. The framework is applicable to any domain where agents operate at heterogeneous and possibly changing levels of resolution, and provides formal guarantees of admissibility preservation and unique repair, together with violation detection and explanation completeness. Evaluation across 100 randomly generated topology changes confirms complete violation detection and explanation coverage.

ABSTRACT. BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side, the precise relation between BV-categories and the logic BV is still not clear. To improve on this situation, we define in this paper a notion of proof identity for BV, based on the notion of atomic flows, which can be seen as a special form of string diagrams. Based on this notion of proof identity, we then strengthen the existing notion of BV-category and prove that it is sound with respect to the logic.

ABSTRACT. The Kripke semantics of various logics arise via categorical dualities between a category of relational frames and their maps, and a category of algebras and logical homomorphisms. When the relational frames are considered as computational systems (e.g. the states of a machine), the corresponding algebra is one of logical predicates on these systems (e.g. predicates on these states, i.e. program logics). Our aim is to extend this phenomenon to relations, putting well-behaved relations between systems (e.g. bisimulations) in correspondence with relations between predicates. This is achieved by constructing particular relational extensions of Tarski duality (for infinitary classical propositional logic) and Thomason duality (for infinitary classical modal logic). We sketch how these dualities give rise to a proof system that relates formulae between different systems.

ABSTRACT. It is an established idea in concurrency theory that every Petri net admits an unfolding semantics. This is a denotational object that represents its domain of possible executions. Unfoldings play an important role in formal reasoning and verification. This paper is concerned with the following well-known problem: while the unfolding resembles a universal construction in the category of Petri nets, it fails in general to satisfy the expected universal property because the construction overlooks the net's internal symmetries. There are two solutions: make these symmetries explicit to obtain a weak universal property (``up to symmetry''); or break the symmetries by assigning individual identities to components of the net, to restore a strict universal property. We review these two solutions in light of recent developments, and show that a universal unfolding to event structures--the canonical domain for Petri net semantics--can be established in each case. This paper additionally demonstrates a 2-categorical approach to Petri net unfoldings. We show that each unfolding semantics determines a 2-categorical relative adjunction involving Petri nets and event structures. Viewed in this way, the above two solutions can be related formally via an appropriate morphism of adjunctions. Finally we exhibit a 2-density property of event structures which implies that unfolding functors are essentially unique.

ABSTRACT. Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of $k$-induction, which is used in software verification. We moreover improve upon a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors of suitably seeded fixed point iterations: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle's sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically. Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no finite complete axiomatization of sequence models given by finitary axioms.

ABSTRACT. We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. In particular, we focus on the question of which formal theories and proof systems can efficiently prove algebraic circuit lower bounds, as follows. - **Formalization of Rank Method** Typically, algebraic circuit lower bounds are shown using the ``rank method", i.e., by exploiting non-trivial upper bounds on the rank of matrices derived from the monomial coefficients of polynomials computable by small algebraic circuits. A recent prominent application of this method is in the constant-depth algebraic circuit lower bounds by Limaye, Srinivasan and Tavenas~\cite{LST25} for the determinant and iterated matrix multiplication over fields of characteristic zero, and the finite field analogue of these results by Forbes~\cite{For24}. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC2, which captures ``reasoning with NC2 concepts''. This complements the work of Tzameret and Cook \cite{TC21}, who showed that basic structural \emph{upper} bounds in algebraic circuit complexity can be formalized in \VNCTwo. Moreover, it offers a unified proof-theoretic framework in which to formulate and study barriers for current algebraic complexity methods (complementing specific barriers discovered by Efremenko, Garg, Oliveira, and Wigderson~\cite{EGOW18} and Garg, Makam, Oliveira, and Wigderson~\cite{GMOW19}). - **Unconditional PCR lower bounds** We show that Polynomial Calculus Resolution PCR cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, PCR cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials. - **Conditional constant-depth IPS lower bounds** We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System IPS then constant-depth IPS cannot efficiently prove constant-depth algebraic circuit lower bounds.

ABSTRACT. Dynamical systems provide rigorous models of movement or evolution over time. Due to their abstract nature, they may be naturally employed for modelling e.g. physical, biological, or financial phenomena. Specifically in the context of Computer Science, computational processes, machine learning algorithms, and multi-agent systems may be regarded as dynamical systems. This wide range of applicability has sparked interest in designing formal specification languages for dynamical systems which may be amenable to automated or computer-assisted deduction, leading to the introduction of *dynamic topological logic* (DTL). When space is continuous but time is discrete, it is known that a sound and complete deductive calculus for DTL exists. However, discrete spaces are oftentimes more suitable for representing phenomena arising from CS, and in this setting, whether such a calculus exists even in principle has been an open question for more than two decades. More precisely, it was unknown whether the DTL of Alexandrov spaces is computably enumerable. In this paper, we use model-search techniques to provide an affirmative answer.

ABSTRACT. A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates---used to establish semantic termination arguments---to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, and two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof term constructed in the definitional variant of the theory can be soundly embedded into the propositional variant, while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.

ABSTRACT. Motivated by applications in computable analysis, we study fixpoints of certain endofunctors over categories of containers. More specifically, we focus on fibred endofunctors over the fibrewise opposite of the codomain fibration that can be themselves be represented by families of polynomial endofunctors. In this setting, we show how to compute initial algebras, terminal coalgebras and another kind of fixpoint $\zeta$. We then explore a number of examples of derived operators inspired by Weihrauch complexity and the usual construction of the free polynomial monad. We introduce $\zeta$-expressions as the syntax of $\mu$-bicomplete categories, extended with $\zeta$-binders and parallel products, which thus have a natural denotation in containers. By interpreting certain $\zeta$-expressions in a category of type-2 computable maps, we are able to capture a number of meaningful Weihrauch degrees, ranging from closed choice on $\{0,1\}$ to determinacy of infinite parity games, via an ``answerable part'' operator.

ABSTRACT. Completeness and representation theorems in abstract algebra, lattice theory, and theoretical computer science are tied to the existence of ideal objects, and thus to transfinite methods such as Zorn's lemma. Yet many concrete uses of such theorems appeal to finite approximations only, which carry a clear computational meaning. In this paper, we introduce co-coverages on complete lattices as a uniform way to specify ideal elements, and associate to each co-coverage a canonical closure operator with a folding property reminiscent of the covering principles at work in constructive algebra. This yields finitary, choice-free alternatives for arguments in which ideal objects are employed to reduce a computational problem to subcases. In a classical setting, our closure operators admit bases which allow to recover a host of primality principles such as the universal Krull–Lindenbaum theorem and Henkin’s lemma.