Papers

This paper investigates cross-agent specification portability using Oracle-to-PostgreSQL migration as a controlled software transformation task. The study combines two experimental stages. First, a specification-first migration pipeline was evaluated on 1,006 PL/SQL files, of which 623 were successfully regenerated and 380 generated scripts executed successfully in PostgreSQL 16. Second, cross-agent experiments were conducted on a dataset of 1,802 Oracle scripts with corresponding PostgreSQL implementations using Amazon Kiro, Google Gemini, and GitHub Copilot, with Claude Code and Cursor included in the initial single-agent evaluation. Native and foreign specifications were assessed using Token F1, exact match, SQL syntax validity, AST exact match, AST mean similarity, and immediate runnability. The results show that specification size alone does not predict implementation quality and that cross-agent transfer can produce substantial agent-dependent degradation. The strongest replicated case occurred when Gemini directly consumed a Kiro-origin specification, producing a Token F1 of 0.035, SQL syntax validity of 2.33%, and AST mean similarity of 0.015. Rewriting substantially improved Gemini in the tested configuration, compression did not provide a universal benefit, and retrieval-augmented ingestion was the only common strategy represented on the per-agent Pareto frontiers of both Gemini and Copilot. The findings suggest that specifications in heterogeneous SDD workflows should not automatically be treated as agent-neutral artifacts and motivate explicit consideration of specification portability, agent-specific interpretation, and retrieval-based access in multi-agent software engineering.

Courcelle's Theorem states that on graphs $G$ of tree-width at most $k$ with a given tree-decomposition of size $t(G)$, graph properties $\mathcal{P}$ definable in Monadic Second Order Logic can be checked in linear time in the size of $t(G)$. Inspired by L. Lovász' work using connection matrices instead of logic, we give a generalized version of Courcelle's theorem which replaces the definability hypothesis by a purely combinatorial hypothesis using a generalization of connection matrices. This paper clarifies the role of logic in such theorems and displays their purely combinatorial assumption.

Runtime assurance for autonomous systems increasingly requires reasoning not only about observed executions but also about anticipated future behaviors. Traditional runtime verification, however, primarily evaluates the execution observed so far and does not directly account for predicted continuations. We propose a formal framework for runtime assurance that combines monitoring of the observed execution with analysis of multiple predicted continuations. To support this integration, we introduce Split Linear Temporal Logic (SplitLTL), a linear-time temporal logic that assigns complementary roles to past and future temporal specifications within a single specification. The past component uses the observed history to determine the assurance requirements applicable at the current point of execution, while the future component evaluates predicted continuations against those requirements. The framework therefore filters predicted continuations according to the requirements induced by the observed history, identifying admissible continuations that can support subsequent decision making. We formally define the syntax and semantics of SplitLTL and present an online monitoring architecture for evaluating observed executions together with predicted continuations.

Many scientific discovery problems require searching combinatorial hypothesis spaces under complex domain constraints. Reinforcement learning (RL) offers a promising approach, but existing methods rely on scalar rewards that provide limited information about why candidate solutions fail, leading agents to repeatedly explore invalid regions. We introduce Certification-Driven Reinforcement Learning (CDRL), a framework that leverages structured feedback from symbolic reasoning tools. When a candidate violates domain constraints, these tools produce certificates identifying the actions responsible for failure. CDRL converts these certificates into reusable constraints that eliminate classes of invalid solutions and guide exploration toward valid regions. We evaluate CDRL on neutrino flavor model discovery in theoretical particle physics, where the hypothesis space exceeds $10^{26}$ possible models, and compare it with the state-of-the-art RL approach previously used for this task. Across three theory spaces, CDRL achieves up to 1.95$\times$ higher valid model rates and up to 6.33$\times$ higher neutrino model rates while evaluating up to 4$\times$ fewer candidates. We further extract 40 interpretable rules from search trajectories using a post-hoc decision-tree framework and show that reusing them as soft constraints yields gains of up to 2$\times$ in valid model rates and 3$\times$ in neutrino model discovery across all three theory spaces. These results suggest that CDRL uncovers reusable structure in combinatorial search spaces and provides a general framework for scientific model discovery.

