ABSTRACT. We present a sound and complete unification procedure for deterministic higher-order patterns, a class of simply-typed lambda terms introduced by Yokoyama et al. which comes with a deterministic matching problem. Our unification procedure can be seen as a special case of full higher-order unification where flex-flex pairs can be solved in a most general way. Moreover, our method generalizes Libal and Miller's recent functions-as-constructors higher-order unification (FCU) by dropping their global restriction on variable arguments, thereby losing the property that every solvable problem has a most general unifier. In fact, minimal complete sets of unifiers of deterministic higher-order patterns may be infinite, so decidability of the unification problem remains an open question.

ABSTRACT. Treating syntactic equality as a logical connective---governed by left- and right-introduction rules within the sequent calculus---offers an elegant and powerful approach to term identity. This treatment of equality allows for the derivation of core mathematical principles, such as Peano’s axioms (excluding induction), and serves as a foundation for the Abella interactive proof assistant. However, integrating this equality into automated proof search remains challenging. We present a proof search procedure that extends unification to handle the complexities of quantifier alternation and equations that occur in both positive and negative occurrences. While established logical frameworks such as lambda Prolog and LF lack direct support for this kind of equality, our procedure enables a lightweight logical framework that addresses this gap. Our system enables unification-aware proof search across a diverse range of first-order sequent calculi that can directly use this form of equality.

ABSTRACT. Building on the small-model constructions for Åqvist’s deontic logics (E, F, F+(CM), and G), we present Deo-SMT, an SMT-based reasoner implemented in Z3 for validity checking and countermodel generation. These logics correspond to well-known conditional systems: F+(CM) extends Preferential Conditional Logic with reflexivity and absoluteness, while G corresponds to Lewis’s VTA. Deo-SMT provides countermodel visualizations as text, matrices, and directed graphs. It outperforms the existing Isabelle/HOL approach and offers a lightweight, user-friendly interface for normative reasoning.

ABSTRACT. We describe grind, an SMT-inspired proof automation tactic for Lean 4. Unlike hammer-style tools that translate proof obligations into external logics and invoke external ATP and SMT solvers, grind works natively in the Calculus of Inductive Constructions, producing kernel-checkable proof terms without any soundness compromises. At its core, grind combines congruence closure for dependent type theory with E-matching and a suite of satellite solvers for linear integer arithmetic, linear arithmetic over ordered modules, polynomial equations over commutative (semi)rings, and associative-commutative operators. Each satellite solver is parameterized by Lean's typeclass mechanism, enabling it to operate over any type implementing the appropriate algebraic interface rather than only hardcoded numeric types. Users can extend grind with new theory solvers through a plugin API, control theorem instantiation through a constraint system on E-matching patterns, and inspect the internal state through an interactive mode with a domain-specific language for navigating the solver. An annotation system with automatic pattern selection enables libraries to declare how their theorems should be used by grind. The tactic ships with Lean and is used extensively in Mathlib, CSLib, and major formalization projects including the Prime Number Theorem formalization and Terence Tao's formalization of Analysis I.

ABSTRACT. We present a formalized theory of context-free grammars and their links to finite automata. In particular we focus on first-time formalizations of an executable translation into Greibach Normal Form, the Chomsky-Schützenberger Representation Theorem and Parikh's Theorem.

ABSTRACT. A string diagram is a two-dimensional graphical representation that can be described as a one-dimensional term generated from a set of primitives using sequential and parallel compositions. Since different syntactic terms may represent the same diagram, this syntax is quotiented by a collection of coherence equations expressing equivalence up to deformation. This work lays foundations for automated reasoning about diagrammatic equivalence, motivated primarily by the verification of quantum circuit equivalences. We consider two classes of diagrams, for which we introduce normalizing term rewriting systems that equate diagrammatically equivalent terms. In both cases, we prove termination and confluence with the help of the proof assistant Isabelle/HOL.

ABSTRACT. Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.

ABSTRACT. In this paper, we present the first proof-of-concept framework for end-to-end formally verified graph generation. Our approach integrates SAT modulo symmetries with the Lean proof assistant, providing a unified, machine-checked verification pipeline that spans high-level graph-theoretic specifications, propositional encodings, symmetry-breaking mechanisms, and solver-based search. By formalizing graph invariance and symmetry reasoning within Lean, we eliminate common trust assumptions and obtain fully certified non-existence results. We evaluate the framework on three benchmark classes of graph-generation problems, showing practical feasibility on nontrivial unsatisfiable instances.

ABSTRACT. Both higher-order logic and dependent types are popular features for languages used for the formalization of complex domains. Recently DHOL was introduced as a language that provides the expressivity of dependent types while retaining the general feel of higher-order logic. Since then multiple extensions and theorem provers have been developed, and DHOL was adopted as the first TPTP standard for using dependent types in automated theorem provers. However, the literature lacks a model theoretical semantics for DHOL. The present paper fills in this gap. It introduces both standard models and Henkin models and proves soundness and completeness. Considerable care went into keeping the formulation as close to the usual definitions for FOL and HOL and thus most intuitive. However, we had to make a significant generalization to Henkin models for HOL in order to obtain completeness in the presence of dependent types. Our results will allow for extending semantic methods for HOL to DHOL and can serve as a model-theoretical reference point for showing the equivalence of theorem provers.

