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.
Certificates are machine-checkable witnesses that help increase confidence in verification results by providing independently verifiable evidence beyond a simple yes/no answer. In this short paper, we present two certificate checkers for hardware model checking, Certifaiger and Cerbtora, which target bit-level and word-level verification of hardware designs, respectively. Certifaiger has been adopted in recent editions of the Hardware Model Checking Competition, but not described in the literature before. Cerbtora extends the same theoretical framework to the word level, in which certificates are expressed in the same modeling language as the design under test and are validated using efficient automated reasoning engines. We describe the architecture and main components of both tools and evaluate them on competition benchmarks.
We present an Isabelle/HOL formalization of the 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.
This paper introduces Pgeon, a meta-prover framework that generates tableau-based automated theorem provers from declarative specifications. In Pgeon, the syntax of a given calculus, its tableau inference rules, and the proof-search strategy are described in a small domain-specific language that closely follows textbook presentations. From such a specification, Pgeon instantiates a fully functional prover, handling tableau construction, rule instantiation, branching, and backtracking in a logic-agnostic manner. Proof-search is driven by a strategy engine that gives users explicit control over exploration order while keeping logical content separate from operational concerns. Pgeon supports first-order reasoning through binders, capture-avoiding substitution, and extensible term generators required for Skolemization and free variable introduction. We describe the design of the specification language, the execution model of the tool, and the strategy mechanism, and illustrate the approach on case studies covering classical first-order tableau calculus and intuitionistic propositional calculus.
We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity assignment and reification, to overcome difficulties in handling partial and variable application.
SMT solvers are used in many safety-critical applications. To provide evidence of the correctness of their answers, some SMT solvers generate externally checkable proof certificates. We present a high-performance checker for SMT proof certificates called Ethos. In contrast with other dedicated SMT proof checkers, Ethos does not implement a fixed proof calculus. Instead, it allows users to specify their own calculus in the declarative language Eunoia, which extends the familiar SMT-LIB syntax to make that easy and convenient. We give a short overview of Eunoia and then focus on Ethos itself. We describe multiple optimization and implementation details which make Ethos fast and practical. We also evaluate Ethos on proofs generated by cvc5, showing that the flexibility of Ethos allows us to efficiently check fine-grained proofs, containing no proof holes, over all SMT-LIB logics without floating point arithmetic.
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 typeclasses, enabling it to operate over any type that implements the appropriate algebraic interface—not just hardcoded numeric types. Users can extend grind with new theory solvers through a plugin API, control theorem instantiation through instantiation constraints on E-matching patterns, and inspect the internal state through an interactive DSL. An annotation system, including automatic pattern selection, enables libraries to declare how their theorems should be used by grind. The tactic is distributed as part of Lean and is used extensively in Lean’s Mathlib [19] and CSLib [2] libraries.
Eunoia is a logical framework designed for specifying the proofs and proof systems of SMT solvers, namely cvc5. We present a translation from a core fragment of Eunoia to the λΠ -calculus modulo rewriting as implemented by the LambdaPi proof assistant. The translation is implemented by our tool eo2lp, which we use for generating LambdaPi encodings of (a) a large fragment of the Cooperating Proof Calculus (CPC), the Eunoia signature defining cvc5’s proof system, and (b) proofs produced by cvc5 on unsat problems from various fragments of SMT-LIB.
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.
This paper proposes a novel automatic abstraction-refinement procedure for verifying hyperproperties. Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of standard temporal properties. Our verification procedure is based on predicate abstraction and the recently introduced reduction of hyperproperty verification to satisfiability of Constrained Horn Clauses (CHCs). Moreover, it formalizes and uses CHC-based refinement for abstract counterexamples in the shape of directed acyclic graphs. We implemented our new algorithm on top of the SMT solver Z3. Our experimental evaluation shows our automatic abstraction refinement procedure can solve a variety of hyperproperty verification problems, completely automatically. This is in contrast to other existing techniques that require a user-given abstraction.
In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.
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.
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.
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
Building on the small-model constructions for Åqvist’s deontic logics introduced in [24], we present Deo-SMT, an SMT-based reasoner implemented in Z3 for checking validity and generating countermodels. Deo-SMT covers all four of Åqvist’s logics (E, F, F+(CM), G) and provides countermodel visualizations as text, matrices, and directed graphs. Our tool outperforms the existing Isabelle/HOL approach, while providing a lightweight and accessible interface for normative reasoning.
The fluted fragment lacks the Craig Interpolation Property. In this paper we establish a weakened form of interpolation. Given an entailment in the fluted fragment, we distinguish predicates that only take an argument sequence starting with x_1 from those that do not. A predicate of the former kind is allowed to appear in a weak interpolant only if it occurs in both the premise and the conclusion; and any predicate of the latter kind can be used in a weak interpolant no matter whether it is in the shared signature. Our proof also shows that the weakened interpolation holds in every finite variable subfragment of the fluted fragment. In addition, this work provides a generalization of A. Herzig’s translation of the ordered fragment, as well as a new proof of the finite model property of the fluted fragment.
We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the π -calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm. We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.
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 ≤ b_1 + … + b_k , where a, b_1, … , 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— ^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.
We report on the new ARI infrastructure that supports tools and competitions in term rewriting. It offers ARI-COPS, a database for confluence problems and competition results, and ARIWeb, a convenient web interface for tools that participate in the annual confluence competition. These are built on top of the new ARI format for rewrite systems, a format converter, certifiers for competition results, and a duplicate checker.
We present a sequent calculus for Scott’s theory of classes founded on positive free logic. Cut elimination, the generalised subformula property and consistency are shown to hold, also in the intuitionistic variant. Eventually the calculus is extended to cover the original Zermelo’s set theory Z without the axiom of choice by means of (systems of) rules. The calculus for Z preserves cut elimination, moreover, some of its subsystems and extensions are also provably consistent.