Decision trees play an important role both in Machine Learning and Knowledge Representation. They are attractive due to their immediate interpretability. In the spirit of Occam's razor, and interpretability, it is desirable to calculate the smallest tree. This, however, has proven to be a challenging task and greedy approaches are typically used to learn trees in practice. Nevertheless, recent work showed that by the use of SAT solvers one may calculate the optimal size tree for real-world benchmarks. This paper proposes a novel SAT-based encoding that explicitly models paths in the tree, which enables us to control the tree's depth as well as size. At the level of individual SAT calls, we investigate splitting the search space into tree topologies. Our tool outperforms the existing implementation. But also, the experimental results show that minimizing the depth first and then minimizing the number of nodes enables solving a larger set of instances.

Examples and counterexamples define the boundaries of mathematical propositions, test foundational conjectures, and resolve open structural problems in abstract algebra. In loop theory, an Osborn loop is a crucial generalization of a Moufang loop satisfying a specialized variable-sandwiching identity. While small finite non-associative examples are known, constructing large examples of proper Osborn loops (loops that are neither conjugacy closed nor Moufang) remains a computational bottleneck. In this paper, we establish an efficient framework for generating large proper Osborn loops by taking the direct product of non-associative conjugacy closed (CC) loops and Moufang loops. We outline the boundary constraints necessary to prevent structural collapse into sub-varieties and provide explicit examples up to order 2025 validated via the GAP package LOOPS.

Turing completeness of a programming language or system characterizes its expressive power; and the strong Church-Turing hypo-/thesis refines such from qualitative to polynomial-time equivalence. Exact Real Computation (ERC) is a novel numerical programming language paradigm: for the imperative processing of continuous data as entities appearing as exact, i.e. devoid of rounding errors [doi:10.1007/978-3-662-44199-2_107]. ERC has been designed [doi:10.46298/lmcs-20(2:17)2024] as convenient and practical alternative, namely proven qualitatively equivalent, to the Turing machines originally underlying Computable Analysis [doi:10.1007/978-3-642-56999-9,doi:10.1007/978-1-4684-6802-1]. The present work quantitatively strengthens this qualitative Turing-completeness: We assign bit-costs to ERC's operational primitives (including partial/multivalued tests) in such a way that any real function incurring polynomial cost becomes Turing-computable in polynomial time, and vice versa. Runtime measurements on implementations in the iRRAM C++ library confirm our theoretical performance predictions.

Vision-language-action (VLA) models can follow natural-language (NL) task instructions, but such instructions may not precisely specify safety-critical or spatiotemporal requirements on the resulting behavior. We introduce Logic-VLA, a formal-requirement-aware VLA that conditions on Signal Temporal Logic (STL) specifications supplied at inference time. Logic-VLA uses a syntax-graph-based STL encoder pre-trained to capture temporal logic semantics. Policy adaptation proceeds in two stages: STL-conditioned supervised fine-tuning on satisfying demonstrations is followed by trajectory-level preference optimization over matched satisfying-violating rollout pairs using a flow-matching surrogate for Identity Preference Optimization. This formulation improves formal requirement satisfaction while preserving the nominal NL task. We evaluate Logic-VLA in closed-loop quadcopter navigation simulation across randomized photorealistic environments and test generalization to STL formulas unseen during training. Across the evaluation benchmarks, Logic-VLA improves STL satisfaction rate over an STL-blind base policy by 24.8 to 40.7 percentage points (pp) while reducing nominal NL task success by at most 1.8 pp, showing that a single VLA can adapt its behavior to varying formal requirements without requiring a separate policy for each specification.

