Papers

Signal Temporal Logic (STL) is a popular formalism for the temporal safety properties of cyber-physical systems, most often used for runtime verification. In the synchronous family of languages, safety properties are instead expressed as synchronous observers, modules composed with a program for static verification, which are also runnable specifications suitable for runtime verification, though this use is rarely explored. We present a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre. Unlike previous work, we allow arbitrary nesting of bounded SSTL properties via modular compilation, and admit a globally unbounded outer operator for online monitoring; the resulting observers serve both runtime verification and, as a by-product, static verification with the Kind2 model checker. We further contribute an interactive visualiser that renders a property's three-valued verdict over an editable trace, and evaluate on two case studies from the literature: a spring-mass system and a car-following cruise controller.

We prove that, on finite simple undirected graphs equipped with a single Boolean node feature, the Boolean queries expressible in $\Sigma$-MPLang, for any collection $\Sigma$ of eventually constant activation functions and with arbitrary real coefficients, form a strict subclass of the Boolean queries expressible in ReLU-MPLang. We thereby settle a recently posed open problem: whether ReLU-MPLang is more powerful than trReLU-MPLang when it comes to Boolean queries. In particular, this implies that ReLU-GNNs are strictly more expressive than {TrReLU,id}-GNNs with respect to Boolean queries on Boolean-featured graphs.

We study the amalgamation decision problem (ADP): given a universal first-order sentence $\Phi$, decide whether the class $\mathrm{fm}(\Phi)$ of its finite models has the amalgamation property. We call $\Phi$ semantic Horn if $\mathrm{fm}(\Phi)$ is closed under binary direct products. By McKinsey's theorem, this is equivalent to $\Phi$ being logically equivalent to a universal Horn sentence. The distinction concerns the input representation: $\Phi$ itself need not be given in Horn form, and converting it into an explicit Horn normal form can incur an exponential blow-up. We prove that the ADP is decidable under this semantic promise. To this end, we associate with $\Phi$ a finite-domain CSP template, called its completion template, and a distinguished infinite family of CSP instances, called its atlas instances. The class $\mathrm{fm}(\Phi)$ has the amalgamation property precisely when all atlas instances have a solution. For semantic Horn inputs, we prove that the completion template admits a semilattice polymorphism. Consequently, its CSP has bounded width and is decided by a fixed level of local consistency. We introduce uniform contextual strategies, finite certificates expressing this local-consistency condition simultaneously for all atlas instances, and give an effective fixed-point procedure for deciding whether such a certificate exists. The resulting algorithm runs in 2ExpTime in general and in ExpTime under any fixed bound on the arities of the input relations. More generally, the construction gives a decision procedure whenever the associated completion template has bounded width. These bounds are optimal: the semantic Horn ADP is 2ExpTime-complete in general and ExpTime-complete for every fixed arity bound of at least three. Both hardness results already hold for syntactic universal Horn sentences.

Nested conditions are used, among other things, as a graphical way to express first order formulas ruling the applicability of a graph transformation rule to a given match. In this paper, we first introduce several operators on conditions mimicking logical connectives. Next we propose an original notion of structural morphism among nested conditions, and we identify circumstances under which morphisms are consistent with the entailment of the corresponding conditions. Finally we frame the results in a categorical context, proving functoriality and universality properties of the various operations.

We define call-by-name and call-by-value reduction and reduction strategies for the calculi slmu (symmetric lmu), lmmt, and Xs (X with implicit substitution). We establish a strong relation between these notions through defining a single interpretation from slmu to lmmt that respects normal reduction, as well as the call-by-name and call-by-value reduction in slmu within the their counterpart in lmmt; for the strategies, we will show similar, but weaker results. We also define a single mapping from lmmt to Xs, and show that this also respects all three notions. We then continue with studying the natural encoding of Xs into lmmt, and show that only full reduction is respected, but that reduction steps are needed to model substitution, so the CBN and CBV strategies cannot be respected. We conclude with studying the combination of our efforts and define an interpretation of slmu into Xs, and show that CBN and CBV reduction are respected. This result underlines that Xs and lmmt are similar, but different calculi, and that the nature of slmu makes that any encoding into either can never fully respect the strategies.