ABSTRACT. This paper presents a certified theorem prover for Grzegorczyk logic (Grz) implemented in the general-purpose proof assistant HOL Light. Our prover builds on original HOL Light formalisations of modal adequacy for Grz with respect to finite partially ordered frames, and on the standard full and faithful translation of Grz into Gödel–Löb logic (GL). This formalised embedding allows us to extend the range of modal systems supported by the HOLMS library for automated modal reasoning, and constitutes a new methodology experimented in our framework, being the first logic added to the library through a modal translation. The deductive engine performs an automated proof search in the labelled sequent calculus for GL. When the proof search on the translated formula succeeds, the system returns a HOL Light theorem certifying provability of the original Grz formula. When proof search terminates negatively, the system constructs a verified GL countermodel and thus certifies that the original formula is not provable in Grz.

ABSTRACT. In recent years, numerous techniques were developed to automatically prove termination of different kinds of probabilistic programs. However, there are only few automated methods to disprove their termination. In this paper, we present the first techniques to automatically disprove (positive) almost-sure termination of probabilistic term rewrite systems. Disproving termination of non-probabilistic systems requires finding a finite representation of an infinite computation, e.g., a loop of the rewrite system. We extend such qualitative techniques to probabilistic term rewriting, where a quantitative analysis is required. In addition to the existence of a loop, we have to count the number of such loops in order to embed suitable random walks into a computation, thereby disproving termination. To evaluate their power, we implemented all our techniques in the tool AProVE.

ABSTRACT. We investigate the uniform fluted fragment, a subfragment of the fluted fragment obtained by imposing the uniformity restriction on Boolean combinations. First, with a novel trick in model construction, we prove that the uniform fluted fragment has an exponentially bounded model property. It follows that, unlike the full fluted fragment (where satisfiability is non-elementary), satisfiability in this subfragment is NExpTime-complete. Second, we formulate a bisimulation for the subfragment, and establish a characterization of its expressive power in the style of van Benthem. Finally, we show that the uniform fluted fragment is equi-expressive with the uniform forward fragment (if we consider only sentences), and that satisfiability in the latter is also NExpTime-complete.

ABSTRACT. Kleene algebras are an algebraic abstraction of regular expressions, one of the central notions in computer science. While the equational theory of Kleene algebras is known to be decidable, reasoning from finite sets of hypotheses (Horn theory) quickly becomes undecidable. This happens even for simple classes of hypotheses which themselves do not involve Kleene star. One of such classes of hypotheses is formed by sum-of-letters hypotheses, of the form $a \leq b_1 + \ldots + b_k$, where $a, b_1, \ldots, b_k$ are letters. In the present paper, we strengthen the undecidability result proved for this class of hypotheses by Doumane et al. (2019) and establish the exact complexity --- $\Sigma^0_1$-completeness. Moreover, we strengthen our result and show the same complexity bounds for one fixed set of sum-of-letters hypotheses. We also accompany this result with a decidability one, for comparison.

ABSTRACT. Automatically identifying temporal properties from observations of a system's behavior provides valuable insight into that system's inner workings. Temporal properties are often expressed in temporal logics, such as Computation Tree Logic (CTL). Existing approaches to learning CTL specifications from observations rely on constraint-solving by encoding the search for formulas into a satisfiability problem that perfectly separates observations that the system can (positive) or cannot (negative) perform. While adequate in noise‑free settings, these methods often struggle with noisy data, such as incomplete executions or mislabeled traces, and scale poorly to large inputs. To overcome these limitations, we propose a neural approach for learning CTL specifications from positive- and negative-labeled observations represented as transition systems. Our method employs a neural network in which neurons encode the presence of CTL operators at specific positions. After training, a deterministic extraction procedure converts network weights into interpretable CTL formulas. In contrast to satisfiability‑based learning approaches, our framework efficiently produces high‑quality specifications even under noisy data conditions. It supports arbitrary CTL formulas up to a user-defined size budget and consistently yields accurate results within short computation times, demonstrating that neural architectures can provide a fast and noise-tolerant method for inferring temporal properties.

ABSTRACT. Natural-language proof assistants such as Naproche and our own system Natty can translate a mathematical text in controlled natural language into a series of logical formulas to be verified. Natty also contains an automatic prover that is designed to quickly verify formulas representing proof steps. Natty's prover is based on superposition, but uses a variety of techniques that are unusual for superposition-based provers, including commutative unification and a form of rewriting that sometimes preserves the rewritten clause. To evaluate this prover and others, we have produced a test suite called TextbookMath containing over 150 theorems and their proofs, which we transcribed from a classic number systems textbook by Mendelson into N, the controlled natural language of Natty. Natty can read this text and generate a set of over 900 conjectures of higher-order logic, each corresponding to a single proof step in the original Mendelson text. We find that established high-order provers such as E and Vampire can prove only about 85\% of these conjectures using a single strategy with a 5-second timeout. Surprisingly, some of the conjectures they fail to prove look relatively easy and should be provable with only a few superposition steps. Natty's automatic prover can prove about 91\% of these conjectures under a similar time restriction. If we expand the Mendelson text with various intermediate proof steps and lemmas, Natty can completely verify a textbook development of the natural numbers, integers and rationals including 5 of Wiedijk's well-known list of 100 theorems.

ABSTRACT. We present an implemented reasoner for fuzzy order-sorted feature (OSF) logic, supporting fuzzy unification and normalization of OSF terms modulo a sort theory. Fuzzy OSF logic is a knowledge representation and reasoning language based on feature symbols, denoting functions, and sort symbols, denoting fuzzy sets. Sort symbols are organized in a fuzzy subsumption relation that extends to OSF terms, record-like structures representing classes of entities. The unification algorithm for these structures provides a calculus of fuzzy type subsumption. We demonstrate the system's behavior on representative examples, such as computing the membership degree of an instance to a sort, and computing subsumption degrees between sorts and OSF terms. We also report a comparison with a resolution-based fuzzy logic programming system.