ABSTRACT. This paper summarises seven papers published since 2016 with the aim of fostering collaboration towards a relatively unexplored goal: supporting the learning of mathematics by software at an early stage of learning, starting with the introduction of variables and ending up somewhere in academic engineering courses. The summary is self-contained and relatively brief, as it refers to the seven papers in which the technical details of the software are presented and discussed, in which related work is mentioned, and which contain many further references. As in many of the seven papers, also this summary starts from education considerations, the requirements arising from the practical teaching of mathematics in schools and at university. These requirements determine the technology implemented in the project Isabelle/MAWEN which is the central point in this summary.

ABSTRACT. Isabelle is a powerful generic proof assistant, usable with many different object logics. Its most common incarnation is with Higher-Order Logic (HOL) as Isabelle/HOL, where it offers powerful proof automation (among a plethora of other features). Ordinarily, this is a strong advantage of Isabelle. But it presents a challenge for teaching its use: powerful automation can easily obscure the basic underlying mechanics of the proof assistant, and thus lead beginner’s understanding astray. Likewise, Isabelle’s version of HOL has evolved significantly compared to Gordon’s original formulation, and a conventional introduction to Gordon’s HOL in a course about Isabelle can easily raise more questions than it will answer. To address both these issues, we introduce MiniHOL, a smaller, readable-for-beginners version of the object logic implemented in Isabelle/HOL’s actual HOL.thy & friends, and report on its use in the introductory theorem proving course on Isabelle/HOL held in the winter semester 2025/2026.

ABSTRACT. We present a tool for teaching classical propositional logic using the sequent calculus. The tool is a concise formalization in the Isabelle proof assistant. The formalization shows that the proof system is sound and complete. The tool has been used for several years as a gentle introduction to propositional logic and automated reasoning in courses for computer science students.

ABSTRACT. We present a methodology for designing SAT encodings of integer multiplication guided by proof trace analysis. By examining DRAT proofs, we identify structural bottlenecks—the top bottleneck variable in standard Comba encoding appears in 31% of all proof steps—and use these findings to redesign the encoding. This methodology produced comba-cs, a carry-save Comba encoding that separates column reduction from carry propagation, achieving 2.6–71× speedup across four SAT solvers. We further show that carry propagation is the dominant driver of SAT hardness for multiplication—not merely correlated with it. A controlled experiment holds the partial-product layout and accumulation topology fixed and varies only the accumulator (integer addition vs. GF(2) XOR): integer commutativity is at least 1000× harder than GF(2) at bitwidth 12, and structural variations (sequential vs. parallel-tree accumulation) change running time by less than 5×. This establishes causation for the commutativity pattern on CaDiCaL. Comparing comba-cs with pre-existing alternative encodings (Booth radix-4, 4-bit blocks, sorting networks), we find that no single encoding dominates: Booth is 17× faster on strength-reduction benchmarks, while comba-cs is 2× faster on bfloat16 commutativity. The optimal encoding depends on problem structure, motivating adaptive selection.

ABSTRACT. Cardinality constraints in Boolean satisfiability (SAT) problems are typically encoded as sets of clauses in conjunctive normal form, which serves as the standard input format of SAT solvers. The ordering of data variables within a cardinality constraint can have a substantial impact on the quality of the resulting encoding and on solver performance, motivating the development of various pre-processing and reordering techniques. In this work, we address the scenario in which a cardinality constraint has already been encoded into clauses. We introduce a proof-producing reencoding method that systematically transforms an existing encoding into a new encoding with reordered data variables, while producing a certificate that establishes satisfiability equivalence between the original and transformed formulas. To illustrate the practical advantages of our approach, we evaluate it using a family of vertex cover benchmarks specifically designed with adversarial variable orderings.

ABSTRACT. In modern combinatorial solving and automated reasoning systems, proof logging and checking is a highly effective way to provide trust in solver outputs. For Boolean satisfiability (SAT), a technique called proof trimming is vital to allow rapid proof checking and reduce the size of stored proofs. However, trimming remains a challenge for richer proof systems. In this work, we design, implement, and evaluate a proof trimmer for the VeriPB proof format, bringing the advantages of trimming to a wide range of certifying solvers, including those for pseudo Boolean optimisation, MaxSAT, constraint programming, and subgraph solving, and for SAT solvers that use techniques like symmetry or cardinality reasoning. We describe and justify the overall architecture of our system, and give details of how the more challenging proof rules are handled. Our experiments demonstrate large reductions in proof size, without compromising correctness, as well as significant speedups for proof checking including formally verified checking.

ABSTRACT. We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4. Key to our approach is REFLECTION: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code. Our method scales to proofs with tens of thousands of steps that would exhaust memory under explicit proof-term construction. Our checker parses all \veripb kernel rule types and verifies unsatisfiability via cutting-plane derivations, proof-by-contradiction subproofs, and redundance/dominance for symmetry breaking; soundness is established in Lean for the rules used along the UNSAT path. In contrast to external verified checkers that produce verdicts, our integration yields Lean theorems that can serve as composable lemmas in larger formal developments. To derive theorems about the original combinatorial problems rather than about PB constraints alone, we support verified encodings. This closes the trust gap between solver output and problem semantics since the constraint translation and its correctness proof are both formalized in Lean. We demonstrate the approach on various combinatorial problems.

ABSTRACT. Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZKUNSAT, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZKUNSAT demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability. Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZkUnsat without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZkUnsat on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.

ABSTRACT. Passive learning of formal models from observed system behavior has produced a rich body of results for sequential computational models. Extending this success to concurrent systems poses fundamental new challenges: concurrent models are more succinct, often lack a unique minimal representative, and their semantics depends on the interplay of multiple simultaneous processes. A common restriction in prior work on learning of concurrent models is the assumption of a fixed, known number of processes---an assumption that is fundamentally at odds with parametrized systems, which are designed to operate correctly for any number of processes. We summarize our recent work on passive learning of broadcast protocols (BPs), a well-studied model of parametrized concurrent systems. For the class of fine BPs--BPs with no hidden state and a finite cutoff--we establish a comprehensive learnability picture: a constraint-based passive learning algorithm that infers a BP consistent with a given sample, returning a minimal equivalent BP when the sample subsumes a characteristic set; hardness results showing that consistency is NP-complete, that characteristic set may be exponentially large, and that fine BPs are not polynomially predictable; along side LeoParDS, the first tool implementing theses techniques in the parametrized setting.

ABSTRACT. We present TPTND-Lean, a Lean 4 implementation of a core fragment of Trustworthy Probabilistic Typed Natural Deduction (TPTND). TPTND-Lean type-checks TPTND derivation trees whose leaves are empirical observations, and whose internal nodes are introduction or elimination rules for probabilistic connectives, producing machine-checked fairness certificates. In this implementation, frequencies and stored interval endpoints are rational numbers; the standard-error term used by the score-test acceptance bands is computed via a bounded-rational Newton iteration. The kernel is small and auditable; each derivation it accepts is a transferable, re-checkable certificate that binds together counts, statistical test, band, and verdict in a single typed tree. We describe a four-stage workflow that takes group-level summary statistics through claim selection and derivation construction to such a certificate. Two case studies on public data illustrate the approach: (i) the ProPublica COMPAS recidivism data (6172 defendants, reproducing the headline racial-bias finding), and (ii) HMDA mortgage-lending data for Delaware (54000 Black/White applications across 2022-2023, demonstrating multi-year temporal composition via Update and intersectional comparisons). Certificates are conditional: they verify the derivation relative to the supplied counts, the chosen statistical rule, and the checker, not the upstream data pipeline. The full source, data pipelines, and all derivations are publicly available at https://github.com/dasaro/tptnd-lean.

ABSTRACT. The Relativity of Causal Knowledge (RCK) explains how agents with different structural causal models can exchange causal knowledge through a shared interventionally consistent abstraction, or backbone. We ask the prior identification question that this transport mechanism presupposes: when is that backbone determined by the agents' private causal knowledge? In the basic two-agent common-effect, case, two private causes influence one shared outcome and each agent identifies only the single-cause causal marginal relevant to its own perspective. We show that, under standard compatibility, non-degeneracy, and local overlap assumptions, those local causal marginals do not identify a unique edge-level backbone. Infinitely many joint intervention kernels can induce exactly the same private reports while disagreeing on joint interventions. The obstruction is therefore not in defining RCK restriction or extension maps once an edge value is fixed; it is in identifying the common edge value to which those maps should apply. We then give a conditional recovery result. Additive separability removes the hidden interaction degree of freedom, but observational residual summaries remain insufficient. Identification becomes possible when agents communicate causally identified response functions. An education value-added example illustrates why this is first a communication problem, and only then a policy-composition problem.

ABSTRACT. A core challenge for real-world agents is determining which aspects of a decision problem are most relevant – that is, deciding what to pay attention to. Salience profoundly influences human decision-making, often leading to choices that diverge from normative rationality. In this extended abstract, we sketch a formal model that captures how salience modulates preferences and drives changes in preference. We provide a representation theorem characterising preference relations shaped by salience-weighted features. This framework provides a mathematical starting point for studying preference change under attentional modulation and for designing systems that can effectively guide human decision-making in complex, multi-faceted environments. At the same time, we highlight important considerations about the responsible design of influence strategies, particularly in contexts where subtle preference shaping may have unintended or harmful consequences.

ABSTRACT. Robots are increasingly being used in different application domains, aided in large part by the deep networks and foundation models that are now considered to be state of the art for many problems in AI and robotics. However, these methods and models are resource-hungry and opaque, and they provide arbitrary decisions in previously unknown situations, whereas practical applications often require transparent, multi-step, multi-level decision-making and collaboration under resource constraints and open world uncertainty. I argue that to leverage the full potential of AI in robotics, we need to revisit fundamental principles such as abstraction, ecological rationality, interactive learning and explainable agency, which can be traced back to the work of the early pioneers of AI. I would like to describe how we can combine the complementary strengths of knowledge-based and data-driven methods for reasoning and learning by embedding these principles in architectures developed for robots.

ABSTRACT. Restricted non-deterministic matrices (RNmatrices) impose constraints on the rows of non-deterministic matrices, filtering out "unsound" rows and retaining only "valid" ones. This yields a more expressive framework than standard NMatrices. Although this approach enables sound and complete semantics for a broad class of logics, eg, paraconsistent logics, propositional intuitionistic logic, and the fifteen normal modal logics of the modal cube, no efficient decision procedures based on these semantics have been proposed. In this paper, we implement the RNmatrix framework to develop a new suite of automated theorem provers for these logics. By encoding RNmatrices and their elimination criteria as Satisfiability Modulo Theories (SMT) problems, we leverage SMT solvers to decide formula validity and construct countermodels. We illustrate the method for paraconsistent logics, where our prover outperforms the current state-of-the-art and provides the first implementation for the entire C_n hierarchy, as well as for intuitionistic and modal logics, where our general-purpose framework achieves competitive performance.

ABSTRACT. Expansion-based QBF solvers decide false instances by partially expanding universal variables, yielding a formula in conjunctive normal form (CNF) that can be directly refuted by a SAT solver. This approach is captured by the $\forall\text{Exp+Res}$ proof system, and certification frameworks for false QBFs have previously been presented. For true instances, the dual approach of existential expansion is less well studied. Partially expanding existential variables yields a disjunction of CNFs containing universal variables, which is not in CNF and thus cannot be passed directly to a SAT solver. Certifying true results has therefore remained an open problem. We present a proof format and checking algorithm for certifying true QBFs in the expansion-based setting, identifying and overcoming the core obstacles introduced by the necessary CNF transformation.

ABSTRACT. Almost 40 years ago, the 2-player game Connect Four was proven to be a first player win. 20 years ago, the Boolean Satisfiability community was challenged to confirm this fact by leveraging Quantified Boolean Formula techniques and associated technology. While a logic-based proof remains out of reach, several barriers have been crossed in the last few years. We report on recent progress and contrast the situation today with what it was when the challenge was first posed.

ABSTRACT. The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively by iterating between a decision oracle used for extracting sources of inconsistency and an optimizer for computing so-called hitting sets (HSs) over the accumulated sources of inconsistency. While the decision oracle is language-specific, the optimizer is usually instantiated through an (often commercial, closed-source) integer programming (IP) solver. This makes proof logging in implicit hitting set solvers challenging. Moreover, IP solvers are known to give incorrect results, mostly due to numerical instability. The presented work deals with obtaining reliable hitting set computation in the context of pseudo-Boolean (0--1 IP) optimization. We explore alternative algorithmic techniques for hitting set optimization based on different ways of employing pseudo-Boolean reasoning as well as stochastic local search. Based on earlier work on proof logging for pseudo-Boolean solving using the VeriPB proof system, we obtain the first implicit hitting set solver that is able to produce proofs of optimality of its solution. Our experimental evaluation highlights a trade-off between efficiency and reliability: replacing a commercial IP solver with a pseudo-Boolean solver enhances reliability and gives proof logging possibilities, at the cost of solving efficiency. To mitigate this trade-off, we experimented with different hybrid approaches that differ in when to replace the IP solver by a more reliable, certifying solver.

ABSTRACT. Modern combinatorial solvers are very efficient but also highly complex and therefore error-prone. The most successful approach to ensure correctness is proof logging, now an accepted standard for Boolean satisfiability~(SAT) solving, where solvers emit a machine-verifiable certificate alongside each result. An important technique to make formally verified proof checking efficient is proof trimming: starting from the final verdict and reading the proof backwards, a checker retains only those steps that actually contribute to the conclusion, discarding the rest. Trimming for richer proof systems beyond SAT, however, remains a challenge. In this presentation, we introduce the first trimmer for the full VeriPB proof system, which uses 0-1 integer linear inequalities and enables certification of correctness for a broad range of combinatorial paradigms, including MaxSAT, pseudo-Boolean optimisation, subgraph solving, and constraint programming. Trimming pseudo-Boolean proofs is significantly harder than trimming clausal SAT proofs. For instance, constraints are not always listed explicitly (cutting planes derivations specify how a constraint is derived, but not what it looks like); proof line deletion can be restricted by the proof format; and the redundance-based strengthening rule induces global proof dependencies that can propagate during the backwards pass. Our algorithm proceeds in three passes. A lightweight decoration pass makes implicit proof information explicit, enabling a subsequent backward trimming pass to identify necessary constraints. A final compaction pass writes the trimmed proof. The central novelty is conditional marking: rather than immediately deciding which constraints to keep, the trimmer collects deferred conditions of the form "if C is ultimately needed, then D must be kept too", resolving them lazily at the end of the backwards pass. This cleanly handles the cascading dependencies introduced by strengthening rules without over-approximating the set of required constraints. We evaluate our trimmer on 2656 proof files generated by six solvers, covering SAT solving with symmetry breaking, MaxSAT, pseudo-Boolean optimisation, subgraph solving, and constraint programming. The results demonstrate a 6.37x reduction in proof size and a 1.81x speedup in total checking time, including the overhead of formally verified checking via CakePB. The benefits are particularly pronounced for constraint programming and pseudo-Boolean optimisation proofs, which shrink by factors of 17 and 11 respectively. These results invite further refinement: the marking heuristics used during unit propagation steps are currently using marked propagation first and trail saving. Better strategies (for instance, preferring earlier or stronger constraints, or those with explicit derivations) could yield tighter trimmed proofs. For applications such as proof storage or UNSAT core extraction, one may wish to trade trimming speed for proof minimality, and we discuss the cost-quality tradeoffs that arise in this setting.

ABSTRACT. Modern proof systems for SAT are based on redundancy notions, which ascertain that clauses are safe to derive through a check involving the whole formula currently held by the solver. This global dependency phenomenon, called interference, presents fundamental issues in proof logging within distributed and incremental settings. Recent work leveraged a close connection between redundancy notions and propositional dynamic logic to propose a logical framework that eliminates the issues posed by interference in unsatisfiability proofs. Proofs in this framework, called dynamic proofs, are freely composable, a feature theretofore missing in state-of-the-art proof systems such as DRAT. However, composability is attained by only allowing implicational proofs, which ostensibly forgoes reasoning about satisfiability, a capability required to capture incremental SAT solving. In this work, we overcome this limitation by showing that dynamic proofs can also witness satisfiability without losing composability; in fact, this can be done without augmenting the framework with new rules. To showcase the expressivity of this proof framework, we provide proofs capturing equisatisfiability in models of both incremental and non-incremental SAT. Furthermore, we present an extension through solution programs. With this extension, proofs of equioptimality can be captured as well.