Many mainstream quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with staged reversible-operation bindings provide domain-level control spaces without exposing tag management. These bindings are eliminated by elaboration before Source typing. Granthi deterministically normalizes each Source program to a canonical wiring form. Every well-typed Source program, including a term of function type, has a unitary boundary interpretation. Under backend correctness (BC), the reference compiler produces a unitary circuit realizing that interpretation. Granthi's currently supported executable fragment is implemented end-to-end: an OCaml DSL elaborates surface programs through a higher-order Core IR to executable quantum circuits via pytket. The language directly supports the pure-unitary quantum switch for explicitly supplied operations; closed instances compile to static circuits. It also supports interference on control-flow history and structured finite control, all within the purely unitary fragment

Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. We evaluate ProofJudge on a novel dataset of 218 declarations drawn from distinct Mathlib PRs. The judge agent is grounded by tool access to the commit the PR is applied to, enabling it to query the library state when scoring. A judge is considered aligned with human preferences when it rates the version of the PR Mathlib accepted above the initial version that was sent back for revision. All six judge models evaluated recover the reviewers' preference well above chance, from 80.8% to 63.5%, and two open-weight judges reach roughly 70% at a tenth of the best judge's cost. We release the judge harness, evaluation dataset, and evaluation traces as open-source artifacts to support further research.

In this paper, we introduce the study of probability functions based on the 6-valued paradefinite (i.e., paraconsistent and paracomplete) logic LETK+. This logic is a powerful and versatile Logic of Evidence and Truth (LET) which is a conservative expansion of both classical logic and FDE. The framework introduced here allowed us to consider gaps, gluts, and reliability (or classicality) of the events, extending the detailed proposal for FDE-based probabilities presented by Klein, Majer, and Rafiee Rad. A distinctive feature of our proposal is the use of twist structure semantics, which gives rise to a natural interpretation of logical probabilities over LETK+ in terms of the three or six regions associated with each formula by a valuation in such models. The LETK+-probability functions are defined axiomatically and semantically, obtaining soundness and completeness results, as one would expect. Finally, conditional probabilities based on LETK+ are also studied. Specifically, both a semantic and a syntactic characterization of Jeffrey's update over LETK+-based probabilities is proposed, showing their equivalence.

Courcelle's theorem and its optimization variants yield fixed-parameter tractable algorithms for a wide range of graph problems on graphs of bounded treewidth or clique-width. However, the limited counting power of $\mathsf{CMSO}$ poses an obstacle to capturing certain optimization problems and properties within this framework. We introduce a new logic $\mathsf{AmCMSO}$, which extends $\mathsf{CMSO}$ with predicates for membership in the families of minimum- and maximum-cardinality sets satisfying a fixed formula $\phi(X)$. In contrast to most previous extensions of $\mathsf{CMSO}$ with cardinality constraints, we give algorithmic meta-theorems based on fixed-parameter tractable model checking for $\mathsf{AmCMSO}_1$ parameterized by clique-width and the formula, and for $\mathsf{AmCMSO}_2$ parameterized by treewidth and the formula. Our proof is based on the combination of Feferman–Vaught-type decomposition and fundamental techniques for dynamic programming. The meta-theorems yield fixed-parameter tractable algorithms for a wide range of optimization problems involving optimal solutions, including network interdiction, pre-assignment for solution uniquification, and diversity maximization, without parameterizing by the optimum value. Finally, allowing an optimality predicate to depend on even one external set variable makes model checking hard for every level of the polynomial hierarchy, already on trees of depth four.