Formal theorem proving with large language models remains challenging due to the difficulty of navigating large proof search spaces efficiently. Existing tree search approaches either feed verbose compiler error messages directly into the generation context, increasing context usage during search, or employ non-standard evaluation protocols that prevent direct comparison with established baselines. We propose a three-role Monte Carlo Tree Search (MCTS) framework that treats the Lean 4 compiler purely as a reward oracle using compiler output as a scalar signal for UCB-guided tree updates without feeding error content into the generation context. Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation. We evaluate across 4 benchmarks spanning competition mathematics and physics (MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata) with three prover models at standard proof attempt budgets (PAB@16 to PAB@256). Our method achieves 87.1% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget. Through an exhaustive axiom-level audit of every compiled proof, we further identify reward hacking in search-based theorem proving: DeepSeek-Prover-V2-7B produces proofs on PutnamBench that pass compilation and the standard sorry-token scan while depending on sorryAx. The audit removes 4 and 8 such proofs from whole-proof sampling at PAB@32 and PAB@128, and 11 and 19 from MCTS. We do not attribute these counts to the search procedure; we report them to establish that kernel-level auditing is necessary for compiler-verified evaluation.

We study the discrete point-based fragment of Ensemble Logic $\EL(\Nat)$ over the natural numbers, a logic combining displacement $\varphi_u$, bounded metric modalities $\boldBox_t$ and $\mdiamond_t$ with additive bounds, Boolean connectives, and first-order quantification over $\Nat$. Motivated by the need for a unified symbolic layer for biomedical knowledge with temporal, spatial, genomic, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of $\EL(\Nat)$ over a finite proposition set $\mathcal{P}$ into first-order monadic Presburger arithmetic $\FO(\Nat,<,+;\mathcal{P})$. This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter machines with recurring control states proves that satisfiability is $\Sigma^1_1$-complete and validity is dually $\Pi^1_1$-complete. Expressively, $\EL(\Nat)$ strictly extends the star-free $\omega$-languages and is incomparable with the $\omega$-regular languages: it defines the non-$\omega$-regular counting language $\{a^mb^mc^md^m\mid m\geq 1\}\cdot\Sigma^\omega$, whereas a delimited parity language remains outside the logic by classical Presburger-arithmetic lower bounds. On the proof-theoretic side, we present a sound Hilbert system $\HEL$ and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible.

Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models, which come with limited guarantees of accuracy. In addition, these methods typically only consider inputs that are known to be correct, and therefore do not assess whether the AF translates incorrect inputs faithfully. To address these limitations, we propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples. Our method is based on automatically generating perturbed reasoning steps that are designed to be invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. We apply our method to eight AF systems across four mathematical datasets, and observe pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements. The most validity-preserving fine-tuned AFs are also the most sycophantic, suggesting a tension between validity and invalidity preservation in current AF systems.

Large-scale formalization of advanced mathematics requires more than translating individual statements: it must reconstruct a coherent theory distributed across heterogeneous sources. This process raises four challenges: discovering implicit dependencies, correcting source defects, preserving semantic fidelity, and reconciling cross-source misalignments. We present FormaTheoria, an end-to-end, AI-assisted workflow that coordinates source acquisition, formalization, proof construction, recursive dependency discovery, independent review, and reconciliation, while preserving provenance and protecting approved declarations. A shared agent framework supports long-horizon execution through tool use, context compaction, review-gated termination, section-level source context, and dependency-aware batch parallelization. Applying FormaTheoria to major components of the Classification of Finite Simple Groups (CFSG), we construct a machine-checked Lean development extending through the Bender–Suzuki theorem and encompassing the Feit–Thompson Odd Order Theorem, Glauberman's $Z^*$ theorem, and the Brauer–Suzuki theorem. This development verifies an extensive body of deeply interdependent finite-group theory while providing a foundation for continuing the CFSG formalization. An empirical analysis of the code and recorded construction process supports the practical relevance of the identified challenges and illustrates the roles of the corresponding workflow components. Together, these results demonstrate how AI-assisted workflows can reconstruct mathematically significant formal theories from distributed literature by combining language-model agents with formal verification, structured review, and explicit dependency management.