ABSTRACT. In this talk we introduce the type-2 analogue of \textsf{FLOGSPACE}, defined through oracle Turing machines, answering a question raised by Kawamura. We show that this class, dubbed \emph{Easy Feasible Functionals} (\textsf{EFF}) is robust, being closed by both type-0 and type-1 composition.

ABSTRACT. Solver-independent modelling languages such as MiniZinc are widely used because they enable rapid prototyping of complex optimisation models without committing to a particular solver technology. However, when using a fixed constraint programming solver, one can extend it with custom problem-specific propagators. This can potentially achieve significantly stronger propagation and improved performance. In contrast, within a solver-independent framework, such constraints are typically expressed through decompositions into simpler primitives, which may weaken propagation and increase runtime. This paper presents an extension to MiniZinc that enables specifying custom propagators directly at the modelling level. These propagators are executed via solver callbacks, preserving solver independence while enabling specialised propagation. Beyond modelling-level propagators, our framework enables the integration of externally implemented propagators, making it possible to incorporate propagation for complex black-box functions, such as simulation models. We demonstrate that this enables the rapid development of efficient problem-specific propagators and facilitates hybrid white-box/black-box optimisation approaches.

ABSTRACT. The minimum-distance constraint min_distance(D, x, z) links selected-point variables x with a variable z denoting the smallest distance between any selected pair. A direct CP encoding introduces one auxiliary distance variable per pair and then constrains the objective to be the minimum of those variables. This encoding is clear and portable, but it also creates a quadratic family of variables and propagators. It can also spend memory representing holes in auxiliary distance domains, even when branch-and-bound only needs useful (lower) bounds on the minimum distance. This paper studies propagation algorithms for the minimum-distance constraint in Gecode. The implemented variants include pairwise propagators, a global support scan, advisor-backed support maintenance, and a matching-based upper-bound propagator. A motivating example for studying these algorithms is p-dispersion with distance constraints, where the minimum-distance constraint is central and pair-specific lower-bound thresholds are part of the model. Preliminary benchmarks on p-dispersion instances from the literature indicate that direct propagation of this constraint can reduce decomposition overhead, but the experiments should be read as an implementation study rather than a complete p-dispersion solver comparison. The organisation of the propagator is important: full global scans can be too expensive, advisor-backed incremental state maintenance and matching-based bounds help on the indexed model, and pairwise bounds remain a strong baseline.

ABSTRACT. Interactive Constraint Acquisition (CA) can assist in modeling constraint problems by acquiring constraints through a query-based interaction with the user. However, existing methods often require a large number of queries. We aim to address this limitation by introducing constraint-specification-based generalization queries, which lift individual learned constraints to higher-level specifications that capture entire sets of constraints at once. We then propose \gqgen, a machine learning-based method to extract such specifications from the learned and excluded constraints during the acquisition process and show how it can be integrated directly within any existing interactive CA algorithm. Our experiments show that our proposed approach reduces the number of queries substantially (by up to 95%), while our user study demonstrates that LLM-based natural language formulations of our generalization queries are understandable to users.

ABSTRACT. Paramita is a Python framework that provides a unified, plugin-based interface for interacting with external tools from the Satisfaibility domain (e.g. SAT and MaxSAT solvers). These tools can be implemented in C++ or Python. The framework follows a strict separation between interface definitions and concrete implementations. Solvers and encoders in C++ are compiled as shared libraries and loaded at runtime. Solvers implementing IPASIR, IPASIR-UP and IPAMIR C++ interfaces can be directly integrated in Paramita with almost no effort. Paramita also supports a higher level modelling language for Non-CNF formulas, extendend with PB constraints and linear objective functions. Paramita is suitable for a wide range of combinatorial optimization and satisfiability tasks. This paper describes the architecture, solver and interfaces provided by the framework, the modelling language and other features.

ABSTRACT. We study when a sound arithmetic theory $\mathcal S{\supseteq}S^1_2$ with polynomial-time decidable axioms efficiently proves the bounded consistency statements $Con_{\mathcal S{+}\phi}(n)$ for a true sentence $\phi$. Equivalently, we ask when $\mathcal S$, viewed as a proof system, simulates $\mathcal S{+}\phi$. The paper's two unconditional contributions constrain possible characterizations. First, for finitely axiomatized sequential $\mathcal S$, if $EA{\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}\phi}$, then $\mathcal S$ interprets $\mathcal S{+}\phi$, implying $\mathcal S{\sststile{}{n^{O(1)}}}Con_{\mathcal S}(p(n)){\rightarrow}Con_{\mathcal S{+}\phi}(n)$ for some polynomial $p$, and hence $\mathcal S{\sststile{}{n^{O(1)}}}Con_{\mathcal S{+}\phi}(n)$. Second, if $\mathcal S$ fails to simulate $\mathcal S{+}\phi$ for some true $\phi$, then for all sufficiently large $k$ it also fails for $\phi_{BB}(k)$ asserting the exact value of the $k$-state Busy Beaver function. Informally, any argument showing that $\mathcal S$ fails to simulate some $\mathcal S{+}\phi$ also yields unprovable $\phi_{BB}(k)$ witnessing the same obstruction. These results suggest that relative consistency strength is a serious candidate for governing when simulation is possible, while leaving open whether it is the correct criterion. The paper's central conjectural proposal is that the above sufficient condition is also necessary: if $EA{\not\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}\phi}$, then for every constant $c{>}0$, $\mathcal S\centernot{\sststile{}{n^c}}Con_{\mathcal S{+}\phi}(n)$. Under this proposal, hardness follows in canonical cases where $\phi$ is $Con_{\mathcal S}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.

ABSTRACT. Cook introduced the equational theory PV, whose terms are exactly the polynomial-time functions, to capture the notion of feasibly constructive proofs. Our aim is to develop a 'positive' version of PV which we call posPV, where the terms are the positive polynomial-time functions, that is, the functions computable in polynomial time without using negations. This is a continuation of previous work on uniform monotone complexity, in particular building on a Cobham style characterisation of the positive polynomial functions. We seek to build a framework analogous to that of Cook by providing a polynomial-size translation of posPV proofs into a propositional proof system, and proving that posPV proves the reflection principle for this language.

ABSTRACT. LLMs and their capabilities to handle natural language are more and more used as an intuitive interface between non-experts users and complex algorithms. This is facilitated by the recent introduction of the Model Context Protocol (MCP). In this work, the LLMs facilitate the use of explanation algorithms by translating back their outputs into natural language adapted to the user.

ABSTRACT. Minimal Unsatisfiable Subsets are often used as a method for explaining why a CSP is unsatisfiable. While the meaning of each constraint in an MUS can be made clearer using a natural language description, the interaction between constraints can make it non-trivial to understand why an MUS is unsatisfiable. We investigate the use of Large Language Models (LLMs) for producing natural language explanations of unsatisfiable CSPs, similar to the example shown. More specifically, we are interested in a concise explanation of why a Constraint Satisfaction Problem (CSP) is unsatisfiable that is both sound and complete.

ABSTRACT. We introduce a novel semantic framework for Linear Temporal Logic over finite traces ($\mathrm{LTL}_f$) that interprets formulas via $\mathit{sl}$-truth on FM-domains, capturing a finitistic truth-in-the-limit notion over increasingly large temporal models. We complement this semantic foundation with a sound and complete proof-theoretic calculus, enabling formal derivations under the new semantics. Using these tools, we formalize several Yablo-type sentences in temporal logic and examine their behavior. Our analysis shows that all principal Yablo variants (including "always", "sometimes", "almost-always", and "unboundedly-often" sentences) are satisfiable in $\mathrm{LTL}_f$ models, so that no genuine paradox arises in the finite-trace setting. Moreover, in the limit semantics one finds that key Yablo formulas become stably true: for example, the unboundedly-often Yablo sentence holds in all sufficiently long finite traces (i.e., it belongs to the $\mathit{sl}$-theory of the class of all finite traces). These results imply that deep nesting of beliefs in temporal interactions is well-founded, avoiding paradoxical loops when agents operate in bounded time domains.

ABSTRACT. Rational synthesis and rational verification study temporal properties of multi-agent systems with strategic agents. Existing procedures focus on existence. They return equilibrium outcomes, but these outcomes can be unnecessarily long and hard to inspect. We introduce Minimal Rational Synthesis (MRS), a procedure for extracting shortest ultimately periodic equilibrium witnesses from the finite automata–game products used in rational synthesis and rational verification. MRS does not change the underlying equilibrium notions. Instead, it optimises witness extraction after the standard rational verification construction has fixed the relevant winner sets, payoff vectors, and punishment conditions. Our method combines exact shortest-lasso search with automata and product reductions, and may output auxiliary certificates containing on-path actions and punishment information. We implement the approach in EVE for the LTL–LTL, GR(1)– LTL, and GR(1)–GR(1) settings, and report initial experiments showing shorter witnesses and fewer brute-force timeouts on the considered benchmarks.

ABSTRACT. We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.

ABSTRACT. We study synthesis for obligation properties expressed in LTLf+, the extension of LTLf to infinite traces. Obligation properties are positive Boolean combinations of safety and guarantee (co-safety) properties and form the second level of the temporal hierarchy of Manna and Pnueli. Although obligation properties are expressed over infinite traces, they retain most of the simplicity of LTLf. In particular, we show that they admit a translation into symbolically represented deterministic weak automata (DWA) obtained directly from the symbolic deterministic finite automata (DFA) for the underlying LTLf properties on trace prefixes. We show that synthesis for LTLf+ obligation properties is theoretically highly efficient -- solvable in linear time once the DWA is constructed. We investigate several symbolic algorithms for solving DWA games that arise in the synthesis of obligation properties and evaluate their effectiveness experimentally. Overall, the results indicate that synthesis for LTLf+ obligation properties can be performed with virtually the same effectiveness as LTLf synthesis.

ABSTRACT. The advancement of linear logic has witnessed its core ideas being woven into various forms of type theory, such as System F and dependent type theory. To provide general semantics for these systems, categorical structures have been proposed: linear hyperdoctrines in the case of System F and linear comprehension categories in the case of linear dependent type theory. These notions bear a fundamental similarity in that they are variations on linear-non-linear (LNL) adjunctions. In this work, we make these similarities precise. Specifically, we define a general notion of linear-non-linear adjunction that unifies categorical semantics of different linear type theories. The general notion is a reformulation of the familiar notion internal to 2-categories with finite products. We recover the familiar notion when the ambient 2-category is that of categories, functors and natural transformations. We show that LNL adjunctions are preserved by pseudofunctors that preserve finite products. This gives a method for constructing models of complex linear type theories from simpler models, reducing the workload in individual cases. To substantiate this claim, we show how various concrete models of linear type theories can be obtained via externalization of internal categories.

ABSTRACT. Differential lambda-calculus is an extension of lambda-calculus which enables one to treat differentiation of analytic functions purely syntactically. Just as simply typed lambda-calculus is sound and complete with respect to Cartesian closed categories by the Curry-Howard-Lambek correspondence, simply typed differential lambda-calculus is sound and complete with respect to Cartesian (closed) differential categories. Cockett and Gallagher refined these ideas to provide a categorical semantics of the untyped differential lambda-calculus, introducing the Cartesian differential Turing category with differential canonical codes. This coherently combined a Cartesian differential category with a type of category that provides a sound and complete semantics for the ordinary untyped lambda-calculus: a Turing category with canonical codes. Now, an important source of examples of Cartesian differential categories comes from the categorical semantics of differential linear logic: monoidal differential categories. Briefly, a monoidal differential category is a symmetric monoidal category with a comonad ! and a natural isomorphism d_A : !A \otimes A \to !A, called the deriving transformation, that satisfies certain coherences that capture the fundamental properties of differentiation, like the product rule and chain rule. The coKleisli category of a monoidal differential category is a Cartesian differential category. It is then natural to ask what is the analogue of a monoidal differential category whose coKleisli is a Cartesian differential Turing category. We solve this problem in two stages. First, we define a type of linear category called the linear Turing category (with canonical codes): a linear analogue of the ordinary Turing category (with canonical codes). We show that the coKleisli category of a linear Turing category is an ordinary Turing category. Further, we provide a sufficient condition for its coEilenberg-Moore category to be an ordinary Turing category. Second, we define a monoidal differential Turing category: a linear Turing category with a differential category structure. We show that that this category is the solution to our question. That is, we show that the coKleisli category of a monoidal differential Turing category with additive canonical codes is indeed a Cartesian differential Turing category with differential canonical codes. We also show that this is the unique solution and provide an example of a monoidal differential Turing category: the category of computably enumerable relations.

ABSTRACT. Runtime Monitoring (RM) enables the automated and objective evaluation of a system w.r.t its system specification. In the automotive domain, RM allows for the evaluation of whether a vehicle's actual behaviour corresponds to an abstract specification of its expected behaviour while interacting inside a traffic scenario. Such runtime monitors, in the automotive domain, must not only consider spatial aspects such as distances, positions, velocities, etc., but also temporal aspects such as the order in which particular traffic situations (or scenarios) occur. Existing runtime monitors provide verdicts on whether the actual vehicle behaviour corresponds to the abstract scenario specification, with possible outcomes being satisfied, violated, or inconclusive. Undesired behavior is detected whenever there is a discrepancy between the monitor's verdict and the expected outcome defined by the scenario specification. Tracing the cause for the undesired behaviour requires knowledge of prior system behaviour. This information can be derived from exact knowledge of the intermediate verdicts of the runtime monitor, the so called monitor progression. This is not trivial to determine because the current satisfied constraints may simultaneously correspond to multiple (traffic) situations. Additionally, the satisfaction of temporal properties also depends on prior spatial and temporal properties. To improve the analysis of unexpected system behaviours, we propose progress-aware RM of abstract scenario specifications. Specifically, we introduce hypercuts to describe all non-violating past and future system behaviors, simplifying the analysis of unexpected verdicts. Each monitor verdict is annotated with a hypercut, which allows the samples to be related back to the abstract scenario specification structure. In this work, we provide a well-defined hypercut using Duration Calculus and describe the construction of a progress-aware runtime monitor, based on Traffic Sequence Chart (TSC) monitoring. Finally, we demonstrate how hypercuts improve the analysis of unexpected verdicts through an application example and present a visualization method.

ABSTRACT. Although the integration of machine learning into safety‑critical systems is growing, a fundamental tension remains: performance‑oriented techniques such as parallelism and optimized execution can introduce opacity and nondeterminism, while safety‑critical systems demand transparency and reproducibility. This paper provides a formalization of ONNX computation graphs that addresses these requirements by focusing on the abstract modeling and verification of graph‑based machine learning representations. The proposed workflow, developed within the SONNX initiative, combines the exploration and validation of structural properties of the graph using the Alloy Analyzer — used to explore and validate structural properties via model checking — with a subsequent refinement of the model in the Why3 verifier, enabling deductive reasoning over type invariants and functional properties. We further introduce an execution semantics for the graph model, defined as a state machine where graph configurations correspond to states and node execution induces state transitions. Overall, our proposed model is thus defined as a set of well-formed graph configurations equipped with a single-rule, transition relation.

ABSTRACT. For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components—a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle—a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.

ABSTRACT. We extend the Dafny system with an interactive proof mode. We present how the interactive proof mode can be used on a motivating example, we discuss the underlying architecture of the system, and provide a prototype implementation.

ABSTRACT. This work investigates resource improvements for probabilistic lazy PCF, a simply typed, higher-order call-by-need functional language with natural numbers, branching, fixpoints, and probabilistic choice. Building on deterministic improvement theory, a contextual cost improvement preorder is defined, requiring semantic equivalence and non-increasing expected reduction steps in all contexts. To avoid context quantification, distribution-cost improvement is introduced as an intrinsic preorder that compares per-value conditional expected steps. The main result establishes that both preorders coincide for closed programs of number type. This extends the distribution-equivalence characterisation to the resource-sensitive setting and enables local, context-free improvement proofs. As applications, garbage collection and a surface unique-copying transformation are verified as cost improvements, while deterministic common subexpression elimination is conjectured to exhibit the same property.

ABSTRACT. Trace logic is an expressive formalism for specifying the step-wise behaviors of recursive programs using state predicates, binary relations, sequential composition, and fixed points. By characterizing a program via its strongest trace formula, verification is reduced to checking the validity of trace formula implications. However, existing proof systems for trace logic are limited to finite traces and rely on explicit fixed-point induction rules, which pose challenges for automated proof search since invariants must be explicitly provided. In this work, we extend trace logic with greatest fixed points to express infinite, reactive behaviors. Furthermore, we propose a cyclic proof system for checking trace formula implications in this extended logic. By representing inductive and co-inductive reasoning as cyclic structures within the proof derivation, our system reduces the need for explicit invariants. Finally, we formally establish the soundness of our proposed system.