Probabilistic shielding is a technique for safe reinforcement learning (RL). Typically, a static observer – called the shield – constrains the learning agent's actions to those for which acting safely remains feasible. Traditionally, the shield is computed from the transition probabilities of the underlying Markov decision process (MDP). Thus, this technique is not applicable when the MDP model is not given a priori, which, unfortunately, is the case in typical RL applications. In this paper, we study the problem of computing a shield in the setting where the transition graph of the MDP is known, but the transition probabilities are unknown. Our approach integrates probabilistic shielding with online model learning: as the RL agent explores the environment, we estimate the transition probabilities. From this estimate, we compute a shield. While the shield may be conservative initially, it adapts as the model estimate becomes more precise. Thus, the shield improves in tandem with the RL agent. This paradigm of adaptive probabilistic shielding raises a number of challenges, such as when to recompute the shield and how to balance between exploration and safety during learning. We empirically evaluate multiple variants of this paradigm across several environments.

In this paper we introduce Hippogriff, a language with a module system that unifies syntax between the core level and the module level. Hippogriff's type theory is dependent, with modularity features enabled via a universe of small types, but Hippogriff still supports general recursion without making typechecking nonterminating. This paper contains two halves. In the first half, we describe Hippogriff and its implementation. In the second half, we build categorical semantics for our use of dependent types that justify the use of general recursion at the value level. Specifically, we use an extension of the second-order generalized algebraic theory framework to include a synthetic phase distinction, and this allows us to make a mathematical connection between dependent type theories and split-context type theories (like System F). Included as supplements are a Haskell implementation of Hippogriff and an appendix describing the full type theory of Hippogriff using a second-order generalized algebraic theory with phase distinction.

We present a simple criterion for combining reduction pairs lexicographically. The criterion is applicable to arbitrary classes of reduction pairs, such as the polynomial interpretation, the matrix interpretation, and the Knuth-Bendix order. In addition, we investigate a variant of the matrix interpretation where the lexicographic order is employed instead of the usual component-wise order. Effectiveness is demonstrated by experiments and examples, including Touzet's Hydra Battle.

Decisions and their consequences can be described and analyzed by means of decision trees. The decisions themselves depend on questions that, whenever possible, should be answered with yes or no. The original BSS machines over the real numbers are graphs with computation nodes and branching nodes for decisions. The evaluation of BSS machines and algebraic decision trees in computer-aided geometry which have been introduced for various types of numbers generally involves the evaluation of systems of literals of first-order logic. Flowchart-like representations and decision trees are also helpful for analyzing decisions made by BSS RAMs over first-order structures. All algorithms defined by machine-oriented programs of BSS RAMs can be illustrated using flowcharts, walks, and paths in program trees. The basic structures of these tools are graphs and their visual representations can help to characterize the behavior of individual BSS RAMs and other first-order machines. We offer a theoretical framework for linking various models. Here, we introduce program paths and transition systems for transforming partial configurations which are defined syntactically and can be extended and refined later. Finally, we define standard orders for program paths and present algorithms for enumerating finite program paths.

This work introduces a formal semantic-block model for specifications and an execution-judged benchmark for evaluating specification quality independently of model capability. A specification is represented as a structure comprising semantic blocks, dependency relations, block-owned rules, decision points, and explicitly open questions, subject to four machine-checkable well-formedness conditions: acyclicity, single ownership, constraint domination, and totality or ambiguity-stop. Determinacy is defined model-theoretically as agreement among all conforming implementations and is estimated empirically through convergence across independent implementers. The model is instantiated on an Oracle-to-PostgreSQL migration specification containing 18 blocks and 19 dependency edges. Computational validation shows that the five-layer decomposition reduces mean per-task context by approximately 71% through dependency closures, covers 85.5% of the study-defined Oracle construct taxonomy with all identified gaps triaged, is not Pareto-dominated by the tested alternative partitions, and is recovered at the 99.9th percentile from citation-derived edges not used to define the original structure. The benchmark keeps the implementer panel fixed, includes a mandatory no-specification control arm, and uses PostgreSQL 16 and a live Oracle instance as deterministic execution judges. Six designed studies, including three pre-registered manipulations and three diagnostic analyses, further examine specification effects. Repeated runs on a 25-unit subsample reveal an empirical variability floor with a median arm-delta spread of 14.4 percentage points. The results support determinacy as a formal concept but not as a standalone empirical quality metric for the evaluated contemporary LLM implementers.