The Traveling Salesperson Problem (TSP) is one of the best-known problems in computer science and arises in many engineering applications, such as smart vehicles and intelligent transportation systems. In the "Euclidean" case, each node is defined by its coordinates in the plane and distances are computed using the Euclidean metric. In the Constraint Programming (CP) literature, the Euclidean TSP is typically addressed by computing the full distance matrix and treating it as a general case; however this approach ignores the geometric information carried by the points' coordinates. In this work, we propose new filtering algorithms, implemented in Constraint Logic Programming (CLP), that exploit such geometric information to achieve stronger constraint propagation than existing approaches. Moreover, we show how this methodology can be extended to other Euclidean variants of the TSP, including the Euclidean Generalized Traveling Salesperson Problem (EGTSP), which is relevant in practical routing and logistics applications. Experimental results demonstrate the computational advantages of the proposed approach.

The Weighted First-Order Model Counting Problem (WFOMC) asks for the weighted sum of models of a first-order logical sentence over a domain. It is a fundamental problem in statistical relational learning, with applications extending to enumerative combinatorics and graph polynomials. Computing WFOMC for the three-variable fragment is $\mathsf{\#P}_1$-hard, whereas polynomial-time algorithms exist for the two-variable fragment and its extensions by cardinality constraints and counting quantifiers. In this work, we explore computing WFOMC in polynomial time over linearly ordered domains, enabling tractable reasoning across inference scenarios and combinatorial problems involving sequences. Because encoding a linear order in standard first-order logic requires three variables, negating our polynomial-time aspirations, we add a linear order axiom directly to the language. This forces one predicate to impose a total ordering on domain elements. We first prove that WFOMC with the linear order axiom can be solved in time polynomial in the domain size. We then extend this result to ordered domains with access to successor relations. While this holds when successors are explicitly defined via the linear order, we demonstrate an alternative implicit approach where successor relations are part of the axiom. This implicit method exhibits significantly better performance on all tested instances, sometimes providing exponential runtime improvements. Finally, we analyze scenarios with two distinct linear orders. We show that WFOMC over the two-variable fragment with two linear orders is $\mathsf{\#P}_1$-hard. However, we develop a polynomial-time algorithm for WFOMC with one linear order and a successor relation of another, pushing the intractability barrier further, yet still leaving the question of how close to a second full linear order one can get.

A precise (sound and complete) subtyping relation $\leq$ specifies that $T'$ is a subtype of $T$ if and only if a program of type $T'$ can always safely replace a program of type $T$ without compromising the safety of a larger program. This paper formulates and proves preciseness of subtyping for mixed choice multiparty session types with session delegation, creation, and interleaving. We prove soundness by developing the first general type system for a full mixed choice multiparty session $\pi$-calculus. To prove completeness, we introduce the three-party lock, which is a minimal and general form of liveness error for handling interleaved sessions, and we establish a new proof technique based on a construction of scheduler processes which enable exhaustive detection for all failures of the subtyping relation. We then extend the preciseness results to a family of mixed choice multiparty session types. Algorithms for checking (1) subtyping and (2) safety, deadlock-freedom, and liveness of typing contexts are fully implemented and optimised to run in quadratic time with respect to the size of the state space and typing context, and have been evaluated with (mixed choice) case studies from the literature.

We prove decidability of Simpson's intuitionistic modal logic IK$ by working directly with cut-free nested proofs. Once the end formula is fixed, only finitely many combinations of input and output formulae can occur at a node, although the modal tree itself remains unbounded. We order these nested sequents by rooted homeomorphic embedding: weakening may add input formulae, while transitivity allows a modal edge to be stretched into a non-empty path. Kruskal's theorem makes rooted homeomorphic embedding a well-quasi-order, but does not by itself make backward application of the rules effective: an inference may still occur inside an arbitrarily large context. The finite-support lemma shows that a minimal predecessor need retain only the positions used by the inference, the images of the chosen basis elements, and the branch points joining them. Together with an effective enumeration of bounded rule instances, this bound makes the minimal predecessors computable. Backward closure from the initial sequents gives an increasing sequence of finitely based upward-closed sets. The sequence eventually stabilises, and its stable value is the set of provable nested sequents. At that point, finitely many cut-free proofs suffice: every other provable nested sequent is obtained from one of them by weakening along an embedding. Their maximum height gives a uniform proof-height bound.

Symbolic model checking is an effective approach for verifying semantically rich temporal-logic properties of cyber-physical systems, but it hinges on discretizing continuous-state dynamics into a finite-state abstraction. To transfer verification guarantees from the abstract model to the concrete CPS, the abstraction must conservatively approximate the concrete state space and behaviors. Hence, model-builders must maintain this soundness while balancing pessimism with tractability. However, they face several common pitfalls such as under-approximating the state space, under-approximating transitions, unsound pruning of "degenerate" behaviors, and improper specification lifting. This tutorial presents a pragmatic, conservative-by-construction workflow for building discrete abstractions of closed-loop dynamical systems. The workflow consists of four modular steps with interchangeable subroutines: (i) state-space partition and abstraction-function design, (ii) conservative transition construction via axis-aligned bounding boxes, polytopes, or sampling with PAC coverage certificates, (iii) mitigation of spurious transitions and self-loops using certified erasure and counterexample-guided abstraction refinement, and (iv) sound lifting of LTL specifications using may-must semantics. We demonstrate the end-to-end pipeline on three case studies and report how these design choices affect abstraction structure, runtime, and verification outcomes.

Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate representation between syntax and classical denotational semantics, which treats programs as operators. Abstract compilation is then understood as the act of abstracting such operators. We develop higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers. We instantiate this framework in the context of recurrence-based static cost analysis, developing solver-independent, optimal recurrence extraction techniques for recursive programs over algebraic data types, that support general function unknowns and catamorphic metrics, a broad class of size metrics beyond traditional approaches.

Decentralization as a concept in computer science has existed for over half a century. Despite its fundamental role across domains such as security, distributed computing, artificial intelligence, cloud infrastructures, and Internet of Things (IoT) architectures, there remains no universally accepted definition of decentralization applicable across computer communication systems. This has become increasingly problematic with the emergence of decentralized AI and machine learning paradigms, including collaborative training, distributed inference, blockchain-based, and agentic AI, where decentralization is often treated as a core design objective. Meanwhile, existing approaches frequently conflate decentralization with related notions such as distribution of trust or specific implementation paradigms. Such ambiguity creates inconsistencies in system analysis, limits comparability between works, and weakens the rigor of formal reasoning surrounding communication architectures and protocol design. In this work, we define this research gap as the Decentralization Problem. We analyze the formal-semantic, epistemological, and pragmatic foundations of decentralization and introduce a graph-based ontology defining it as both relational and subject-specific property of computer communication systems. The framework formally distinguishes decentralization from distribution and supports evaluation through two novel metrics: Void Tolerance and Imperviousness. We also provide a browser-based implementation that enables automated classification and metric computation of arbitrary systems. Instantiations to federated learning and blockchain architectures show consistent, comparable assessments where existing definitions produce incomplete or contradictory conclusions, providing a domain-independent foundation for analysing decentralization across heterogeneous systems.

Various type systems have been developed to track the cost $\kappa$ of a computation using a cost-tracking monad $M\ \kappa \tau$. On its own, this only tracks the worst-case cost of a computation. If we also want to track amortized cost, then we can add a type $[\kappa]\tau$ which stores potential $\kappa$ with a type $\tau$, together with operations for storing and releasing potential. In this work, we build on one such system, $\lambda$-amor: $\lambda$-amor allows to track cost and potential in the type system and subsumes effect and coeffect-based systems, call-by-value and call-by-name based languages. In this paper, we identify the abstract properties that denotational models of type theories for cost and potential have to satisfy: Cost and potential must be modelled by an adjoint pair of graded functors, where the functor modelling cost forms both a graded monad and a compatible graded comonad. We present three concrete instances of this general abstract scheme: (1) A simple set-theoretic model that ignores the cost tracked by the type system, (2) the Kripke logical relations model in the original $\lambda$-amor paper (which we show can be turned into an instance of the adjoint model), and (3) a novel model based on copresheaves on a monoidal category of costs, where we model pairs and functions by Day convolution and its right-adjoint.

Given a category $\calC$ and a center, that is a collection of pairs $(d_i, N_i)$ consisting of a morphism $d_i$ and a sieve $N_i$ over its codomain, the dilatation of $\calC$ is a new category $\calC'$ in which every $n \in N_i$ factors, uniquely and functorially, through $d_i$. This paper presents the theory of dilatations of categories through a full formalization of the construction and its main theorems in the Lean~4 proof assistant, on top of the Mathlib library. An appendix collects a systematic dictionary between the mathematical statements and the Lean declarations that formalize them.

GK is a query-directed first-order prover that extends ordinary resolution-based proof search with explicit positive and negative claims, numerical confidence values, and prioritized default rules with exceptions. It works directly with non-ground clauses, including equality and function terms. Candidate proofs are found by bounded first-order proof search; exception conditions of defaults are checked by further bounded searches, recursively when exceptions themselves depend on defaults. This avoids requiring a finite global grounding, while allowing incomplete searches to be reported as such. This paper adds structure-preserving quantitative reporting to that framework. Retained proof histories are used in two calculations. The first reconstructs the uncertain ground premises used by each proof and computes the probability that at least one retained proof is available, without counting shared premises independently. The second resolves positive and negative support at intermediate atoms before that support is propagated through later rules; the same calculation evaluates uncertain exception conditions for individual rule applications. Reports separate positive support, negative support, conflict, and ignorance and identify detected incomplete calculations or fallbacks. The implementation performs bounded reconstruction and dependency traversal after proof search and still requires no global grounding. Analytic examples and independent simulators reproduce the reference calculations on their stated fragments. Comparisons with probabilistic logic, probabilistic ASP, default logic, and goal-directed ASP identify cases of agreement, semantic difference, unsupported translation, and incomplete computation.

A disjunctive policy allows a value to depend on at most one of two secrets and never on both: an analyst may consult one client's file or the other's, a share of a split secret may be released but not its sibling. Such policies are not lattice-shaped, and Hunt and Sands introduced the quantale of information to give them a semantics, leaving the enforcement layer open. We build the flow-sensitive type system family that the quantale calls for, and show that the object which makes such families useful, the universal type object from which every member specialises, splits in two, with a consequence for enforcement. Over the free commutative quantale on the program variables the whole mechanism survives for every policy: monotone renaming, canonical derivations, principal typings, internal completeness. Over the free object with idempotent generators the certified bound is strictly more precise and still sound, because it records that two reads of one source honour one disjunct. The gap cannot be closed from inside the independent-attribute family: no mechanism of that shape whose labelling maps support monotone renaming certifies a bound more precise than the first, and for principal typings under generator-exact homomorphic specialisation the two coincide. Under the ethical-wall and secret-sharing labels the second read of a disjunctive source therefore drives every such certificate to no guarantee, and programs that satisfy the policy are rejected. The literal transcription of the lattice-era object is no escape either: it is a further quotient that loses branch disjunction. Precision is recovered by deferring specialisation to the judgement level, and the resulting read-out map is the least sound join-preserving one.

Institutional policies stay in natural language while the systems that check compliance demand machine-readable constraints. Bridging that gap is still done by hand. PolicyKG closes the loop. It is an LLM pipeline that reads a policy PDF, classifies each sentence as an obligation, permission, or prohibition, lifts the label into first-order deontic logic, and emits SHACL constraints. Four stages run on a LangGraph state machine with per-stage validators. The piece that matters most is the Corpus Adapter: a YAML vocabulary registry that grounds LLM predicates in a target ontology. Retargeting to a new domain means swapping the registry, not retraining a model. On the Asian Institute of Technology Policies and Procedures corpus (1,663 sentences, 443 rules), PolicyKG reaches 86.9% deontic classification accuracy (Cohen's kappa = .709). Three annotators independently re-label a 50-item sample and agree at Fleiss' kappa = .844. SHACL shape correctness on a 69-shape subset is F1 = .866. The FOL path handles 79.2% of rules; the rest go through a direct NL-to-SHACL fallback. We audited every one of the 443 rules for second- or higher-order constructs. An automated regex checklist flagged none, and a first-author pass on the 92 FOL-fallback cases confirmed the same. The exact upper 95% Clopper-Pearson bound on the true HOL rate is 0.67%. This is an audit finding for one corpus, not a proof of FOL sufficiency for institutional policy. Swapping the AIT registry for a GDPR registry raises exact property alignment from 1/15 to 11/15 (Fisher's exact p < .001; Cohen's h = 1.53). On the LexDeMod lease-contract benchmark (N = 200), Macro F1 drops to .370 because lease English uses "shall be entitled" for permission – exactly the vocabulary mismatch registry swap is meant to fix. Repeated runs produce hash-identical SHACL outputs.

The term “partition logic” denotes two constructions at different levels. In automaton and generalized-urn models, selected partitions generate Boolean event algebras whose contextwise union forms a concrete pasted event structure; in Ellerman's framework, whole partitions are classifications governed by refinement and partition operations. For a finite set $U$, Ore's correspondence maps each generator $\pi$ to its Boolean algebra $\BA(\pi)$, but it neither identifies the pasted carrier with $\Part(U)$ nor makes pasting a partition operation. It yields $\BA(\pi\wedge\sigma)=\BA(\pi)\cap\BA(\sigma)$ and $\BA(\pi\vee\sigma)=\langle\BA(\pi)\cup\BA(\sigma)\rangle_{\rm BA}$, where $\langle\cdot\rangle_{\rm BA}$ denotes Boolean-algebra generation. Thus meet captures the common event algebra, whereas join gives the ambient Boolean closure. Chinese-lantern, Firefly, and triangular examples distinguish shared events, atomic intertwining, and inherited concrete order. Ellerman's direct-sum decompositions (DSDs) provide a vector-space analogue: component projections of an orthogonal DSD resolve the identity and encode exclusive outcomes, but its components are not equivalence classes of vectors. Gleason and Kochen–Specker applications require globally context-consistent valuations on those projections.

Termination and nontermination of infinite-state systems are complementary problems that, despite their close connection, are typically addressed by separate techniques. The core idea of this paper is to connect termination and nontermination analysis, enabling the two to share intermediate results and guide one another. We present a new termination analysis approach based on the generation of well-founded transition invariants. It leverages Craig interpolation for transition invariant generation, capturing the structural reasons for termination. The proposed technique extends safety-based nontermination analysis, enabling it to prove both termination and nontermination within a unified framework. We implemented our approach in the GOLEM verification framework and evaluated it on benchmarks from the Termination Competition (TermComp). Empirical results demonstrate that combining termination and nontermination is beneficial and yields performance comparable to state-of-the-art tools.

We establish a Lindström-style maximality theorem for Maruyama's exact-truth-test presentation of Fitting's modal logic over a fixed finite Heyting algebra and crisp Kripke frames. Unlike the existing characterization over finite MTL-chains, no linearity or distinguished coatom is assumed. Exact truth tests yield Boolean tests for designated and non-designated values and a derived existential modality sufficient for the saturation argument. We prove that every abstract extension which is compact, has the Tarski Union Property, and is strongly invariant under bisimulation is $1$-expressively equivalent to Maruyama's version of Fitting's Heyting-valued modal logic. As a consequence, every exact-value fibre of an extension formula is definable in Maruyama's exact-truth-test modal language.

The paper Conjecture: the set of prime numbers is supernatural conjectures that no non-constant function built from the identity and constants by finitely many pointwise additions, multiplications, and exponentiations maps every positive integer to a prime. We give a complete Lean~4 formalization of that paper over Mathlib: every definition, example, remark, numbered result, and experimental table row has a machine-checked counterpart, with no \lcode{sorry}. The conjecture and similar generalizations are stated exactly, as named open problems. So stated, the conjecture becomes a precise target: an automated reasoning system can now attempt a kernel-checked proof.

Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 elementary identities. Surprisingly, Wilkie showed that the following identity is valid over the positive integers and yet does not follow from Tarski's axioms: \begin{align*} &\left((1+x)^y + (1+x+x^2)^y\right)^x \cdot \left((1+x^3)^x + (1+x^2+x^4)^x\right)^y = \\ &\left((1+x)^x + (1+x+x^2)^x\right)^y \cdot \left((1+x^3)^y + (1+x^2+x^4)^y\right)^x. \end{align*} Gurevič gave an algebra on 59 elements that satisfies Tarski's axioms but not Wilkie's identity, and over the years several authors whittled down the size of such a countermodel, culminating in a countermodel of size 12 due to Burris and Yeats. On the other hand, Zhang proved that there is no countermodel with fewer than 11 elements. Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats. Moreover, we show that there are exactly 8,957,952 countermodels on 12 elements up to isomorphism and provide a simple classification of them. Our SAT approach outperforms dedicated tools for finding countermodels in equational theories, namely Mace4 and SEM. Furthermore, using autoformalization, we prove the correctness of our main result in Lean.

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

The runtime of Constraint Programming (CP) solvers is highly sensitive to modeling choices, such as symmetry breaking, implied constraints, global constraints, constraint reformulation, and variable representation. Improving these constraint models has traditionally required human expertise, and existing automated reformulation systems are restricted to a predefined library of hand-crafted transformation rules. We introduce an agentic framework that instead reformulates a constraint model from an open-ended space and establishes correctness empirically rather than by construction: a Large Language Model (LLM) agent, given a model and three training instances, proposes alternative formulations, validates each by injecting its solution back into the original model, and diagnoses and repairs failures, returning the best variant it finds in a median of about fifteen minutes. The models are expressed in the CPMpy modeling library, and each proposed model is evaluated on three larger test instances. Across nine combinatorial optimization problems, the generated models outperform the originals on 21 of 27 test instances, and on some problems solve more than two orders of magnitude faster. A comparison against non-agentic baselines that reuse the same validation and selection tools indicates that the gains stem from the agent's iterative diagnosis and repair, not merely from sampling several candidates. These results demonstrate that autonomous agentic methods can support the improvement of constraint models.

In this paper we discuss the foundations behind a novel methodology for the validation of semantic mappings between different data sources based upon different foundation ontologies, where the methodology builds a framework based upon the metaphysical commitments of the ontologies. We provide as example the test case of mappings between IES and BFO, and we especially focused on providing cardinality constraints on the mappings between the two ontologies. In order to demonstrate the applicability of our method, we showcased how these principles can be operationalized through SPARQL queries validating the results of a mapping pipeline.

Runtime monitoring has recently been proposed as a rigorous method for analyzing algorithmic fairness of autonomous decision systems used in critical scenarios such as credit lending, job application, and the criminal justice system. Prior work has shown that runtime monitoring, in principle, can be an effective technique for establishing the kind of human oversight required by legislation such as the EU Artificial Intelligence Act. In practice, the available monitoring tools have not been developed with this application in mind and display several critical shortcomings in these scenarios. In this paper, we present FairMon, a runtime monitoring tool tailored to fairness analysis of high-stakes decision systems. FairMon uses RTLola as a flexible specification language for monitors, which we have extended with conditional probability operators that allow for concise descriptions of algorithmic fairness properties. The tool also features a real-time visualization of intermediary values, enabling human insight into the dynamics of the monitored system.