ABSTRACT. We study rewriting for measurement-bearing expressions whose measured leaves carry both bounded uncertainty and observation-token identity. A token-sensitive enclosure semantics assigns each expression its warranted enclosure—the set of values realizable by token-consistent hidden-value environments. Over that denotational core we define two rewrite judgments mechanized in Lean 4: RewritesTo for sound one-way claim tightening via enclosure containment, and Interchangeable for genuine equivalence via enclosure equality. The checked development establishes three compact classification results: same-token cancellation, shared-background subtraction, and same-token self-division over positive intervals are interchangeable with their simplified forms, while the corresponding distinct-token variants support only one-way tightening. Its main negative result is that provenance-blind summaries—even ones that preserve intervals, dimensions, and syntax modulo token erasure—cannot in general recover the correct rewrite class. We also show that on the exact fragment both rewrite judgments collapse to ordinary equality of exact denotations. All stated results are sorry-free in Lean 4.

ABSTRACT. Many techniques have been developed to explain logical reasoning, such as proofs or abduction. However, such methods are useful mainly for experts in logic, e.g., for debugging ontologies. For actually explaining logical consequences and missing consequences to end users of logic-based systems, e.g., in the Semantic Web, it is necessary to study how to adapt and present such explanations in an understandable way. We report on a series of user studies investigating both entailment explanations via proofs and missing entailment explanations via abduction and counterexamples in the context of Description Logic (DL) ontologies. For the former, we assess the influence of prior knowledge on the necessary explanation granularity; for the latter, we compare the efficacy of abductive versus counterexample-based approaches. While we did not find objectively quantifiable results, we analyse and discuss the results of detailed qualitative user interviews, and extract recommendations for executing user studies on logical reasoning systems.

ABSTRACT. This abstract is for a paper published in 2025 in the proceedings of the 14th International Joint Conference on Natural Language Processing and the 4th Conference of the Asia-Pacific Chapter of the Association for Computational Linguistics, and we extend it here with a new study that closes the gap with previous research. Large language models (LLMs) are increasingly applied in domains that demand reliable and interpretable reasoning. While formal reasoning methods can generate correct proofs, these proofs are often inaccessible to non-expert users. This raises a natural question: Can LLMs, when given a proof, faithfully interpret its reasoning and communicate it clearly? Recently, we have introduced \texttt{ProofTeller}, a benchmark that evaluates this ability across three tasks: (1) identifying key proof steps, (2) summarizing the reasoning, and (3) explaining the result in concise natural language. The benchmark covers three domains: \emph{Biology}, \emph{Drones}, and \emph{Recipes}, representing scientific, safety-critical, and everyday reasoning scenarios. We find a consistent near-conclusion bias: LLMs tend to focus on steps closest to the final proof conclusion rather than on the most informative ones. A targeted human study confirms that explanations based on such steps are rated less appropriate for end users. These findings indicate that even when reasoning is provided, current LLMs face challenges in communicating key information in a useful manner, highlighting the need for LLMs that can communicate important details reliably.

ABSTRACT. Abduction is a central approach to explain missing entailments from a knowledge base by providing a hypothesis, that would, if added to the knowledge base, make the missing entailment become true. Abduction under repair semantics has recently been investigated in detail, where several desirable properties and optimality criteria were considered, such as signature-restrictions and minimality in size and of introduced conflicts. Naturally, hypotheses that satisfy more than one of these properties or combine a property with an optimality criterion would be even more desirable for applications. So far, such hypotheses have not been investigated in the literature. In the present paper, we consider the ABox abduction problem for hypotheses satisfying more than one property or additional optimality criteria, for EL_bot under brave and AR semantics. Our main observation is that often requiring additional properties for hypotheses does not lead to an increase of complexity.

ABSTRACT. The need for explanations to predictions in knowledge graphs is increasing because they are generally computed via embedding-based methods that are efficient, but do not explain predictions. Many explanation methods rely on axioms in the knowledge graph that are incomplete, thus often making the explanations incomplete. One way to address this gap is to consider, for explanations, hypothetical knowledge at the schema or assertion level. However, methods based on hypothetical assertions often ignore existing facts. Conversely, approaches that enrich explanations via rule learning typically disregard the available schema. We propose LPX-AbPoint, the first method using a combination of abduction and pinpointing techniques to compute explanations consisting of both schema axioms and existing or hypothetical assertions. We present a comparative empirical study showing that our method produces more useful explanations than approaches relying solely on observed knowledge, while remaining complementary to rule learning techniques.

ABSTRACT. One way of enhancing link prediction in knowledge graphs in an interpretable and trustworthy way is to use ontology embeddings. These embeddings translate a knowledge graph together with its background ontology into a vector space by representing concepts as convex sets and logical operators between these concepts as geometric operations between the resp. sets. This allows for using both geometric regularities and background knowledge for learning. Some fragments of the description logic ℰℒ++ such as ℰℒℋ𝒪(○)^\bot are particularly well-suited as a basis for an embedding, as they offer a good trade-off between expressiveness and complexity. One popularapproach for embedding these ontologies is to interpret concepts as boxes in some R^n. Although box embeddings proved to be particularly useful in this context, they are not able to represent every ontology correctly. In this work, we open the door to a new geometric framework by introducing prism embeddings. Firstly, we show that prisms do not suffer from the same restrictions as boxes. To illustrate this advantage, we present concrete ontology examples that are problematic for box embeddings but can be represented using prisms. Secondly, we show that prism embeddings extend box embeddings in the sense that each box interpretation of an ℰℒℋ𝒪(○)^\bot ontology induces a prism interpretation, though possibly at the cost of an increase in dimensionality of at most two. Finally, we discuss the usage of prism embeddings in practice by sketching adaptations of implementations of box-based embedding approaches to the prism case.

ABSTRACT. In this proposed talk, we will present work in progress towards a “primitive” categorical structure for concurrent game semantics: a categorical structure that is simple and lets us derive categorically familiar models of various languages and evaluation strategies.

ABSTRACT. Bidirectional information flow is a central concept in both categorical game semantics and practical functional programming. In game semantics, the Joyal-Street-Verity's Int construction provides a canonical way to build compact closed categories from traced monoidal categories, elegantly modeling bidirectional interaction and feedback loops. Conversely, in functional programming, the Lens construction offers a robust, compositional framework for bidirectional state access and update. This work-in-progress explores the structural relationship between these two paradigms. We propose an adjunction between the categories arising from the Lens and Int constructions. By formally connecting the state-based approach of the Lens construction with the traced monoidal approach of the Int construction, we aim to bridge abstract game-semantic models with compositional theories of bidirectional flow. In this talk, we will outline the core functorial mappings between these categories, present the ongoing proofs of the adjunction, and discuss its potential applications to the foundations of game semantics.

ABSTRACT. For a first-order language with full ground references and iteration, we give an explicit denotational semantics. A type denotes a “platform set”, which is a family of “platforms” that indicate the references included. A state is represented as a tree, showing the result of following chains of references, whose nodes are partitioned into finitely many equivalence classes, showing the aliasing. The model is equivalent to known models that use ends or coends, or strong nominal sets, but is simpler in the sense that a morphism is simply a function.

ABSTRACT. In this work we introduce proof-theoretic tools to the investigation of logics of qualitative probability which, to the best of our knowledge are missing in the literature. We report on ongoing work, introducing weaker systems for qualitative probability based on the model of the polynomial approximation of classical logic that have polynomial computational complexity and approximate full qualitative reasoning.

ABSTRACT. This paper studies strategic communication under ambiguity within a cheap talk framework, extending standard models beyond probabilistic beliefs. We represent uncertainty using Dempster–Shafer mass functions, allowing for non-additive and ambiguous beliefs, and analyze how a sender optimally communicates when unsure how a receiver resolves such ambiguity. Considering neutral, robust, and optimistic attitudes, we characterize equilibrium behavior and show how ambiguity shapes persuasion strategies and outcomes.

ABSTRACT. Wepropose an ASP approach to reasoning about Halpern-Pearl actual causes and argue that our encoding is simpler, conceptually more appropriate, and more general than the existing approach in literature.

ABSTRACT. Joe Halpern and I started about causality and harm in voting contexts first in July 2025 in Dusseldorf, and longer in December 2025 in Paris, where Joe had been invited to give a seminar, which was excellent. We talked about voting and causality for several hours and he promised to send me his latest draft, which he did on December 28.

ABSTRACT. We study the problem of computing actual causes for neural network (NN) predictions under structured input dependencies. Existing explanation methods typically assume feature independence, which can produce misleading explanations when inputs are causally related. To address this limitation, we formalize explanations using Halpern and Pearl actual causality within Structural Causal Models (SCMs). We reduce the computation of actual causes to a NN verification problem by combining differentiable relaxations with branch-and-bound verification techniques. Our preliminary experiments indicate that the proposed method is effective and scalable for computing causal explanations of neural network predictions.

ABSTRACT. Both Quantified Boolean Formulae (QBF) as well as Dependency Quantified Boolean Formulae (DQBF) can impose spurious dependencies among variables. Since computing all spurious dependencies is in general intractable, dependency schemes are applied to detect independencies. Several dependency schemes for DQBF have been proposed in recent years. One of the strongest currently available dependency schemes is the family of implication-free dependency schemes by Beyersdorff et al. In this paper, we extend the implication-free dependency yielding an even stronger dependency scheme.

ABSTRACT. Symmetry breaking techniques have been extensively studied in automated reasoning for reducing the search space. In particular these techniques have already been well explored in the case of SAT and QBF. In this talk we discuss symmetries of dependency quantified boolean formulas (DQBF), a generalization of QBF which allows for explicit quantifier dependencies. It turns out that extending existing QBF symmetry techniques to DQBF is non-trivial due to a possible non-linear dependency structure. We illustrate these difficulties with an example that shows that a naive lifting of QBF symmetry breaking is not sufficient, and that we need more refined methods for dealing with such dependency structures.

ABSTRACT. Dependency quantified Boolean formulas (DQBF) provide a powerful, NEXPTIME-complete formalism for succinct encoding of NP-complete problems. While significant effort has been invested in developing DQBF solvers, their practical performance compared to explicit-representation solvers remains under-explored. In this work, we evaluate DQBF solving for classical succinct graph problems, such as graph coloring, $k$-clique, and Hamiltonian cycle, against traditional solvers using explicit representations. Our experimental results highlight that in general the DQBF approach is more advantageous than SAT-based approaches in handling these complex succinct combinatorial tasks.

ABSTRACT. In this paper we continue assessing the feasibility of the approach to the mechanization of type theory by using classical syntax and Stoughton's multiple substitutions and report some substantial progress. We present formal proofs of confluence for beta-reduction and by using Takahashi's revision of Tait and Martin-Löf's proof, subject reduction for the entire family of the Pure Type Systems and consistency for some impredicative subclass, assuming normalization. As to the proof of confluence, we also develop a theory of alpha-commutative relations which, in our view, entails a clearer presentation and treatment of the problem than in similar developments. Finally, we assess general merits and drawbacks of the approach. The whole development has been machine-checked using Agda.

ABSTRACT. Rewriting Induction (RI) is a formal system in term rewriting to establish program equivalence. The recently defined Bounded RI for higher-order Logically Constrained Term Rewriting Systems (LCSTRSs) yields a convenient proof system for analyzing real programming code. A practical challenge in RI is the automatic generation of induction hypotheses, called lemmas. While various lemma generation techniques exist for plain term rewriting, there are much fewer that consider the intricacies brought on by calculations or constraints. Taking advantage of recent developments in higher-order RI, we here present a new approach based on templates, which operates by recognising typical programming constructs as instances of higher-order functions. While templates have been used as a stand-alone method to justify the correctness of program transformations, we here consider their integration in Bounded RI to obtain a complementary lemma generation heuristic. This allows us to prove equivalences that were previously out of reach.

ABSTRACT. Following in the footsteps of the success of Mathlib -- the centralised library of formalised mathematics in Lean -- CSLib is a rapidly-growing centralised library of formalised computer science and software. In this paper, we present its founding technical principles, operation, abstractions, and semantic framework. We contribute reusable semantic interfaces (reduction and labelled transition systems), proof automation, CI/testing support for maintaining automation and compatibility with Mathlib, and the first substantial developments of languages and models.

ABSTRACT. Large language models excel at code generation for mainstream programming languages but struggle with domain-specific languages such as MiniZinc, a constraint modeling language for combinatorial problems. To address this propose Learn2Zinc and investigate whether targeted fine-tuning can teach small language models (0.6B to 20B parameters) to generate syntactically correct and semantically valid MiniZinc models from natural language descriptions. Our key finding is that syntax errors dominate failures: the out-of-the-box execution accuracy of small language models is near zero. We propose cross-model error bootstrapping approach that collects syntax errors from multiple LLM runs and leverages those to curate an error correction dataset. With an ensemble of our fine-tuned models, we achieve up to 98% execution accuracy. The solution accuracy remains at 35% indicating that while syntax is learnable, constraint reasoning still remains a challenge. We open-source Learn2Zinc fine-tuning pipeline, datasets, and models for further research.

ABSTRACT. Constraint Programming (CP) is a powerful paradigm for solving combinatorial problems, yet translating natural language problem descriptions into executable models remains a significant bottleneck. While Large Language Models (LLMs) show promise in automating this translation, they often struggle with subtle semantic errors in the absence of oracle validation at test time. To address this, we introduce CP-SynC (Constraint Programming modeling with Synthesized Checkers), a multi-agent workflow for zero-shot constraint modeling in MiniZinc. CP-SynC coordinates modeling agents that generate and refine candidate models and validation agents that synthesize semantic checkers to provide feedback on semantic correctness. To mitigate noise inherent in individual LLM outputs, CP-SynC explores multiple modeling trajectories in parallel and employs selection agents to select the final model via multi-agent evidence aggregation. Extensive experiments on a benchmark of 100 CP problems show that CP-SynC substantially outperforms representative baselines in MiniZinc modeling.

ABSTRACT. Constraint programming languages such as MiniZinc provide a way of modelling a wide range of problems, enabling their solution with general-purpose constraint solvers. However, the process of turning a natural language problem description into a constraint program requires a human expert familiar with the target language. This is a barrier to broader adoption and use of constraint solvers. Large Language Models (LLMs) are excellent at processing natural language and competent at imperative programming. Recent work shows that LLMs are moderately effective at turning natural language problem descriptions into MiniZinc constraint models. However, they are relatively weak at writing MiniZinc, when compared with their ability to write conventional programs in C, Java and Python. We have previously developed the CoPTIC constraint programming system, which uses bounded model-checking to repurpose C as a declarative programming language. A CoPTIC model is a C program that checks whether a prospective solution satisfies the required constraints. As LLMs are better at writing C than MiniZinc, we posit that they will be better at turning natural language problem descriptions into CoPTIC models than into MiniZinc models. We propose to evaluate this claim using the CPEVAL benchmark.

ABSTRACT. Large Language Models (LLMs) provide a flexible interface for interpreting natural language problem descriptions, but they remain unreliable when asked to solve constrained optimisation tasks directly. We study a neuro-symbolic approach in which an LLM translates a natural language description of an optimisation problem into executable Python code using PySAT. The generated program constructs a weighted partial Maximum Satisfiability (MaxSAT) instance, invokes a MaxSAT solver, and returns the resulting assignment in a prescribed output format. In this way, the LLM is used primarily for semantic parsing and modelling, while the optimisation step is delegated to an exact symbolic solver. We outline an end-to-end pipeline consisting of natural language input, intermediate encoding plans, PySAT code generation, MaxSAT solving through RC2, and independent validation of returned solutions. This workshop abstract distils the main idea of using LLMs as natural language front-ends for solver-backed MaxSAT modelling, with the goal of making MaxSAT technology more accessible to users who do not write formal encodings by hand.

ABSTRACT. We introduce ZebraProlog, an approach for solving the Zebra Logic benchmark combining Large Language Models (LLMs) and constraint programming. We compare the performance of ZebraProlog with the logic.py approach, another approach for solving the Zebra Logic benchmark using LLMs and a constraint solver. Our approach does not go through an intermediate representation of the problem in a domain specific language, but rather directly translates to Prolog/CLP(FD) code which is then executed to find a solution. This approach contributes to clarify the benefits and costs of using an intermediate representation. Our experiments reveal two main findings: on the one hand, the DSL-based approach of logic.py gives a slight advantage in terms of success rate (91.9% for logic.py vs 84.6% for ZebraProlog). On the other hand, the DSL-free approach of ZebraProlog is 19.6% faster than logic.py.