This document is the result of pulling together small parts of different lecture notes I have written over several decades for first-year graduate-level courses – typically with the title Formal Methods – which included many other topics of mathematical logic and theoretical computer science. After combining these materials, I updated the references and adjusted the text to account for progress accomplished in the intervening years. The sample of open problems in the last section is a small collection of special cases that are still unresolved up until the date of this writing.

Confluence guarantees that diverging rewrite choices can always be rejoined. For finite terminating string- and term-rewriting systems, confluence is decidable by critical-pair analysis, and in polynomial time for length-reducing strings. For finite terminating (hyper)graph transformation systems, in contrast, confluence is undecidable. We show that undecidability already appears for words on a circle, that is, strings up to rotation. Confluence of finite cycle-rewriting systems over the fixed alphabet $\{0,1\}$ is undecidable, indeed $\Pi^0_1$-complete, even when every rule has a nonempty right-hand side and strictly reduces length. Under this restriction termination is syntactically evident, and derivations from a nonempty length-$n$ cycle have fewer than $n$ steps. The same holds over every fixed alphabet with at least two letters, while the one-letter case is decidable. Rotation alone separates cyclic from string rewriting. The proof compiles a deterministic verifier into a weighted cycle system with one controlled branch, then into a binary length-reducing system via a run-length code whose cleanup rules send every reducible malformed cycle to one error normal form.

In the last years, a number of proofs of the fact that $O_2$ is a multiple context-free grammar (MCFG) were given. Such results can be exploited in the fields of both computational linguistics and of computational algebra. Here, we focus on a recent such proof spelled in terms of factorizations of string tuples, and give a new result with a stronger characterization of such factorizations than in existing theorems.

Mislove, Goubault and Varacca investigated how to define random variables in Domain theory to form monads over the category of bounded complete domains. They intended to model probabilistic programming languages with their random variables monads. In this paper, we focus on the random variables defined by Mislove from a topological perspective. We provide a topology for $\surd$-max continuous random variables on a $T_0$ space, we construct a new $T_0$ space, where $\surd$-max property is essential for the monad structures. We show that the spaces of normalized $\surd$-max simple random variables form a monad over the category of $T_0$ spaces and that the spaces of normalized $\surd$-max continuous random variables give a monad over the category of d-spaces. In addition, on a sober space, the space of normalized $\surd$-max continuous random variables is the sobrification of the space of normalized $\surd$-max simple random variables.

Tsetlin Machines (TMs) learn interpretable Boolean clauses using finite-state automata. We introduce the Quantum-Logic Tsetlin Machine (QL-TM), which replaces Boolean literals with quantum propositions represented by projectors while retaining classical include/exclude automata. Clauses are restricted to commuting measurement contexts and activate through the Born probability of their joint projector. We prove an exact reduction to ordinary Boolean TM clauses in diagonal computational-basis contexts and connect Pauli-projector clauses to stabilizer and syndrome semantics. Controlled experiments on Bell states, phase-flip syndromes, randomized 16-class stabilizer tasks, mixed literal pools, context-budget ablations, and finite-shot noise show that correct non-diagonal contexts recover physically meaningful clauses, while diagonal or wrong contexts lose the relevant phase/syndrome information. The context-budget results closely follow the predicted separability ladder 2^(b-k) as true stabilizer generators are removed. The contribution is a controlled bridge between Tsetlin clause learning and quantum logic, not a claim of quantum advantage.