ABSTRACT. Logic puzzles like Sudoku have been very popular for several decades, some videos showing the solution steps for a complex Sudoku variant instance have over 10 million views. This makes this problem domain an ideal area to demonstrate the advantages of using Constraint Programming to a wider audience. We present an interactive application for solving Sudoku variants, extending the classical Sudoku grid with a variety of additional constraints. The aim is not just to search for solutions of a given puzzle, but to help a user to find a solution interactively. We use an off-the-shelf constraint solver, Choco-solver, to model and propagate 200 common Sudoku variant constraints. This uses a combination of specific global constraints and table constraints to describe feasible or infeasible tuples. In other cases, we use logical expressions over basic constraints to model complex side constraints. The user can add constraints interactively if the solver does not find the solution by propagation alone, or rely on an agent to add deduced constraints dynamically. We evaluate the solver on different data sets, and show that over 97% of the problems in the 2025 Sudoku Grand Prix can be solved by the tool, and that many popular, complex puzzle instances can be solved by a handful of manual constraints and propagation alone.

ABSTRACT. Helmut Simonis's 2005 ModRef paper, Sudoku as a Constraint Problem, used standard 9x9 Sudoku as a compact constraint-programming laboratory for comparing propagation-oriented models. This paper extends that setup to Sudoku puzzles of sizes 6x6, 9x9, 16x16, 25x25, and 36x36. We generate 32,000 unique-solution base puzzles and run 170,000 hardness walks that add clues back to the puzzles, generating 402,201 additional, simpler instances. These walks ensure that every studied size includes instances in easier hardness buckets. The original hardness categories identified by Simonis remain useful, but the grid size changes the observed propagation behaviour. No initially generated 25x25 or 36x36 puzzle is solved without search, even with domain-consistent propagation and domain shaving. Puzzle generation uses Gecode and OR-Tools, and hardness testing uses Gecode.

ABSTRACT. Answer set programming (ASP) and reasoning from conditional belief bases are two most prominent approaches to nonmonotonic reasoning. Both frameworks are rule-based in principle, yet substantially different with respect to syntax and semantics. Recently, approaches to combine ASP programs with conditional belief bases to prioritize answer sets have been proposed. A crucial question for applying such approaches is to decide which knowledge and beliefs should be modeled in which part of the combined knowledge base, ASP or conditionals. In this paper, we investigate the differences between encoding information in ASP vs. as conditionals in more detail. We point out general differences between the reasoning processes of ASP vs. conditionals and provide guidelines for knowledge engineering with ASP and conditionals. Moreover, we illustrate how choosing either of the two frameworks has significant effects on the resulting solutions. In particular, we focus on how factual information can be taken into account in the combined framework of ASP and conditionals in various ways. Furthermore, we build bridges between ASP and conditional reasoning by showing how conditionals with a suitable syntax can be encoded as weak constraints in ASP. Conversely, this may also help to find suitable weights for weak constraints in ASP programs.

ABSTRACT. Human reasoning often operates through qualitative concepts expressed by linguistic labels such as high, low, expensive, or cheap, whose interpretation depends on context and is usually vague, despite being rooted in numerical data. This paper explores a novel fuzzy-logic-based qualitative extension of Answer Set Programming (ASP) to bridge numerical information and qualitative reasoning. The underlying language, formally introduced in a separate work, provides a principled framework that avoids rigid thresholds and supports robust reasoning under vagueness. Focusing on a representative use case, we illustrate how the framework integrates numerically grounded inputs (such as outputs of machine learning models) with symbolic reasoning over qualitative labels. Key features, including learning-based membership functions and semantically enriched predicates, enable the combination of expert knowledge, contextual factors, and subjective interpretations within a unified declarative setting.

ABSTRACT. We consider a *definitional fragment* of Temporal Equilibrium Logic (TEL), which allows to capture temporal rules containing complex (implication-free) temporal formulas in rule bodies. We show that the basic reasoning tasks in this fragment are PSPACE-complete, under the assumption that formulas are interpreted over finite traces. This shows a significant drop from the EXPSPACE-completeness of unrestricted TEL. Our method is based on characterizing stable models in terms of different kinds of *type sequences*, which allow to reason both about existence and non-existence of stable models. In addition to handling tasks like stable model existence, we also show how the set of all stable models of a program can be represented as a non-deterministic finite state automaton (NFA). Our method is self-contained in the sense that, in contrast to previous approaches, it does not rely on technical automata-theoretic results as black boxes. Our method can be implemented using SAT solving techniques and a prototype system is available.

ABSTRACT. The computation of geometric loci is a foundational feature of Dynamic Geometry software. Despite its conceptual importance and long history, current Dynamic Geometry systems still lack a fully symbolic and algebraically meaningful approach to locus computation. Even platforms that integrate computer algebra, such as GeoGebra, mainly provide numerical or graphical outputs whose interpre- tation remains limited. In this paper, we present a Computer Algebra System-based exploration of symbolic locus computation aimed at identifying conceptual, algebraic, and algorithmic challenges that arise when attempting to move beyond current Dynamic Geometry capabilities. Computer Al- gebra Systems play a central role in our work, not as a black-box calculator, but as a research tool that allows the design and testing of non-standard symbolic algorithms based on elimination theory, ideals, and parameter handling. Through a series of representative examples, we show why truly symbolic locus computation is mathematically nontrivial and computationally demanding, and why a Computer Algebra System is essential for experimenting with new approaches that may eventually inform the development of future Dynamic Geometry commands. Our work should be understood as an ongoing process to lay the groundwork for gradual and feasible advances rather than proposing finished solutions.

ABSTRACT. In German secondary education, students' exposure to proof-writing is typically limited to simple term rewriting, informal arguments, and the use of computer algebra systems (CAS). The Deutsche SchülerAkademie is a program offering intensive academic summer courses to secondary-school students in their final two years before graduation. Within this context, a course aimed at teaching students the basics of Isabelle/HOL was conducted, culminating in the formalization of the students' own correctness proof of the RSA cryptosystem. The authors participated in this course, one as a student and the other as an instructor. In this paper, we describe the aims and the framework of the course as well as the resulting curriculum. Furthermore, we discuss the difficulties faced by the students and how these were addressed. Finally, we reflect on the students' achievements and possibilities for further improvement.

ABSTRACT. Maximum Satisfiability (MaxSAT) is an approach for solving NP-hard optimization problems expressed in propositional logic. Among the known approaches for solving MaxSAT is the Implicit Hitting Set approach that combines SAT solvers and Integer Linear Programming solvers. No Implicit Hitting solver participated in the most important evaluation of state-of-the-art MaxSAT solvers—the annual MaxSAT Evaluation—since MaxHS did in 2022. Since then, MaxHS remains unmaintained and is not allowed to participate under the current ruleset. Further, recent advances in MaxSAT testing have revealed numerous bugs in MaxHS. In this paper, we describe our revision of MaxHS, which include numerous bugfixes, the integration of an open source Integer Linear Programming solver that allows MaxHS to participate in the evaluation, and an exact mode that avoids numerical problems.

ABSTRACT. Anytime MaxSAT solving is indispensable in applications that require finding near-optimal solutions within a flexible, user-controlled time budget. Recent years have seen substantial progress in anytime MaxSAT algorithms, including the introduction of SAT-based local search, the development of efficient approximation techniques, and significant advances in classical local search methods. However, all leading anytime solvers—including the winners of the three most recent MaxSAT Evaluations (MSEs) in the anytime categories—reuse the code base of a single solver, tt-open-wbo-inc. While highly efficient, this code base lacks an in-memory API, is non-incremental and incomplete, and contains a substantial amount of dead and legacy code. We introduce Aperture, a new solver for SAT-based optimization, including MaxSAT, written from scratch in C++ with in-memory APIs for C++ (IPAMIR-compliant) and Python. For MaxSAT, Aperture is anytime, incremental, and complete; algorithmically, it follows a similar high-level approach to tt-open-wbo-inc, but employs a unified flow for both weighted and unweighted MaxSAT. Performance-wise, Aperture is highly competitive as a MaxSAT solver. Under the benchmark sets and evaluation conditions of MSE 2024, it outperforms both the MSE 2024 winner SPB-MaxSAT-c and tt-open-wbo-inc in all four anytime categories, and in 8 out of 12 anytime categories across the three most recent MSEs (2022–2024). Moreover, Aperture outperforms leading non-anytime MaxSAT solvers on 2 out of the 6 incremental benchmark sets from MSE 2022, an evaluation setting in which—unlike the anytime categories—both incrementality and completeness are mandatory. Beyond MaxSAT, Aperture also supports other paradigms for optimizing an objective function under Boolean constraints, including Optimization Modulo Bitvectors (OBV) and black-box optimization. Across all supported paradigms, the solver is incremental and anytime; it is complete for MaxSAT and OBV, but incomplete for black-box optimization.

ABSTRACT. We revisit the problem of computing a smallest minimal unsatisfiable subset (SMUS) of a propositional CNF formula. The state-of-the-art algorithm by Ignatiev et al. frames SMUS extraction as finding a minimum-cardinality hitting set of the set of minimal correction sets (MCSes), and solves the resulting optimization problem by a generate-and-test loop over a growing MCS collection. We propose to replace the hitting-set loop with a full branch-and-cut solver—concretely, SCIP augmented with a custom constraint handler—so that every incumbent solution discovered during the search is a valid UNSAT subset, giving a monotonically improving anytime sequence. The feasibility is enforced by a separation oracle that, given a fractional point in the LP relaxation, identifies a violated MCS inequality by solving an instance of the weighted MaxSAT problem. Experimental evaluation suggests that, although the formulas with smaller gaps between the smallest MUS cardinality and the number of disjoint MCSes in a formula, such as the ones from the MUS track of the SAT Competition 2011, are favorable for implicit hitting set solving, our branch-and-cut approach is superior to the implicit hitting set approach on formulas with large gaps.

ABSTRACT. We present work in progress towards a combinatorial characterisation of first-order bicategories. These structures provide a categorical setting for studying first-order logic through a string-diagrammatic syntax. Unlike string diagrams for monoidal categories, those of first-order bicategories do not admit a straightforward combinatorial representation in terms of hypergraphs, due to two interacting monoidal structures. Developing such a representation is a necessary step towards a computationally feasible implementation of string diagram rewriting: structurally equivalent string diagrams can then be interpreted as the same hypergraph, substantially simplifying matching procedures.

ABSTRACT. See PDF

ABSTRACT. The talk will be based on two preperints on sequential theories. One paper shows that a certain weak set theory of Harvey Friedman requires a parameter to witness its sequentiality. The other paper proves non-sequentiality of a certain extension of Robinson`s Q with pairing. This theory is a subtheory of PA^_, the theory of nonnegative of parts of discretely ordered commutative rings.

ABSTRACT. The aim of the present note is to report on ongoing work to investigate the linear fragment of the λ-calculus using the tools of categorical universal algebra, adapting the techniques and ideas developed by Hyland to the linear setting of operads and monoidal categories. We start by investigating algebraic models of the linear λ-calculus through the notion of semiclosed operad and we prove that each of such models gives rise to a linear reflexive object in a closed monoidal category. Inspired by the notion of λ-algebra, we define a category of linear λ-algebras, and we prove that this category is equivalent to that of semiclosed operads. Therefore, combining the two results, we have that every linear λ-algebra gives rise to a linear reflexive object in a closed monoidal category.

ABSTRACT. Multicategories are considered an appropriate setting to model term calculi since they allow a more natural treatment of typing contexts and of the composition rule. Additional structure on them describes structural rules such as the exchange rule, the contraction rule and the weakening rule. Cartesian multicategories with one object are called cartesian operads. This specific class of objects is the setting which we will consider in this talk to categorically describe the untyped lambda calculus seen through the lens of linear logic. In doing so, we refine Hyland's approach to the untyped lambda calculus as a semi-closed algebraic theory. Cartesian operads are equivalent to clones. This equivalence gives us an abstract way to phrase two presentations of the untyped lambda calculus: the more traditional, additive one and the multiplicative one which is in the spirit of linear logic. This result can be extended to the general framework of cartesian Cat-operads and Cat-clones. This then yields two generalizations of the Set-enriched situation where the rewriting theory of the lambda calculus also obtains an explicit algebraic treatment. In this way, the untyped lambda calculus can be both equipped with the structure of a closed Cat-clone and that of a cartesian closed Cat-operad. Moreover, in this richer setting, we obtain by universal construction an equational theory on rewritings that deserves to be further explored. We aim to do so by defining a rewriting theory of the rewritings themselves, bringing together Hyland's and Hilken's approaches.

ABSTRACT. We have recently constructed sequent calculi for non-commutative linear intuitionistic versions of modal logics K, T, K4 and S4 that we have defined via semantics in terms of monoidal categories with a strong monoidal endofunctor, copointed endofunctor, semicomonad or comonad, optionally well-copointed/idempotent. Here we show that the designs of these sequent calculi are directly justified by equivalent semantics of these logics in terms of representable multicategories for suitable notions of (generalized) multicategory and representability: they are presentations of the free such representable multicategories.

ABSTRACT. The logic of inferable, L-DINF, models cooperative agents that reason through explicit beliefs, background knowledge, mental actions, physical actions, roles, resources, costs, preferences, and equivalence classes of actions. We add a probabilistic package to the modular semantics of L-DINF, assigning probability measures to epistemic alternatives and success probabilities to physical actions, while preserving the original separation between the core epistemic model and optional packages. We define probabilistic explicit belief, probabilistic executability, and a deterministic instantiation of the L-DINF action selector based on a probability-aware desirability score. We show how an agent can select a lower-preference but more reliable action when reliability outweighs preference. The proposal is conservative, explainable, and directly extensible towards dynamic probability update.

ABSTRACT. We consider the Strategy Repair problem for an autonomous agent acting in a stochastic dynamic environment. The problem concerns finding the minimum number of modifications that refine a strategy for a probabilistic reachability game into an optimal one, i.e. maximising the probability of winning. After introducing and motivating the problem, we first present a polynomial-time solution for one-player games, i.e. Markov decision processes. The approach exploits a game-to-game reduction, followed by solving a suitable instance of the minimum spanning tree problem. We then extend the problem to the discounted case, where the agent is required to win the game in the fewest possible moves.

ABSTRACT. Multi-agent decision making under uncertainty can be modelled using decentralised partially observable Markov decision processes (DecPOMDPs). However, DecPOMDPs are notoriously difficult to solve due to their exponential dependence on the number of agents. Lifting is a technique that treats groups of indistinguishable instances through representatives if possible, yielding tractable inference in the number of instances in a model. This paper discusses the assumptions necessary for indistinguishability among agents, providing a definition of so-called isomorphic DecPOMDPs that have a model complexity no longer dependent on the number of agents, as well as a lifted solution approach that exploits this lifted agent set for space and runtime gains.

ABSTRACT. In this paper, we prove that \PATLH is exponentially more succinct than \PATLC. In prior work it was shown that \PATLC strictly subsumes \PATLH in expressive power, yet it was conjectured that any \PATLC-specifiable property could be encoded with exponentially shorter formulas than in \PATLH. Establishing this remained elusive, since existing succinctness proofs (e.g., for non-probabilistic \ATLH vs \ATLK) do not readily transfer to the Shannon-entropy setting. Here we resolve the conjecture by explicitly constructing a family of \PATLH formulas $\varphi_n$ of size $O(n)$ and proving that any equivalent \PATLC formula requires size $2^{\Omega(n)}$. Our argument uses the one-person formula-size-game framework. This formally confirms a conjecture from the previous \PATLH/\PATLC study, demonstrating a genuine exponential succinctness gap and advancing recent developments in logical succinctness for strategic-epistemic logics.

ABSTRACT. Multi-agent systems are commonly designed to reduce disagreement through voting, consensus protocols, debate, or fault-tolerant aggregation. We argue that this objective is insufficient for value-laden tasks, where disagreement may reflect genuine normative uncertainty rather than agent error. Building on prior work on reasoning-trace disagreement in human-AI collaborative moderation, we propose a knowledge-representation layer in which reasoning traces and agent decisions are abstracted into symbolic disagreement states. Given agents producing explicit reasoning traces and binary decisions, we distinguish four states according to reasoning similarity and conclusion agreement: convergent agreement, divergent agreement, convergent disagreement and divergent disagreement. These states support defeasible strategic routing rules. We instantiate the framework in content moderation and argue that disagreement-aware routing provides a bridge between sub-symbolic LLM deliberation and symbolic knowledge representation for multi-agent strategic reasoning.

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

ABSTRACT. In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking to keep the clause database compact, thereby reducing the memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best.

ABSTRACT. State-of-the-art projected model counters have achieved remarkable advances by integrating a variety of methods, including those from SAT solvers. However, this has resulted in increasingly complex implementations. Furthermore, the integration of multiple methods may introduce unexpected inconsistencies, leading to incorrect model counts. To address these issues, we propose a declarative framework for describing the projected-model counting procedure that integrates practical methods. Our framework captures all methods implemented in GPMC, one of the state-of-the-art projected model counters, while remaining open to future extensions. We also present a proof sketch for the correctness of the framework, outlining the key ideas.

ABSTRACT. Reductions and gadgets are key tools in computational complexity, with gadgets serving as the building blocks of reductions. Despite their importance, gadget construction has traditionally been ad hoc. We present a method to compute gadgets automatically, enabling systematic reductions and offering insights for both theory and practical solver design.

ABSTRACT. Access to high-quality benchmark instances is essential for developing new algorithms and constraint models, as well as for comparing existing approaches. However, hand-crafted instances are often time-consuming to produce and may offer limited coverage of the relevant instance space. Consequently, automated benchmark instance generation has been widely studied across optimisation and related fields. In this work, we study AutoIG, a previously proposed constraint-based automated instance generation framework that combines automated algorithm configuration, constraint modelling, and constraint solving to generate instances of a specified difficulty for a target solver. A key limitation of AutoIG is that it does not explicitly encourage diversity among the generated instances. This can lead to benchmark sets that satisfy the desired difficulty requirements but provide limited variation in solver behaviour. As a preliminary step towards addressing this limitation, we investigate three simple mechanisms for promoting diversity in the performance space. That is, we aim to generate instances that not only meet a target difficulty level, but also induce diverse performance from the target solver. Experiments on two problem classes and two solvers show promising potential, while also revealing several open challenges, including how diversity should be defined and measured, and how diversity-promoting mechanisms affect the search process during instance generation.

ABSTRACT. In this paper, we introduce ranking-based semantics for incomplete argumentation frameworks (IAFs). These frameworks are extensions of Dung's abstract argumentation framework with qualitative uncertainty about the existence of arguments and attacks. Up to this point reasoning on incomplete argumentation framework have only followed Dung's extension-based approaches, where a set of arguments is either jointly accepted or not. We discuss several approaches how to rank the individual arguments. The first two approaches rely on the acceptance status of the arguments with respect to an extension-based semantics. Another family of approaches utilises ranking-based semantics on the individual completions of an IAF (i.e. AFs where the uncertainty is ``resolved'') and then aggregate the resulting rankings with voting rules. In addition, we propose a number of principles the ranking-based semantics for IAFs should follow, some adapted from existing principles out of the formal argumentation literature, others novel principles tailored to IAFs. We determine which of these properties are satisfied by our approaches.

ABSTRACT. We show that deciding whether an argument a is stronger than an argument b with respect to the discussion-based semantics of Amgoud and Ben-Naim is decidable in polynomial time. At its core, this problem is about deciding whether, for two vertices in a graph, the number of walks of each length ending in those vertices is the same. We employ results from automata theory and reduce this problem to the equivalence problem for semiring automata. This offers a new perspective on the computational complexity of ranking semantics, an area in which the complexity of many semantics remains open.

ABSTRACT. Skeptical acceptance under the preferred semantics is one of the most intricate reasoning problems in abstract argumentation. That is why efficient solving approaches are of utmost importance for this problem. In this work, we investigate algorithmic shortcuts that can be used to solve this reasoning problem with considerably less resources than sound and complete approaches. Besides an overview of the state-of-the-art, we also propose several novel shortcuts to improve the applicability of such techniques. Finally, we perform an extensive evaluation of all shortcuts regarding their potential to improve the runtime efficiency of argumentation solvers. As our results show, we can significantly improve the runtime of state-of-the-art argumentation solvers by utilizing a variety of shortcuts.

ABSTRACT. We study the use of an educational proof assistant in an introductory proof course through a quasi-experiment in a varied setting: multiple teachers, students with different study programs, and a mixed Dutch-English language environment. First-year university students are known to struggle with writing proofs. Waterproof is a proof assistant that is designed to support the transfer of skills to paper proofs by working with controlled natural language. We focus on the students' ability to construct valid mathematical proofs, and on their learning process. We study this through in-class observation, surveys, and analysis of student performance and proof structure. We present evidence that effects of using an educational proof assistant carry over to the pen-and-paper context, even when the assistant is English and the proof is given in Dutch. We also present evidence that suggests students in the Mathematics-Computer Science program achieve higher grades when using Waterproof. Our most important conclusion is that an educational proof assistant can help students be more explicit in their proofs.

ABSTRACT. We introduce Waterproof River: An LLM-based tutor that augments the educational software Waterproof. In Waterproof, students can write proofs in controlled natural language. Waterproof River gives additional support with writing proofs in this form. We give an overview of its features, such as helping with syntax, asking for a hint, translating a free-form natural language proof to Waterproof syntax, and asking questions on the lecture notes. We present its implementation and discuss how such a tool could evolve based on in-class experience.

ABSTRACT. In this talk, we will present a formalization of a preparatory-class propositional-logic corpus which is both readable and machine-checked. The goal of this work is to produce material that can be used to teach students who are not acquainted with a proof assistant. To reach this goal, we base our work on a layer above the Lean proof assistant called Yalep [10] which allows to express proofs in a minimalistic controled natural language. We explain the scope of the formalization, the main modeling choices, and the main difficulties. We also present representative results, including the formalization of two competitive exam problems to show that the library is usable in this context.

ABSTRACT. Modern Boolean Satisfiability (SAT) solvers, based on the Conflict-Driven Clause Learning (CDCL) paradigm, achieve state-of-the-art efficiency but present a steep learning curve due to their sophisticated algorithms and highly optimized data structures. Understanding these complex mechanics and evaluating the effectiveness of problem encodings is notoriously challenging for students and emerging researchers. To ease this learning process, we introduce the Interactive SAT Tracer (SAT-IT), an open-access web environment designed to make the foundations of SAT solving highly visible and interactive. SAT-IT offers a staged pedagogical progression—from naive backtracking to DPLL and full CDCL with the two-watched literals scheme. Users can clearly inspect fundamental data structures, search space trails, and solving statistics. The tool interactive search space exploration is boosted with literal-level breakpoints for targeted inspection, alongside versatile automatic solving modes that offer both continuous real-time execution and state-based subroutine automation. Combined with a powerful ``what-if'' capability for stepping backward to explore alternative decisions, an instance manager, and an extensible architecture ready to support additional algorithms, SAT-IT serves as a practical, granular lens for experimenting with SAT solving algorithms and analysing encodings efficiency.

ABSTRACT. Steiner triple systems (STS) and subsets of these known as partial STS (PSTS) are combinatorial objects that have received substantial interest from mathematicians since their introduction in 1847. Over the last three decades, (P)TS have found applications in diverse fields ranging from digital circuit testing to wireless transmission. Perhaps unsurprisingly, the ``triple'' in (P)STS allows for a mapping to 3-conjunctive normal form (3-CNF) formulas, the Boolean formula used as input to 3-SAT. Prompted by this ready conversion of (P)STS to 3-CNF formulas and numerous real-world applications of (P)STS, we explore the intersection of (P)STS with 3-SAT and its counting version #3-SAT. We explain the properties of (P)STS-generated 3-CNF formulas in terms familiar to the SAT community and experimentally compare them against randomly-generated 3-CNF formulas. We find that PSTS-3-CNF formulas are statistically distinct from randomly generated 3-CNF formulas, in both probability of satisfiability and expected solution count.

ABSTRACT. This paper addresses the Multi-Skill Project Scheduling Problem (MSPSP), an NP-hard optimization problem. We propose and evaluate MaxSAT and pseudo-Boolean optimization encoding for the MSPSP. We explore the fundamental trade-off between the expressive power of pseudo-Boolean (PB) constraints and the raw efficiency of MaxSAT solvers. By adapting implied constraints naturally expressed as PB constraints from the literature, we examine whether such additional reasoning provides a greater performance boost to MaxSAT or PB solvers. Our initial hypothesis---that including natural PB constraints into our MSPSP model would provide a greater incremental boost to PB solvers than to MaxSAT solvers---was tested through an exhaustive experimental evaluation using state-of-the-art solvers. Contrary to our expectations, MaxSAT solvers consistently outperform PB solvers on the MSPSP. Moreover, our results demonstrate the benefits of integrating implied constraints, as they significantly reduce the number of timeouts, regardless of the formalism used.

ABSTRACT. We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementations while retaining the same $\mathcal{O}(n^2(1+|A|))$ worst-case complexity. We then introduce a family of synthetic SAT benchmarks based on the observation that, for any formula $\phi$, the equivalence $\phi \leftrightarrow \mathrm{NF}_{\mathrm{OL}}(\phi)$ is a tautology whose Tseitin encoding yields unsatisfiable instances that are hard for state-of-the-art SAT solvers yet have short orthologic proofs. Applied to EPFL arithmetic circuits, our algorithm solves these instances efficiently while Kissat times out on a significant fraction. Finally, we show that using orthologic normalization as a preprocessing step reduces formula size and solving time by approximately 26\% on average over a large set of Boolean circuit benchmarks.

ABSTRACT. In Quantified Boolean Formulas (QBFs), dependency schemes help identify spurious or superfluous variable dependencies introduced by the quantifier prefix but not essential for constructing countermodels. Detecting such dependencies can provably shorten refutations in certain proof systems and is expected to improve the performance of QBF solvers. Among the most prominent solving techniques for QBFs is Quantified Conflict-Driven Clause Learning (QCDCL), a generalization of CDCL to the quantified setting. The proof system defined by Beyersdorff and Boehm in \cite{BB-LMCS23} provides an abstract framework that captures the reasoning employed by QCDCL solvers. The proposed talk will describe how dependency schemes can be incorporated into QCDCL-based proof systems in various phases: during preprocessing, in the decision heuristics, or within propagation and learning.

ABSTRACT. In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.

ABSTRACT. The General Data Protection Regulation (GDPR) establishes purpose limitation as a fundamental constraint on personal data processing: personal data must be collected, stored, and processed strictly in accordance with explicitly specified purposes. Therefore, systems are required not only to declare the purposes under which personal data are processed, but also to ensure that their runtime behaviour remains aligned with the declared purposes. Yet, in mainstream software engineering practice, purposes are often treated as informal declarations, largely disconnected from system behaviour and, therefore, not amenable to rigorous reasoning about purpose compliance. This gap becomes particularly problematic in distributed systems, where personal data may flow across multiple entities and evolve through complex communication patterns. To address this challenge, recent works propose a more elaborate treatment of purposes based on structured, action-oriented representations of the data-processing interactions involved in their fulfilment. Building on these insights, we introduce a formal, purpose-aware framework grounded in multiparty session types in which purposes are modelled as structured interaction protocols among system entities. Within our framework, system implementations are specified using a process calculus that captures the semantics of distributed interactions and features private data as a first-class entity. Furthermore, we define a type system that verifies compliance between declared purposes and system models, and we establish subject reduction and purpose fidelity results, thereby ensuring that well-typed systems do not deviate from their specified purposes during execution. We demonstrate our approach through a case study involving a healthcare system. Ultimately, our objective is to evolve this formal framework into a software-engineering-oriented approach that unifies purpose modelling and compliance verification within a lifecycle-driven methodology, thus enabling a practically applicable privacy-by-design process.

ABSTRACT. Path Predicate Modal Logic (PPML) is a generalization of Basic Modal Logic, where atoms are relational predicates instead of propositional symbols. The study of PPML is motivated as a way to abstractly investigate data-aware formalisms, such as XPath or DataGL. In this paper, we investigate some basic model theoretical aspects of PPML to better characterize its expressive power. More concretely, we investigate different ways of defining Hennessy-Milner classes, and a van Benthem characterization theorem. In doing so, we discuss the main challenges of dealing with the novel features of PPML, and what are the similarities with the standard approaches.

ABSTRACT. We study TEL^o , an extension of the description logic EL with the temporal operator O^n (‘in n instants from now’),by encoding its canonical models with sets of integers. We characterise reasoning in TEL^o in terms of operations on such sets and arrive at a correspondence between (fragments of) TEL^o and (classes of) resolved systems of equations over sets of integers. This generalises the previously established link between TEL^o and formal grammars, leading to simpler proofs of known results as well as yielding new results.

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

ABSTRACT. Temporal extensions of description logics often lead to a substantial increase in the complexity of reasoning. Nevertheless, tractable extensions of ℰℒ have been developed by restricting the occurrences of temporal concepts. One can even add so-called convex metric temporal diamond operators to ℰℒ, if they are only allowed to occur on the left-hand side of concept inclusions. In this paper, we consider the dual convex box operators for the first time, and investigate the behavior of complex temporal formulas in which convex diamond and box operators can be combined via composition, union and intersection. We demonstrate the intricate interplay between these operators, and present decision procedures for checking subsumption between complex temporal formulas.

ABSTRACT. This work investigates the expressive power of ontology-mediated queries (OMQs) from a descriptive complexity perspective. We first show that OMQ languages based on non-monotonic extension of one of the most expressive description logics cannot express all coNP-computable generic Boolean queries, despite being coNP-complete in data complexity. We then propose an extension of this language and show that it is expressive enough to precisely capture the class of all Boolean queries computable in coNP.

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 Truszczýnski 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.

ABSTRACT. Modern proof logging has been highly successful for discrete reasoning, but scientific computation still relies heavily on complex numerical pipelines whose outputs are rarely independently checkable. This talk uses a recent Keller-box computation arising from a Falkner–Skan thermal-flow model by Anwar et al. (2025) as a focused case study for this certification gap. After similarity reduction, the governing equations become a coupled nonlinear boundary-value problem; the final numerical solution is then produced through first-order reformulation, implicit box discretization, Newton linearization and repeated solution of block-tridiagonal linear systems. In such a setting, correctness is not a purely analytic matter: it depends on the fidelity of discretization, the consistency of boundary treatment, the soundness of linearization and the actual convergence behavior of the iterative solver. The talk argues that this solver layer is a natural target for proof logging. Rather than attempting to certify the entire physical model at once, we isolate the computational core and propose a certificate structure for it: logs for the reduced boundary-value problem, machine-checkable witnesses for each discretized system, residual certificates for Newton iterations, explicit verification of boundary-condition satisfaction and auditable checks for the numerical quantities ultimately reported from the computation. The case study also highlights challenges that are specific to numerical reasoning: floating-point effects, truncation of infinite domains, dependence on mesh choice and the need to distinguish empirical convergence from certifiable correctness. The broader aim is to help articulate what a proof-logging discipline for nonlinear scientific solvers should look like. We suggest that numerical workflows of this kind are both important and structurally rich enough to serve as realistic benchmarks for the next generation of certifying algorithms.

ABSTRACT. Reasoning about nonlinear real arithmetic (NRA) is pervasive in safety-critical applications. The applications range from robot motion planning to digital signal processing. Nevertheless, the decision procedures involved are usually highly intricate. The fastest complete algorithms have a doubly exponential lower bound, their implementations are notoriously delicate, and even mature tools occasionally return incorrect results. Given that many applications cannot tolerate unsound answers, it is necessary to develop means for certifying the answers of such algorithms. Two routes are commonly pursued: building a formally verified implementation, or instrumenting an existing solver to produce a machine-checkable proof certificate for every answer. The latter is considerably less intrusive, can be adapted more easily to changes in the solver, and is already the path taken by proof-producing SMT solvers such as cvc5 for theories like linear arithmetic and bit-vectors. Extending this treatment to NRA, however, has remained largely open. In this talk we report on ongoing work to bring proof production --- and independent proof reconstruction --- to four NRA algorithms with very different flavours, all in the context of cvc5 and lean-smt, a Lean tactic capable of reconstructing such proofs in the ITP: - Incremental Linearization (Cimatti et al.). An abstraction-refinement procedure that approximates multiplication by its tangent plane and transcendental functions by their Taylor polynomials. We have instrumented cvc5 to produce proofs for this algorithm, formalized the solver's proof calculus in Lean and extended lean-smt to reconstruct its proofs. The mechanization exposed several missing hypotheses and unsound corner cases in the documented calculus, which the cvc5 team has since addressed. - Cylindrical Algebraic Decomposition (Collins). The fastest known complete decision procedure for NRA, but also the most complex to instrument. We have instrumented cvc5's CAD to to produce proofs for the univariate case, and extended lean-smt so that it is capable of reconstructing such proofs. For achieving this, we had to implement a library of computable real algebraic numbers and to prove Sturm's theorem in Lean. This was inspired by a prior work done in the ITP Isabelle/HOL. We are currently working on the multivariate case. This generalization poses several challenges: formalizing complex proofs of the theorems on which the algorithm is based on; certifying that certain computations were done correctly by cvc5; instrumenting cvc5 to log its reasoning following a novel proof calculus. - Sums of Squares (Parrilo). This method reduces the unsatisfiability of a universally quantified nonlinear formula to finding sums-of-squares decompositions of polynomials via semidefinite programming. Although incomplete, the approach naturally produces a certificate in the form of a polynomial identity, which is very cheap to verify. The main challenge is that semidefinite programming solvers often suffer from numerical imprecision due to floating-point arithmetic; the proof checker must therefore attempt to repair any incorrect certificate. Such certificates have already been explored in prior work within HOL Light. We are investigating this technique as a solver for QF_NRA in cvc5. - Gröbner Basis (Tiwari). Similarly to Sums of Squares, this method aims to find a polynomial that certifies the unsatisfiability of the input formula. The result known as Positivstellensatz guarantees that, under certain conditions, such polynomial must be present in the elements of the Gröbner Basis of the input. This method uses a set of extension rules to force such conditions to be met. It is thus a method complete relative to an oracle, which would decide which extension rule to apply in a given state. Checking the certificate produced by this method also requires tracking the variables introduced by the extension rules and proving a relationship between the produced polynomial (which may have fresh variables) and the input polynomials. We are likewise prototyping it inside cvc5. The four algorithms span a useful dichotomy: incremental linearization and CAD are well-established inside SMT solvers but there are real challenges to check its results; the witness-based methods are more exploratory on the solver side, but the produced certificates have a cheap overhead to be computed and are straightforward to verify.

ABSTRACT. Bit-vector solving is essential to many practical applications of Satisfiability Modulo Theories (SMT) solvers. Currently, most state-of-the-art SMT solvers handle this theory by means of bit-blasting: After simplifications, the input formula is converted into an equisatisfiable formula in propositional logic, which has its satisfiability decided by a SAT solver based on resolution, which is known to handle counting and modular reasoning poorly. Unfortunately, arithmetic bit-vector operators produce large CNF encodings, especially for multiplication, whose refutations can be exponential in size. One alternative is to reason at the word level via polynomial constraints, solved using computer algebra techniques, that can be captured by the Polynomial Calculus (PC). However, this approach does not handle general reasoning well. Pseudo-Boolean (PB) solvers reason with cutting planes, a proof system that can polynomially simulate resolution and is exponentially stronger on some of the arithmetic structure of bit-vectors, while avoiding the difficulties PC has with bit-level reasoning. This suggests that converting bit-vector constraints into PB constraints rather than propositional clauses could yield smaller proofs and potentially faster solving. An analogous strategy of translating bit-vectors into integer arithmetic has already shown such gains on increasing bit-widths. Liew et al. proposed an approach to verify properties of bit-vector multiplication based on pseudo-Booleans, via cutting-planes proofs, presenting a construction of optimal polynomial-size proofs for a class of bit-vector multiplicative identities. In this work, we plan to extend this approach to the context of SMT solving by developing a novel proof-producing decision procedure based on blasting to PB constraints, leveraging external PB solvers. We are implementing this in the cvc5 SMT solver, building on its extensive infrastructure for proof logging, which produces proofs in the Cooperating Proof Calculus (CPC) and Alethe proof formats; as the PB solver we use RoundingSat, which produces cutting-planes proofs in the veriPB format. So far we translate all operators of the fixed-size bit-vector theory of SMT-LIB except bit-shifts, division and remainder, discharging the resulting constraints to RoundingSat. Proofs of the decision procedure will combine cutting-planes reasoning with a justification of each translation step to PB constraints; we are extending Alethe and CPC to capture them, and their respective proof checkers Carcara and Ethos to verify them. In the talk we will detail the encoding strategy used for the operators we already cover, the obstacles posed by bit-shifts, division and remainder, and how the cutting-planes proofs produced by RoundingSat can be lifted into Alethe and CPC for checking by Carcara and Ethos.

ABSTRACT. For line-based propositional proof systems, there is a default way to extend them to proof system for quantified boolean formulas (QBF). For static proof systems, there is no such default method. Most known static proof systems are algebraic or semi-algebraic, like the Nullstellensatz, Sherali-Adams and Sum-of-Squares proof systems. For these proof systems, extensions to proof systems for QBF were defined and studied by Beyersdorff et al. (SAT 2025). In this paper, we define and study an extension to a QBF proof system of the - to the best of our knowledge - only known pure Boolean static proof system, the hitting proof system. This proof system was introduced by Kullmann (Dagstuhl 2012) and first studied in detail by Filmus et al. (ITCS 2024).

ABSTRACT. Automatic prompt optimisation is a challenging black-box combinatorial problem central to deploying large language models (LLMs) at scale. Existing generation-based methods ignore concrete failure patterns of the current prompt, while iterative editing methods suffer from premature convergence. We introduce LEAP (Local–global Exploration for Automatic Prompting), a two-stage framework alternating between a convergence stage—targeted editing guided by verbal error feedback and multi-parent beam search—and an escape stage that activates upon stagnation and leverages the full optimisation history to generate structurally diverse candidates. On four NLP benchmarks against six baselines, LEAP achieves a mean composite score of 0.485, outperforming the nearest competitor by 7.1%.

ABSTRACT. Agent safety in high-stakes domains requires formal policy enforcement, but most existing approaches either rely on probabilistic guardrails (prompt-based steering; fine-tuned classifiers, e.g., Llama Guard \cite{inan2023llamaguard}) that offer no formal guarantees, or on hand-coded symbolic enforcement that does not scale to the breadth of real policy specifications. In this paper, we present an alternative approach: an autoformalization pipeline that translates natural language agent prompts, MCP tool descriptions, and policy documents into formally verified policies via an LLM-based generator-critic loop. These policies run in a deterministic policy harness external to the agent, which evaluates agent actions against these formal policies to decide whether those actions should be permitted. We use Cedar as our policy language, which is formally analyzable by SMT solvers \cite{cutler2024cedar}. This work draws inspiration from the LLM Modulo framework \cite{kambhampati2024llmscantplanhelp} and neurosymbolic AI. On the MedAgentBench benchmark, our autoformalized policies cover substantially more of the natural language policy than the hand-coded symbolic enforcement in prior work. We have open sourced the external harness with support for several agent scaffolds, alongside custom Cedar language bindings in Python.

ABSTRACT. Assessing quantitative properties of probabilistic programs, like e.g. almost sure termination, is often an undecidable problem. It is, therefore, interesting to identify classes of programs for which these problems become tractable. In a paper to be presented at LICS 2026 (https://arxiv.org/abs/2604.27986) we have shown that the weighted relational model of linear logic can be used to translate (Positive) Almost Sure Termination ((P)AST) for Probabilistic Higher-Order Recursion Schemes (PHORS) into a problem involving generating functions. Then, by using algebraic properties, we have identified a class of PHORS (extending Li et al.’s affine PHORS) whose corresponding generating function is algebraic, making the (P)AST problems decidable. In this abstract, we show that this framework is also fruitful for different quantitative problems and other classes of programs. In particular, we consider two types of quantitative problems: exact inference (i.e. computing the posterior probability distribution generated by a program) and computing the termination probability of a program. To consider inference, we consider Boolean PHORS, a variant of PHORS having a type for the booleans. We then present a typing system that ensures the generating function of a (Boolean) PHORS is either rational or algebraic. In the rational case, we show that exact inference for (Boolean) PHORS is computable and that not only (P)AST is decidable, but the exact value of the probability of termination can be computed in polynomial time. In the algebraic case, we show that we can compute an approximation up to any desired precision of the posterior distribution.

ABSTRACT. We investigate a formula-based approach for updating ABoxes in DL-Lite (ℋℱ) horn, a description logic that enjoys a low computational complexity of reasoning. Specifically, we extend the existing coherence update semantics from DL-Lite (ℋℱ) core to deal with conjunctions on the left-hand side of TBox axioms, which introduce ambiguity in the update result. We address this problem by proposing the new prioritized coherence update semantics that employs rankings over conjuncts to select among competing updates while preserving the central properties of minimal change, syntax independence, and uniqueness. We further show that updated ABoxes can be computed via a stratified Datalog¬ program based on a novel consequence-based calculus. The approach runs in polynomial time, matching the complexity of standard reasoning in DL-Lite (ℋℱ) horn.

ABSTRACT. The literature on ontology-mediated query answering (OMQA) has been shaped by two key results: first-order rewritability for DL-Lite, and PTime hardness of data complexity for essentially every description logic beyond it. This has effectively positioned DL-Lite as the only practical choice for query rewriting, restricting OMQA solutions to first-order queries and ontologies that can be rewritten into them. This AC0--PTime dichotomy is especially limiting if we consider that OMQA targets graph-structured data, and that standard graph query languages (including the recent ISO standards GQL and SQL/PGQ) are typically NL-complete. Towards identifying a rich Horn DL that can be rewritten into graph query languages and that can still express many ELI and DL-Lite ontologies, we introduce a stratification mechanism for ELI^\bot that controls the interaction between conjunction and recursion. In this way, we obtain ELI^\bot_\preceq, a description logic that strictly extends the core DL-Lite, supports reachability axioms and restricted conjunction, and allows for reasoning in NL. We establish the NL upper bound via a rewriting into nested two-way regular path queries, a fragment of GQL, providing initial evidence that our ontology language is a promising candidate for extending OMQA to graph query languages.

ABSTRACT. In this extended abstract, we summarize our recent work (to appear at KR 2026) on the complexity of deciding whether a given fact is relevant to a Boolean conjunctive query (CQ), i.e. whether the fact belongs to some minimal subset of the data that makes the query hold. Despite being of central importance to query answer explanation, the combined complexity of deciding query relevance has not been studied in detail, leaving open what makes this problem hard, and which restrictions can yield lower complexity. Relevance has previously been shown to be harder than query evaluation: namely, Sigma^p_2-complete for CQs, even over a binary signature. We further observe that NP-hardness applies already to (acyclic) chain CQs. Our work identifies self-joins (multiple atoms with the same relation) as the culprit. Indeed, we prove that if we forbid or bound the occurrence of self-joins, then relevance has the same complexity as query evaluation, namely, NP (without structural restrictions) and LogCFL (for bounded hypertreewidth classes). In the ontology setting, we establish an analogous result for ontology-mediated queries consisting of a CQ and DL-Lite_R ontology, namely that relevance is no harder than query answering provided that we bound the interaction width (which generalizes both self-join width and a recently introduced ‘interaction-free’ condition). Our results thus provide useful insights into what makes relevance harder than query evaluation and allow us to identify natural classes of queries which admit efficient relevance computation.

ABSTRACT. We extend concurrent game structures with a simple notion of preference over computations and define a minimal notion of rationality for agents based on the concept of dominance. We use this notion to interpret a CL and an ATL languages that extend the basic CL and ATL languages with modalities for rational capability, namely, a coalition's capability to rationally enforce a given property.

ABSTRACT. Recent work in the field of multi-agent systems has sought to apply techniques and concepts from formal methods to provide rigorous theoretical analysis and guarantees for complex systems in which multiple agents strategically interact, thereby creating the field of equilibrium analysis, also called rational verification. The main goal of equilibrium analysis is to study the complexity-theoretic properties of equilibria and solution concepts for multiplayer games in game theory, as a way to reason about the overall system in a precise, mathematical manner. Multi-agent systems, however, are complicated mathematical objects that consist of multiple different components. Therefore, even specifying deterministic multi-agent systems, the focus of this paper, is a non-trivial matter. In this paper, we argue that issues of representation create a recurring issue in the literature that we call the model gap. This model gap issue often causes issues for researchers wishing to provide complexity-theoretic lower bounds. We further argue that the model gap issue can be resolved by representing multi-agent systems implicitly, using circuits to compute functions.

ABSTRACT. Alternating-time temporal logic (ATL or more generally, ATL*) is a logic for reasoning about computational models of multi-agent decision-making. It mainly deals with strategic capabilities of agent coalitions in multi-player games. Whilst ATL* is useful for the specification and verification of multi-agent systems, it needs further extensions for modeling human players because they usually have to make decisions with uncertain and vague information. As probability calculus is the standard approach to model uncertain information, there have been some probabilistic extensions of ATL. However, in real-world situations, forms of incomplete information are diverse. Hence, in this paper, we propose another two extensions of ATL* to accommodate incomplete information. On one hand, the possibilistic ATL* can represent and reason about uncertainty arising from imprecise predictions of outcomes caused by agents' actions in terms of possibility theory. On the other hand, the many-valued ATL* facilitates the representation and reasoning of fuzzy events. In both extensions, we introduce the syntax and formal semantics of the proposed logics.

ABSTRACT. We use Alternating-time Temporal Logic to study strategies in classical reachability turn-based sabotage games. We extend the usual scope of sabotage games with a liveness version of the game and with concurrent sabotage games. We relate our temporal approach to the graph-theoretical notion of minimal $s{-}t$ cut, and propose its dynamic counterpart. Finally, we indicate how epistemic extensions of ATL and ATL$^{\ast}$ can be useful in studying imperfect-information sabotage games.

ABSTRACT. We study multi-modal logics applied to multi-agent systems modelled by concurrent game models (CGMs) where the commonly assumed principle of independence of agents' actions need not hold. In reality, this principle is often violated by various physical, normative, or other natural constraints on the possible, or admissible, combinations of actions that may be executed by the agents. This motivates the study of variants of CGMs with constraints on the admissible action profiles. We consider three natural approaches for implementing such constraints. The first two allow the agents to choose actions simultaneously, where non-admissible action profiles respectively block or deadlock the system. The third approach requires agents to choose actions sequentially in some priority order, and only presents each agent with choices of actions that do not conflict with previously made choices by other agents, thus making it impossible to select a non-admissible action profile. These approaches are modelled by variants of CGMs. To formalize reasoning in each of them, we introduce suitable conservative extensions of Alternating-time Temporal Logic (ATL, ATL*). For most of these logics, we have shown that they have the same complexity of model checking and satisfiability decision as their ATL/ATL* bases, and proposed complete axiomatic systems.

ABSTRACT. Deep reinforcement learning produced adversarial agents capable of superhuman performance. The opacity of these policies creates critical barriers to auditability. Conventional distillation methods make this worse; by focusing on replicating teacher-replay data, they sacrifice robustness at the learner-induced decision frontier—the very states where interpretability matters most. To address this, we introduce an Auditable Composite Distillation on a Sparse Tactical Frontier (AIRD), a composite-policy framework that decomposes these regimes. AIRD employs a human-interpretable nominal tree to govern routine states and a model checking step handles frontier states for introducing residual corrective policy. This architectural separation resolves distribution mismatch at a structural level, eliminating the need for retraining. As a first testbed, we audit Connect4 5x6 environment and show that AIRD extends the safe planning horizon from 8 to 10 play and reduces opponent-attractor states by 47%.

ABSTRACT. Neural networks for vision are widely used but do not provide explanations for their decisions. A recent approach (e.g., ConSpec) uses concepts to bridge the gap between pixel-like features and human-understandable text, and a propositional logic to express specifications of the model's behavior. However, such approach remains limited and cannot express simple properties involving multiple concepts, predicate on their strength (a proxy for the presence of a concept in the input), or predicate on multiple input images. This limitation is mostly due to the non-linear relationship between concepts' strengths and the latent space representation of the model, which makes satisfiability checking difficult and restricts the application of the logic to explain the network's decisions. We propose Concept Parts Network (ConPNet), a novel architecture that integrates the concepts' strengths computation directly into a classifier and then uses these strengths for prediction. Such architecture allows us to extend ConSpec to support arbitrary linear combinations of concepts' strengths (ConSpecReal), which are necessary to express a wider range of specifications, and efficiently check them with an SMT solver. Our initial experiments show that ConPNet retains competitive classification efficiency and supports effective explanation of predictions through ConSpecReal formulas.

ABSTRACT. State-of-the-art SAT solvers from the SAT Competition are all using a local search component. Experimentally at the beginning of the search, many better assignment are found; so we developed a new method to not store those each time, based on caching flips. This method was already part of Kissat but was not described so far. We also describe the implementation in CaDiCaL which reuses watch lists instead of using full-occurrence lists. Finally, we ported the new \tassat algorithm to CaDiCaL improving the performance of CaDiCaL.

ABSTRACT. Local Search (LS) solvers for SAT can surpass CDCL solvers on some prominent satisfiable industrial and combinatorial benchmarks. They operate by flipping variable assignments and maintaining per-variable scores incrementally to guide variable selection, so performance is largely determined by how efficiently each flip is executed. We revisit a largely forgotten data structure that reduces per-flip overhead by eliminating costly clause scans. We dub this scheme NobleCount, integrate it into the leading LS solver ProbCCAnr, and evaluate it on industrial FCC spectrum-repacking instances and the SC22 anniversary track, two standard testbeds for modern LS solvers. ProbCCAnr with NobleCount achieves new state-of-the-art results on both benchmarks. On FCC, where it already overtook not only other LS solvers but also leading CDCL solvers, employing NobleCount further reduces PAR2 by 24.8% at a 20s timeout, with consistent PAR2 gains across all timeouts up to our final 300s timeout. On SC22, at longer timeouts where another LS solver, TaSSAT, originally overtakes ProbCCAnr, NobleCount lifts ProbCCAnr to outperform TaSSAT in PAR2 score.

ABSTRACT. Solving hard combinatorial problems such as the minimum Kochen-Specker problem requires finding all solutions to large Boolean satisfiability (ALLSAT) formulas, pushing the limits of existing parallel solver infrastructure. We present ams-dist, a new distributed hybrid solver that combines Cube & Conquer and portfolio solving. Building on AlphaMapleSAT-CnC, ams-dist introduces four key improvements: a fully distributed MPI manager-worker architecture, a portfolio clause-sharing simplification phase in which groups of workers collaboratively simplify subproblems in parallel, a distributed beam lookahead cubing procedure with a balanced scoring objective, and a progress-based work-stealing policy during the conquering phase that uses irredundant clause count to estimate subproblem difficulty. These improvements maintain substantially higher core utilization throughout execution compared to the baseline AlphaMapleSAT-CnC. We evaluate ams-dist on Kochen-Specker instances of orders 17-22 on a computing cluster at up to 3072 cores, comparing against the distributed pure portfolio solvers painless and MallobSat. ams-dist achieves consistent speedups of 1.5-3× on tractable instances and is the only solver to solve order-22 instances within a 6-hour timeout.

ABSTRACT. Majority Inverter Graphs (MIG) have been shown to be an excellent basis for circuit representation. However, no Circuit-SAT solvers that accept MIGs natively exist currently. Current Circuit-SAT solvers operate only on AND, OR, and XOR gates, not majority functions. Furthermore, majority gates are difficult for traditional CDCL solvers to tackle due to their large Tseitin transformation. This paper introduces a new CDCL Circuit-SAT solver, named MIGSat, that can efficiently operate on the majority basis by employing novel techniques, including: (1) a watchlist mechanism for the Majority function, (2) an efficient BCP mechanism, including a MiniSat-style blocker for the majority function, (3) a Tseytin clause derivation method for conflict analysis of the majority function, and (4) a MIG specific branching heuristic based on EVSIDS. We also implemented versions of existing heuristics, like LBD and activity-based clause deletion and clause simplification, to improve performance. Lastly, we demonstrated that our solver generally matches the performance of MiniSat on Miter circuits, and can be significantly faster than MiniSat and Kissat on Pigeonhole Circuits. Although still limited in its raw solving power, MIGSat can serve as a foundation for additional research in Circuit-SAT on the MIGs.

ABSTRACT. In higher education, activity-based teaching has become increasingly popular as an alternative or complement to lecture-based teaching. The topic-swapping peer-teaching classroom activity is as follows: first, each student acquires a topic; then, over rounds, they form pairs to swap their acquired topics within the pair until each topic has been acquired once by each student. The idea behind the topic swapping activity is for students to: (1) acquire knowledge about each topic and (2) interact with many students. The topic-swapping activity can be formulated as a constrained optimisation problem (COP). An optimal solution to the COP is where (1) each formed student pair is unique and (2) each student acquires a novel topic each round (one they have not had previously). We have modelled the topic-swapping activity COP in the MiniZinc modelling language. From our findings, constraints (1) and (2) often conflict, resulting in no such optimal solution. Additionally, our experiments show that finding solutions even for small instances is difficult.

ABSTRACT. At a wedding, a seating plan can satisfy capacity limits, grouping requests, separation requests, and balance constraints while still leaving a guest at a table with little shared ground for conversation. This paper introduces Table Talk Tuning (TTT), a small constraint modelling problem drawn from a real wedding-seating case. The name points to the part of the task that ordinary seating constraints leave implicit: giving each guest at least one plausible conversation topic shared with enough tablemates. TTT uses guest topic scores to prefer tables where each guest has a strongest shared topic that enough tablemates can sustain together. The conversation score is optimised after structural terms for table slack and gender balance, so social fit becomes part of the seating objective rather than a post-processing check. We present a MiniZinc model, three synthetic instance families from 10 to 150 guests, a reproducible benchmark pipeline, and a native Gecode implementation for studying objective-aware search. The experiments compare MiniZinc solvers and native search strategies. They show that the conversation terms change the returned seatings on matched instances, and that objective handling matters in practice even when the underlying model is fixed.

ABSTRACT. Planning domains are usually represented in first-order logic. However, historically, most of the planners have been using grounded problem representations. Since grounding can lead to a combinatorial explosion, and thus make some problems intractable, the community has developed techniques to deal with hard-to-ground problems. Those techniques include, for example, splitting action schemas, or partially grounding actions to relevant instantiations for the goal at hand. Recently, a new family of planners which work directly on lifted representations has emerged. However, most of these so-called lifted planners still rely on grounding to some extent. With the aim of broadening the range of approaches to lifted planning, in this work we present a satisfiability-based lifted planner that works on first-order representations and does not rely on grounding at all. We encode the lifted planning task into a quantifier-free formula with uninterpreted functions, in first-order logic with equality. Despite showing higher solving times than the state-of-the art, the planner proves to consume very little memory and is competitive on hard-to-ground instances.

ABSTRACT. Auto-grading student constraint models requires a checker to validate candidate solutions against the problem specification. In practice, for example in the Coursera MOOC on MiniZinc, the checker is developed separately from the teacher's own constraint model. This duplicates effort and risks inconsistencies that produce confusing feedback and unfair grades. We present a framework for CPMpy in which the checker is automatically derived from the teacher's constraint model. By adding a feedback template to each constraint, granular feedback is returned when a student solution violates a specified constraint, domain, or objective. Decision variables in the teacher's model that are intentionally hidden from the student are assigned consistently via a Maximal Satisfiable Subset computation. The same model also provides a performance baseline for grading, generates instances of various difficulty, and can be obfuscated and distributed for local checking. We illustrate the approach on an example Flexible Jobshop Scheduling project, demonstrating violation detection on a toy instance, and checker performance on larger instances.

ABSTRACT. Operational game semantics are presented through labelled transition systems, of which the induced bisimilarity on programs is shown to be included in CIU equivalence, a variant of contextual equivalence. Soundness of operational game semantics follows from external context lemmas which state that CIU and contextual equivalences coincide. This talk will show how one may avoid the use of CIU equivalence entirely, by changing the initial operational configurations of terms in the operational game semantics. The construction is inspired by a proof technique for the genericity lemma due to Takahashi.

ABSTRACT. We study contextual interactions in an ML-like language equipped with general references and continuations through the lens of operational game semantics, focusing on the reachability and approximation problems. Previous work showed that these problems are decidable in the loop-free setting via automata over nested data, where bounded P-views admit a finite representation. With the addition of loops, however, P-views become unbounded, and these techniques no longer apply. We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data, together with new restrictions of the P-view: the shallow P-view and enriched shallow P-view. These provide a finite representation of the relevant visible fragment of unbounded traces. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops. This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

ABSTRACT. We discuss how to solve whole hierarchies of behavioral equivalence problems as single quantitative problems about modal logics through energy games. My work on generalized equivalence checking of concurrent programs proposes the first unified way to check for whole ranges of equivalences. Its prototype implementation https://equiv.io can compute which notions from van Glabbeek's strong and weak linear-time–branching-time spectrum relate pairs of finite-state processes.

ABSTRACT. This is a proposal for a talk concerning some technically easy yet little-known observations. I previously presented this material briefly in a talk at Università Roma Tre in May 2019, but it is not written down anywhere other than my slides. My apologies for the paucity of drawings in this hastily prepared abstract.

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

ABSTRACT. We implement an agentic approach that improves constraint models. It receives a CPMpy model and three small training instances as input, autonomously creates and tests alternative CPMpy models, and outputs the variant that it considers best-performing within about fifteen minutes. We then evaluate the proposed model on three larger test instances. Our experiments on nine combinatorial optimization problems show that the generated models outperform the original models on 20 out of 27 test instances (74\%), demonstrating that autonomous agentic methods can support the improvement of constraint models.

ABSTRACT. Recent works in Constraint Programming (CP) have investigated how Large Language Models (LLMs) can assist in model formulation from natural language problem descriptions, lowering the barrier to modelling. However, even when a model is correct, solver performance remains highly sensitive to modelling choices. Formulating high-performance models that effectively prune the search space requires expertise and manual trial-and-error, through techniques such as symmetry breaking, redundant constraints, or global constraint reformulation. In this work, we explore the potential of LLMs to assist in the model optimisation process. We present and evaluate an LLM-guided iterative framework that takes an initial constraint model and a natural language problem description as input, and produces a semantically equivalent but computationally faster model. Each step of the iterative process includes a model evaluation on a set of training instances to assess the candidate model before using it in the next generation, which additionally includes solver feedback (runtime/UNSAT/error etc.). We systematically evaluate our approach on a set of diverse combinatorial problems from CSPLib, and across various strategies that configure the context at each iteration.

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

ABSTRACT. We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT, implementation through Codex prompts, and repeated LLM-assisted code audits and revisions. Although the codebase implements several algorithms and solver components, our evaluation focuses on configurations that combine core-guided optimization, lightweight preprocessing, core minimization, integration with integer linear optimization backends, and a new core-sequence lookahead approach. Our experience suggests that LLMs can support solver implementation from papers, while requiring external validation, benchmarking, and human guidance. In our experiments, fuzzing and MaxSAT Evaluation instances did not reveal wrong answers in the tested configurations, although performance remains below the best hand-engineered MaxSAT solvers. We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.

ABSTRACT. Intelligent agents interacting with their environment need to reason about the effects their actions will have on their surroundings. For actions with deterministic outcome this problem is well investigated in the context of planning problems. But many real-world actions may not always result in their typical outcome, and exceptional outcomes of an action have to be taken into account. In this work we present a framework for reasoning about actions with uncertain outcomes. Inspired by conditionals, we introduce defeasible action rules that capture the typical outcome of action, without committing to what happens in exceptional circumstances. As semantics of these rules we introduce uncertain transition schemas: graph-based representations of transitions between possible worlds in which edges between states are assigned a rank indicating their typicality. We define an inference operator for defeasible action rules inspired by rational closure, adapting its intuitive semantics to the dynamic setting. Furthermore, we explore a generalization of this framework that uses partial or total orderings over transitions instead of ranks. This generalization strictly increases expressive power and enables more refined reasoning operators. Finally, we extend the language of defeasible action rules with a notation to express that certain properties are not affected by the execution of an action, thus allowing to explicitly formulate frame axioms in this defeasible setting.

ABSTRACT. Action reversibility deals with the problem of whether and under what circumstances we can undo effects of a given action. Recent works established the notions of action reversibility in the propositional settings. Action reversibility represents whether, for each state of concern, effects of an action can be undone by some action sequence. The present paper studies the concept of action reversibility in lifted STRIPS settings that represent the environment by first-order predicates and define action schemas defined over those predicates. In particular, we define the notions of lifted reversibility and lifted uniform reversibility. Although undecidable in its most general form, due to the undecidability of first-order logic, we show that several results from the propositional settings can be generalized to the lifted settings.

ABSTRACT. We introduce a new exponential modality for coherence spaces that can "count up to 2". Its Kleisli category provides an interesting example of finitary yet intensional semantics of the simply typed λ-calculus. The eventual goal is to present this semantics using an intersection type system, and derive a corresponding notion of graded resource approximants, with a view towards applications to higher-order transducers.

ABSTRACT. By 'enriching' the usual sequent calculus of linear logic over the reals, additives and multiplicatives can be interpreted as addition and multiplication. We thus obtain Quantitative Linear Logic (QLL). Besides the technical curiosity, this creates a bridge between structural methods (chiefly linear logic) and quantitative ones. We support this claim in various ways, and invite the community to further explore this newfound connection. The talk is based on recent work joint with Atkey, Komendantskaya, and Grellois, as well as with Flinkow, Komendantskaya, and Monahan.

ABSTRACT. We present a polymorphic Linear lambda-calculus as a proof language for second-order intuitionistic Linear Logic. The calculus is extended with scalar multiplication and term addition, which enable the proof of a linearity result at the syntactic level. The syntactic linearity yields a correspondence between proof-terms and linear functions. We develop a sound and adequate denotational semantics based on hyperdoctrines valued in semimodule-enriched Linear categories.

ABSTRACT. In an introductory programming class using, e.g., Python, students are often asked to modify sample programs under specific coding constraints so that the modified programs prompt the printing of expected results by means of print statements in the sample programs. In grading the submitted programs, checking only the correctness of the required printing is insufficient, as it cannot detect unacceptable computational behaviors, deceptive printing, and/or violations of coding constraints. In this paper, we propose a method to support the grading of introductory programming assignments based on the comparison of rewrite sequences of rewrite systems obtained from a pre-prepared answer program and students' submitted programs. In our method, both the answer program and submitted programs are transformed into logically constrained rewrite systems, respectively, and their rewrite sequences from the same initial state for the required execution of the assignment are compared. This enables us to detect differences in execution, such as the use of different constructs or incorrect loop conditions.

ABSTRACT. Code fusion, also called deforestation, is a compiler-optimization technique that removes intermediate data structures. Though it has been studied in the literature for over 30 years, it is rarely used in production compilers due to the many challenges that automatic deforestation faces. We believe that many of these issues can be solved if we think about deforestation as an interactive process instead. In this work-in-progress report, we describe the user-controlled system we envision and give preliminary results from working on it. More specifically, we present a small, domain-specific language for deforestation and give intuition for the way many of previous deforestation techniques can be expressed in it.

ABSTRACT. The effectiveness of SAT solvers depends critically on how constraints are encoded into conjunctive normal form (CNF). Two logically equivalent encodings of the same problem can differ by orders of magnitude in solving performance. However, constructing effective encodings often requires substantial expertise, making SAT technology difficult to use reliably in practice. To address this problem, a wide range of reencoding techniques have been developed that transform formulas into representations exposing stronger propagation, improved simplification opportunities, or additional structural information. Unfortunately, most existing proof systems are designed for clause-level reasoning and provide only limited support for certifying such higher-level transformations. Several examples illustrate the need for proof-producing reencoding. First, the way XOR constraints are encoded as CNF can have a surprisingly large impact on SAT-solving performance. Even subtle changes in recursive encodings can lead to substantial performance differences. In particular, placing auxiliary variables at the beginning versus the end of the recursion, often referred to as linear and pooled encodings, respectively, can strongly affect solver behavior. Such transformations are difficult to justify compactly because they replace one structured encoding by another while preserving equivalence only over the original variables. Second, the effectiveness of cardinality encodings depends not only on the chosen encoding scheme, but also on how literals are ordered within the constraint. Recent work has shown that sorting literals prior to encoding can substantially improve SAT solving performance by exposing additional structure to propagation and simplification. Although such sorting transformations preserve the semantics of the original constraint, they are difficult to validate in existing proof systems because the resulting encoding may differ globally from the original one. In particular, the transformation changes the interaction between auxiliary variables and the input literals while preserving equivalence only over the original variables. This highlights the need for proof systems that can certify semantic-preserving reencodings with higher-level constraints. Third, symmetry breaking in SAT is constrained by what is visible in the CNF formula. When higher-level constraints such as cardinality or XOR constraints are encoded into CNF, auxiliary variables may obscure the symmetries of the original problem. As a consequence, symmetry-breaking techniques operating only at the CNF level may fail to detect important structural symmetries that were present before encoding. This talk argues that the widespread use of CNF as the standard SAT benchmark format creates a fundamental tension between solver performance and trustworthiness. Many effective preprocessing and reencoding techniques rely on recovering higher-level structure from CNF formulas, such as XOR or cardinality constraints, and then transforming these constraints into more solver-friendly representations. However, these transformations raise important certification questions. Should CNF formulas be lifted into richer high-level representations together with corresponding proof objects? If so, how can these high-level representations and proofs be translated back into CNF-level certificates that can be checked independently? Alternatively, should correctness be justified directly at the CNF level without introducing higher-level abstractions? This talk addresses these questions and discusses possible directions for integrating proof logging, reencoding, and high-level reasoning into trustworthy SAT-solving pipelines.

ABSTRACT. Pseudo-Boolean proof logging is now being used for a wide range of problems that are not naturally pseudo-Boolean. This is very useful for verifying complex algorithmic and reasoning steps being carried out by solvers, but there is still an encoding gap: why should we trust that the pseudo-Boolean model means the same thing as whatever problem the user cares about? And, for that matter, does the solution as expressed over Boolean variables correspond to the high-level solution that we claim? For a variety of subgraph-finding problems, Gocht et al. introduced end-to-end verification, starting with a HOL description of the problem and verifying the meaning of the output in graph terms. There, the final verification theorem does not mention the pseudo-Boolean intermediaries or how the VeriPB proof system works. In this talk, we discuss what it would take to get a similar process to work for constraint programming, building upon the VeriPB proof logging methodology introduced in the Glasgow Constraint Solver. We will explain what we are aiming for and why we want it; why the problem is complicated; how we've chosen to try to address it; and what remains to be done. Ultimately, we would like to be able to go from human-understandable problem statements written in several domain-specific languages, all the way to solutions, whilst having extremely strong guarantees that the solutions are correct.

ABSTRACT. Recently, we have seen many advances in proof logging methods for CP solvers. However, by design, proof logging is agnostic to how the solver produces a proof. For example, it does not verify that an individual propagator achieves its advertised level of consistency. This potential source of bugs may lead to misleading empirical conclusions about new propagation algorithms. We propose a runtime certification framework to address this gap. Propagators emit certificates that justify both the retention and the removal of values in domains. These certificates are checked at runtime by checkers that are significantly simpler than the propagation algorithms. We make the existential definitions of consistency levels constructive. At fixpoint, a propagator must be able to produce a witness for any relevant value (bounds for bounds-consistency; domain values for domain-consistency). If it cannot provide a witness for a specific value, it did not propagate to its advertised consistency level. To certify removal of values, every value removal and conflict must be accompanied by an explanation. Explanations are checked for soundness and applicability (i.e., whether they are applicable in the current state). This is closely related to checking a proof step, but done at runtime against the live solver state rather than post-hoc. Finally, we introduce the notion of weak consistency for propagators that are neither bounds- nor domain-consistent (e.g., timetabling for cumulative, prevent-and-check for circuit). A weakly-consistent propagator removes those values that, when assigned to a variable, trigger a detectable conflict. This gives us a verifiable property applicable to many practical propagators that previously lacked consistency properties. We implemented propagation certificates in Pumpkin, with checkers for linear inequality, maximum, element, cumulative (timetabling), and circuit (prevent-and-check). Enabling all checkers results in a 1–2 order-of-magnitude slowdown in our experiments. However, only running checkers for a single propagator type (the realistic development scenario) substantially reduces this overhead. Using this framework, we identified and fixed several consistency bugs in propagators in Pumpkin. In addition, manually injected off-by-one mutations were also caught within one second of solve time.

ABSTRACT. In this talk, I will present a generalisation of conflict-driven clause learning (CDCL) for constraint programming over abstract domains. A core idea in constraint programming is propagation: each constraint has an associated algorithm that during search prunes potential non-solutions. The abstract theory of constraint propagators as idempotent, monotonic, contracting functions over partial orders has led to the development of propagators and solvers over non-integer domains, such as strings, sets or floating point numbers. Building on this theory, I introduce a generalisation of reasons, explanations, and implication graphs from CDCL to propagation-based solving over abstract domains. A central result shows that cuts in the implication graph are no-goods. An abstract scheme is presented that unifies CDCL solving from SAT and lazy-clause search from constraint programming. This work is a first step to generalising proof logging for abstract domains in constraint programming.

ABSTRACT. A constraint programming (CP) solver that implements proof logging will output a machine-checkable certificate of correctness alongside any result it obtains. This is useful for trusting claims of unsatisfiability or optimality, as well as for debugging and auditing solver implementations. Proofs can be constructed by having the solver log justifications for each inference it makes, and previous work has shown that many standard CP reasoning techniques can be efficiently justified using a pseudo-Boolean (PB) proof format. Multiplication constraints of the form $X \times Y = Z$ are a fundamental primitive for CP modelling, but they pose a unique challenge for PB proof logging, given their non-linear nature. In this talk, I will present an overview of how multiplication constraints can be encoded as $0$-$1$-linear inequalities, and then how bounds-consistent reasoning can be justified using the \emph{VeriPB} proof format. We will see that this is possible to achieve, but comes with significant costs in terms of proof logging and checking overhead. I will then discuss what this means for certified CP more broadly, and some ideas for making PB proofs of this nature more usable and efficiently checkable in practice. This talk will be mostly based on the previously published paper, "Certifying Bounds Propagation for Integer Multiplication Constraints" and a short version was presented at AAAI in 2025.

ABSTRACT. In this work, we propose a knowledge compilation language for quantified Boolean formulas. We show that the language is capable of efficiently solving important QBF queries like satisfiability, model counting, MaxQBFs, and conjunctions. We also present an algorithm to compile an equivalent representation in the target language for a given QBF. Finally, we discuss some strengths and limitations of the proposed language.

ABSTRACT. Conventional notions of equivalence for quantified Boolean formulas (QBFs) consider only free variables, even though quantified variables are also relevant in many settings. Therefore, we investigated solution-based notions of equivalences that properly reflect the semantics of quantified variables. We encoded the resulting equivalence checking problem itself as a QBF and used this to implement QSOLE, the first fully automatic checker for solution-based QBF equivalence. This talk provides a summary of our work on solution-based QBF equivalences and how they can be checked.

ABSTRACT. Toda's Theorem is a fundamental result in computational complexity theory, whose proof is based on a reduction from a QBF problem with a constant number of quantifiers to a model counting problem. The recent progress in model counting tools raises the question of whether this reduction, henceforth called Toda's reduction, can be utilized to construct a practical QBF solver. This question follows a line of research that revisits theoretical results from an algorithmic aspect, thus brings new theoretical and engineering challenges. For Toda's reduction these challenges arise mainly because the reduction is purely theoretical and based on ideas that are entirely orthogonal to the search-space approach used by current QBF solvers. In this work, we address this question by transforming Toda's reduction into a concrete probabilistic QBF solver that uses model counting as an oracle. A naive implementation is hopeless due to a massive formula blow-up. Therefore we next identify three main factors that drive the blow-up. While we present solutions that overcome some of the factors, we also show that one of them, the union bound factor, largely overlooked in the literature, is in fact dominant and in some cases unavoidable. We then show how for some cases, even this factor can be avoided, and report our preliminary results on a prototype implementation.

ABSTRACT. Reactive synthesis asks for a system satisfying a given LTL specification. Bounded synthesis translates the specification to a universal co-Büchi automaton and then searches for systems of increasing size. For each size, a constraint system asserts the existence of an implementation of that size whose product with the automaton has no rejecting run. Faymonville, Finkbeiner, Rabe, and Tentrup (2017) compared SAT, QBF, and DQBF encodings of bounded synthesis and concluded that, despite being the most concise, the DQBF encodings lost to QBF because DQBF solvers were not yet competitive. Nine years on, we run a similar comparison with current state-of-the-art DQBF solvers. DQBF has narrowed the gap considerably but, in our experiments, still trails the QBF pipeline. When compared to new reactive synthesis tools, bounded synthesis has fallen behind. This gap is not entirely a solver issue: many instances are lost in the initial LTL-to-automaton translation. Encodings that bypass the automaton construction are therefore a natural target for future work.

ABSTRACT. Robust classification is commonly understood as the stability of a classifier under small perturbations (often adversarial) of input data. In this paper, we propose a logical framework for robust classification grounded in topological semantics for modal logic. Evaluation points are feature vectors representing machine-readable objects, and formulas express explicit classifications. Robustness is interpreted geometrically as local truth persistence: a classification is robust at a point if it holds throughout some non-empty open neighbourhood of that point. Building on this perspective, we introduce a logical language with a robustness modality interpreted over S4 topological spaces, together with a novel robustness-sensitive conditional connective. This conditional connective captures global inclusion relations between robust regions and other properties of the classifier: it holds at a point when the neighbourhood witnessing the robustness of one formula is contained in the truth set of another. In this way, robust classifications can be systematically linked to classification conditions. We provide a sound and complete axiomatisation of the resulting logic. Finally, we introduce Minimal Robust Models, a constructive method for generating models from specified robustness constraints. This yields formal tools for analysing, explaining, and structuring robust classification behaviour.

ABSTRACT. In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), ob- tained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic (M⊃), as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its correctness, showing that the resulting Boolean circuit faithfully characterizes the validity of the encoded DLDS. A Lean formalization establishes machine-checked guarantees of this correspondence, providing a certified link between proof compression and circuit-level verification. This approach opens new perspectives for automated theorem proving and formal certification.

ABSTRACT. Developing software for formal mathematics is straightforward since the problem and the method of solution are clearly defined. But then the software is also intended to be used by students and/or pupils and it turns out (as is well known from commercial products) that the user interface requires several times the development effort compared to the backend. This demonstration shows that the proof assistant Isabelle possesses generic functionalities that allow an existing backend to be connected to the state-of-the-art user interface Isabelle/jEdit with a reasonable amount of effort.

ABSTRACT. We present Rocq Game, a web-based educational tool designed to support interactive learning with the Rocq proof assistant. The system provides a setup-free, browser-based environment leveraging jsCoq, combining gamified progression, structured learning paths, and real-time proof feedback. Rocq Game separates pedagogical content from application logic through a lightweight domain-specific language, enabling instructors to create modular learning materials efficiently. Initial classroom deployment in a type theory course indicates that the tool lowers the entry barrier to proof assistants while maintaining the expressive power of Rocq.

ABSTRACT. For line-based propositional proof systems, there is a default way to extend them to proof system for quantified boolean formulas (QBF). For static proof systems, there is no such default method. Most known static proof systems are algebraic or semi-algebraic, like the Nullstellensatz, Sherali-Adams and Sum-of-Squares proof systems. For these proof systems, extensions to proof systems for QBF were defined and studied by Beyersdorff et al. (SAT 2025). In this paper, we define and study an extension to a QBF proof system of the - to the best of our knowledge - only known pure Boolean static proof system, the hitting proof system. This proof system was introduced by Kullmann (Dagstuhl 2012) and first studied in detail by Filmus et al. (ITCS 2024).

ABSTRACT. Compiling constraint models to conjunctive normal form (CNF) is commonly regarded as a one-way transformation, since auxiliary variables and clausal decomposition obscure the original problem structure. Related methods of structure recovery include gate extraction and cardinality detection, but those recover only fragments, not the complete encoding. We present an autonomous agent, powered by an LLM, that reverse-engineers a complete, semantically equivalent PySAT encoding from a DIMACS CNF file. We use a SAT-based equivalence checker to verify the high-level encoding and obtain counterexamples for iterative refinement. The agent queries the formula through bounded analysis tools. It combines structural with abductive reasoning to hypothesize the underlying combinatorial problem. We evaluate our approach on several combinatorial problems with instances generated by independent encoders (PySAT, Picat, Sugar, BEE), giving the agent no metadata. We obtain 85 reconstruction on 48 instances and demonstrate that the agent handles direct, order, and log encodings of the same problems. Our scaling study confirms feasibility up to 1.2 million clauses.

ABSTRACT. In The Art of Computer Programming, Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen’s graph: the minimum number of colors needed to color the squares of an n x n chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis substantially by comparing thousands of encodings for the same problem, thereby identifying additional factors that are important for solver performance. We obtain 1584 encodings for this problem by varying (a) the constraints that encode which color is assigned to each cell, (b) the constraints that forbid the same color appearing in a row, column, or diagonal line, and (c) the symmetry-breaking constraints. We find that the three most impactful encoding factors are (i) the choice of symmetry-breaking constraints, (ii) enabling so-called clique hints, and (iii) enforcing that each cell is assigned exactly one color through blocked clauses. Furthermore, while Knuth proposed clique hints as an advantage of the order encoding, we show in fact that they can be effectively employed for the one-hot encoding as well.

ABSTRACT. We introduce power term polynomial algebra, a representation language for Boolean formulae designed to bridge conjunctive normal form (CNF) and algebraic normal form (ANF). The language is motivated by the tiling mismatch between these representations: direct CNF↔ANF conversion may cause exponential blowup unless formulas are decomposed into smaller fragments, typically through auxiliary variables and side constraints. In contrast, our framework addresses this mismatch within the representation itself, compactly encoding structured families of monomials while representing CNF clauses directly, thereby avoiding auxiliary variables and constraints at the abstraction level. We formalize the language through power terms and power term polynomials, define their semantics, and show that they admit algebraic operations corresponding to Boolean polynomial addition and multiplication. We prove several key properties of the language: disjunctive clauses admit compact canonical representations; power terms support local shortening and expansion rewrite rules; and products of atomic terms can be systematically rewritten within the language. Together, these results yield a symbolic calculus that enables direct manipulation of formulas without expanding them into ordinary ANF. The resulting framework provides a new intermediate representation and rewriting calculus that bridges clause-based and algebraic reasoning and suggests new directions for structure-aware CNF↔ANF conversion and hybrid reasoning methods.

ABSTRACT. In standard concurrent game models, the set of available actions for agents at each state is fixed. In real-world scenarios, however, this assumption rarely holds. The actions available to an agent at a given state often depend on various constraints, which can be external (objective) or internal (subjective). For instance, one agent’s choice of an action may affect another agent’s available actions; selecting a goal may change an agent’s action set; adopting a particular strategy may alter the set of feasible actions. Strategic reasoning in such settings thus frequently involves changes of agents’ available actions. In this work, we introduce a logic for local strategic reasoning with dynamic action contexts, designed to capture reasoning that involve such changes. Related frameworks include logics using strategy contexts, logics for strategic reasoning in social scenarios, logics for conditional strategic reasoning, and strategy logics. Our logic introduces four dynamic operators: adding action constraints, action choice, constraint relaxation, and full action-resetting. Formulas of the logic are evaluated over a tuple (M, s, AC), where M is a standard concurrent game model, s is a state, and AC is an action context specifying the available actions for each agent at every state. The four dynamic operators are interpreted as local updates of the action context. The logic is expressive and versatile: various other operators, well-known or new, can be defined in the language.

ABSTRACT. The paper presents the logic of local nested conditional abilities, allowing for formal reasoning about what coalitions can achieve, conditional on others acting conditionally on yet others, etc. A two-sorted formal language NConStR is introduced, interpreted over concurrent game models, in which such nested conditional abilities of coalitions can be expressed. It is demonstrated that NConStR can be embedded into Local Basic Strategy Logic (LBSL) via a recursive translation, establishing that LBSL is at least as expressive as NConStR. This embedding allows for the transfer of known metalogical results from LBSL — such as decidability and axiomatizability — to NConStR.

ABSTRACT. Humans can often achieve their goals by delegating sub-goals/tasks to other agents. They may do this without knowing the details of other agents' strategies or getting agreement on a joint strategy. Instead, they use their knowledge about other agents' abilities and make assumptions about others' cooperativeness to synthesize their own individual strategy which uses delegation and handles possible interference between it and that of others. In this paper, we examine how we can formalize such subjective/first-person reasoning about ability under imperfect information as a kind of subjective strategic reasoning under cooperativeness assumptions in a multi-agent epistemic situation calculus with strategic operators.

ABSTRACT. The same arguments often need to be evaluated under different external regimes. An agent with influence over the regime has a strategic lever that standard formalisms do not directly capture. We introduce context-dependent argumentation frameworks (CDAFs), an extension of Dung's theory in which a defeat function determines, per context, which attacks succeed. A perspective-labeled specialisation derives the defeat function from a relevance set $\rho$ and a priority $\pi$. The relevance set is the agent's action space. In a small worked example, the agent's target argument is rejected under every full-relevance injective priority, yet accepted under a partial activation that no VAF audience can mirror. We define the corresponding decision problem, ACTIVATION-MANIPULATION, and record baseline complexity bounds. Tight bounds and multi-agent variants are left open.