The two-dimensional bandwidth minimization problem (2DBMP) seeks an injective embedding of a guest graph into a square grid that minimizes the maximum Manhattan distance over its edges. Heuristic methods can provide strong upper bounds, but these bounds do not by themselves certify optimality. We present an efficient exact SAT-based approach for 2DBMP that incrementally searches for the minimum feasible bandwidth and certifies optimality through satisfiability and unsatisfiability results. On the standard $\lceil\sqrt n\rceil \times \lceil\sqrt n\rceil$ host grid, under a 3600 s time limit, the proposed SAT approach certifies optimal bandwidths for 41 of 43 Regular instances and 42 of 93 Harwell–Boeing instances, achieving substantially broader optimality certification within the 3600 s time limit than a previous exact approach evaluated with a 72-hour time limit. In addition, it certifies three bandwidth values that improve all previously published comparison values considered in this study and establishes all three as optimal. We further evaluate the approach on alternative host geometries, namely $2\times\lceil n/2\rceil$ and $n\times n$ grids, to assess its effectiveness beyond the standard host. Overall, the results demonstrate that the proposed SAT approach provides an effective exact method for the small- and medium-sized benchmark instances considered in this study, with fewer than 400 vertices, while heuristic methods remain important for larger and more challenging instances.

We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions.

Robust Markov decision processes optimize one policy against a set of plausible transition functions. This can be conservative when the unknown dynamics are fixed and become partially identifiable after deployment. We study adaptive policy portfolios: finite sets of memoryless randomized policies synthesized offline and paired with a lightweight online selector. Robust regret is a natural measure of portfolio quality: for each plausible environment, it measures the loss of the best portfolio member relative to the policy that would have been optimal had that environment been known. Related regret objectives were studied by Ghavamzadeh et al. (2016) with an emphasis on approximations and relaxations for safe policy improvement. We give a complexity-theoretic account of portfolio certification and synthesis. Certifying a given portfolio is $\forall\mathbb{R}$-complete already for deterministic portfolios in acyclic (s,a)-rectangular RMDPs. Synthesizing a portfolio of unary-bounded size is $\exists\forall\mathbb{R}$-complete for general rational polytopes, even with fixed discount and acyclic dynamics. The single-policy case is already hard, both combinatorially and algebraically. Finally, we present an offline portfolio construction that is amenable to runtime specialization.

Erdős problem 647 asks whether any $n > 24$ satisfies $\max_{m<n}(m + \tau(m)) \le n + 2$, where $\tau$ is the divisor-count function. Computational searches have excluded solutions up to $10^{12}$ by direct sieve and up to roughly $9.17 \times 10^{18}$ within a modular reduction whose Lean component relies on native_decide; those computations sit outside any proof kernel. We give the first exclusion checked end to end by one: no solution exists with $24 < n \le 10^9$, proved in Lean 4 with axiom closure exactly {propext, Classical.choice, Quot.sound} – no sorry, no native_decide, no problem-specific axiom. The proof replays a chain of 6,685,922 factorization witnesses whose excluded intervals concatenate across $(24, 10^9]$; it needs no primality facts beyond primes below 1024, and it is the finite, fully proved form of a domination-interval argument whose asymptotic step was the identified gap in a withdrawn January 2026 claim on this problem. The generation pipeline is cross-checked by two further independent implementations, the compiled development replays through the standalone lean4checker, and two from-source verification legs – Lean toolchains compiled from source by gcc and by clang, mathlib rebuilt with no cache – reproduce the committed certificates byte for byte, with olean digests identical across three builds on two architectures. Our range is three to ten orders of magnitude below the computational frontiers we cite; the contribution is the trust base, not the range.

Grounded arithmetic is a family of formal systems for reasoning about computation in which a statement may be asserted only when a terminating computation backs it; the logics are paracomplete - for a sentence whose backing computation never settles, neither the sentence nor its negation is derivable, so paradoxes like the Liar are harmless rather than explosive. The reflective member of the family, RGA, can quantify over its own computations, but cannot certify that its own unbounded searches have definite yes-or-no answers. This paper studies what happens when that openness is closed by exactly one rule - ATI, the $\omega$-grounded universal: if every numeric instance of a universal sentence is certified decided, the universal is certified decided. The resulting system, OGA, shares RGA's syntax and rules symbol-for-symbol otherwise, and every consequence is developed as a machine-checked theorem. Decidedness certificates become abundant - every totality question about a computable function is certified to have an answer, whether or not anyone can produce it - and this is exactly the provable separation between the two systems. OGA is complete for its own semantics; certified-but-unresolved sentences receive values built from the system's own open questions. Provability remains recursively enumerable, with a primitive-recursive certificate checker, while $\omega$-truth deliberately is not. Within that asymmetry, incompleteness takes a new form. The Gödel sentence is classified, unconditionally, as a genuine fiction: neither provable nor refutable, yet valued, and carrying a computable pedigree recording exactly what adopting it as an axiom commits one to. The adoption is itself a theorem suite: extending OGA by any finite stock of true fictions is consistent, and independently certified adoptions can never collide.

Runtime Verification (RV) techniques are typically defined under the assumption of complete observability of system executions. In many realistic settings, however, monitors must operate under partial observability, where events may be lost, delayed, or unobservable. This raises fundamental questions about how to interpret specifications, verdicts, and uncertainty during monitoring. In this paper, we propose a new syntax and semantics for Probabilistic Trace Expressions (PTEs), a formal framework that integrates probabilistic reasoning into the operational semantics of Trace Expressions. Trace Expressions (TE) are a highly expressive specification formalism for runtime verification that we started to develop 15 years ago. Rather than attaching probabilities to syntactic transitions, as we did in the original formulation of PTEs dating back 2022, probabilities are now associated with the set of event types enabled in each semantic state, ensuring semantic consistency beyond finite-state models, and high modularity of the PTE specification. The PTE framework supports principled reasoning about missing events (gaps), distinguishes between observational and generative probabilistic interpretations – which represents a more refined semantics w.r.t. the original PTE formulation of 2022 – and subsumes classical probabilistic models such as Hidden Markov Models. We discuss how PTEs enable belief-based monitoring under uncertainty, illustrate their use in one representative Mars Rover scenario, and reflect on the conceptual implications for runtime verification in partially observable environments.

Graph Neural Networks (GNNs) have achieved remarkable performance in node classification tasks, motivating growing interest in methods capable of explaining their predictions. Recent logic-based approaches, such as LogicXGNN, derive global logical rules for Graph Neural Networks (GNNs) from collections of explanatory subgraphs. While informative, these subgraphs may contain redundant structural information that is specific to individual nodes, potentially limiting the generality of the extracted rules. In this work, we propose a logic-based framework for node classification in Simple Graph Convolution (SGC) networks that uses minimal abductive explanations as an intermediate representation for rule extraction. For each node, we compute a minimal set of node-feature pairs sufficient to preserve the predicted class. These explanations are then used to train decision trees from which global logical rules are extracted. Experiments on benchmark datasets show that the proposed framework produces compact global rules while maintaining high fidelity to the original SGC model.

Linear temporal logic is a modal extension of propositional logic that allows one to state how a system should behave over time. Its canonical domain is the booleans, but discretely-valued judgements are of little use in steering softly-valued systems (neural policies, adaptive controllers, sequence models, etc). In such cases, the goal formula's (dis)satisfaction becomes a training signal, and differentiability becomes a prime concern. Candidate differentiable semantics abound, but navigating them is tricky. Implementations, where available, are shallow embeddings, demanding an upfront commitment to a single semantic algebra and its (usually implicit) conduct. The paper casts the reader as a functional programmer asked to come to terms with this predicament, and refusing. Out of that refusal comes an evaluation engine that is algebra-generic and amenable to differentiation, together with an executable specification of the algebras it can accept. Various algebras are implemented and audited for their behavior, both forward and backward. Each algebra turns out to be a choice of which direction to disappoint, and how. Everything described (and more) is part of the PyTorch library telos, to be found at https://github.com/konstantinosKokos/telos.