ABSTRACT. First-order logic extended with Henkin quantifiers is not recursively enumerable, even for the simplest Henkin quantifier that is not definable in first-order logic. Despite this, such quantifiers arise naturally in the analysis of partially ordered quantification, motivating partial proof systems suitable for automated reasoning. We present a tableau-based proof system with unification for first-order logic extended by the simplest Henkin quantifier. The system is derived from a second-order function calculus but avoids second-order unification by internalizing dependency structure via side-variable and weak regularity constraints.

ABSTRACT. We report on our efforts to translate HOL-Light theorems on HOL-Light types/functions into Rocq theorems on Rocq types/functions. To this end, we developed in Rocq tactics to automate the proofs required for replacing a HOL-Light inductive type or recursive function definition by an equivalent but more idiomatic one in Rocq. We also explain how we replaced the definition of real numbers, as well as a number of mathematical notions like R^n spaces and the definition of limit, hence providing to Rocq users many definitions and theorems in logic and analysis that had not been formalized in Rocq before.

ABSTRACT. Hyperproperties, which express system behaviors that relate multiple execution traces, cover a variety of important safety and secu- rity properties. Among these, hyperproperties of the form ∀∃.φ, where φ is an invariant or a SafetyLTL formula, capture many practically rele- vant specifications including noninterference, symmetry, and robust path planning. Despite their importance, efficient verification algorithms for such properties remain limited. In this paper, we propose novel verifica- tion algorithms for such ∀∃-hyperproperties. Our approach extends classical induction and k-induction techniques, widely used in single-trace verification, to the hyperproperty setting. We develop hyper-inductive reasoning principles that generalize the base and step cases of induction to sets of traces, refinement techniques to strengthen the property, and incremental approaches to increasing the bound of the k-induction. As a byproduct, we introduce hyper-(k)-inductive invariants, as certificates to witness satisfaction of ∀∃-hyperproperties over transition systems. We evaluate our approach on various bench- marks, demonstrating that our methods are complementary to state-of- the-art hyperproperty model checkers, and we analyze in which cases one option prevails over the others.

ABSTRACT. Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), and SCL(T).

ABSTRACT. We introduce a new family of benchmarks for the problem of diagrammatic equiva- lence between circuits. Three variants of this problem are considered, ranging from basic to challenging, and benchmarks are generated for each variant. We provide first-order encodings in both TPTP and SMT-LIB formats, together with scripts that automatically generate benchmark instances. We evaluate these benchmarks on state-of-the-art auto- mated theorem provers and SMT solvers, highlighting the impact of encoding choices on solver performance.

ABSTRACT. We study the cycle-detection problem for affine single-path linear-constrained loops over the integers. A cycle is a finite execution that returns to its initial state. Cycle detection is a natural relaxation of termination: every cycle witnesses non-termination, while an infinite execution need not contain a cycle.

We prove that cycle detection for affine integer loops belongs to $\Sigma_2^P$. The proof relies on the algebraic structure of periodic vectors of the update matrix. Using the cyclotomic factors of its characteristic polynomial, we obtain a polynomial representation of the periodic subspace and of exponentially distant states along a periodic orbit. We then apply a small-integer-solution theorem to show that, whenever a cyclic state exists, one exists with polynomial bit-length. Consequently, cycle existence can be expressed by existentially guessing such a state and universally quantifying over a polynomial-size binary encoding of a position in its orbit, with the resulting predicate decidable in polynomial time.

ABSTRACT. We present a PSPACE-complete fragment of first order logic we call QEALM (QBF-like EPR by Alternating Level-ordered Miniscoping). Unlike other well-known fragments it is more analogous to QBF (Quantified Boolean Formulas) because it has game-like alternations and can be restricted to complete problems for the polynomial hierarchy. QEALM is a natural first order analogue to QBF just as EPR (Effectively Propositional logic) is a first analogue to Dependency QBF.

In this paper we prove the PSPACE and Polynomial Hierarchy completeness theorems of QEALM among other nice properties such as closure under Robinson's resolution and retained hardness after intersection with Schaefer fragments. We use our new definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.

ABSTRACT. A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP benchmark. We experimentally study the impact of the approach across several ITP-derived benchmark sets and its interaction with theorem proving strategies.

We find that while the neural guidance consistently improves performance within individual benchmark domains, cross-benchmark application of guiding models underperforms the plain default strategy. The picture when considering combined strategies is less clear-cut, indicating persisting value of neural guidance but under diminishing returns.

ABSTRACT. We present a system for generating intermediate lemmas, used as cut formulas, that restructure first-order proof search in saturation-based theorem provers. Given a CNF problem, a heterogeneous graph neural network encodes clauses, literals, terms, variables and symbols. An autoregressive decoder then samples candidate lemmas by pointing to symbols in the input and by obeying arity constraints during decoding. Candidate lemmas are accepted when an ATP proves both sides of the cut, i.e. the problem extended with the lemma and with its negation. Together with adjustable criteria for proof-search speedup this gives a supervised learning signal and a learning-proving feedback loop.

We train and evaluate the methods on ATP datasets built from the Mizar Mathematical Library with both E and Vampire. On the E test set, the best single configuration helps 96 of 187 baseline-proved problems, while an ensemble helps 127 67.9%, with speedups up to 196x. We also show that a cut generator trained on the E data transfers to Vampire: when the cuts are delivered as AVATAR claims, Vampire proves 501 hard Mizar problems unsolved by Vampire or E before, and speeds up 2236 further problems. In combination with trained Deepire and Vampire's CASC mode, the learning/conjecturing/portfolio methods discussed here prove 1228 Mizar problems unsolved by Vampire or E before.

ABSTRACT. Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean 4 formalization covering both deterministic and stochastic models. We first formalize Hopfield networks -- recurrent networks that store patterns as stable states -- and prove their convergence, and the correctness of Hebbian learning, the rule that updates parameters to encode patterns. We then turn to stochastic networks, whose probabilistic updates converge to a stationary distribution: we formalize the dynamics and learning of Boltzmann machines and prove their ergodicity -- convergence to a \emph{unique} stationary distribution -- via a new formalization of the Perron--Frobenius theorem.

ABSTRACT. Symmetry breaking in graph search problems remains challenging: complete symmetry breaking constraints are typically exponential in size, while partial approaches trade pruning strength for scalability.

We introduce a strength-driven, redundancy-aware methodology for constructing compact partial symmetry breaking constraints based on graph patterns. Each pattern corresponds to a simple clause over equality literals and can be integrated directly into CP or SAT models.

Our approach incrementally selects strong, non-redundant patterns, yielding partial symmetry breaks that achieve substantial pruning while remaining compact. This provides a principled framework for deriving lightweight symmetry breaking constraints beyond previously studied constructions.

We evaluate the proposed constraints on graph instances with up to 25 vertices using a redundancy ratio metric. The resulting partial symmetry breaks constitute only a small fraction of the size of complete symmetry breaking constraints, while delivering significant performance improvements across several graph search benchmarks compared to previously defined partial symmetry breaking methods.

ABSTRACT. Pattern-matching is the primary programming construct used to analyze the contents of algebraic data types in statically typed functional languages. Additionally, dependent types allow us to benefit from very precise information about data being processed. However, pattern-matching on dependent types turned out to raise surprisingly complex challenges, that have required more than two decades of intensive research to produce current implementations in Agda, Epigram and the Equations plugin of Rocq. Another popular tool among Rocq users is the historical inversion tactic which solves many use cases at the cost of a loss of control over the form of the programs obtained and some reliability issues. Both approaches in Rocq rely on intermediate equalities to produce a well-typed term in the underlying type theory, many of which turn out to be unnecessary. Alongside those tools, we believe that there is room for a complementary minimalist approach based on recent improvements of small inversions that generates explicit terms that are more readable and explainable. We present here this approach and its current automation implemented in MetaRocq.

ABSTRACT. Roel de Vrijer's assignment maps a simply typed \(\lambda\)-term to a measure whose numerical component drops after every \(\beta\)-contraction. We present that assignment as a compact Haskell program, which uses host-language functions for the functional component of the measure. We prove that the returned integer is in fact a decreasing bound on all subsequent reduction sequences.

ABSTRACT. Transition-based generalized Büchi automata (TGBAs) can be substantially more compact than equivalent Büchi automata and they are produced or processed by most state-of-the-art ω-automata tools. Research on complementation algorithms for ω-automata focuses mainly on standard Büchi automata, with a few recent exceptions. We present a complementation construction applicable directly to TGBAs based on the idea of “simple and optimal” Büchi automata complementation by Allred and Ultes-Nitsche. We also provide an upper bound on the size of the complement. The bound is asymptotically better than the upper bounds of other complementation approaches applicable to TGBA. Experimental evaluation shows that on complex TGBAs, our complementation clearly outperforms the complementation processes available in modern tools including Spot and Kofola.

ABSTRACT. Maslov's class K is a decidable fragment of equality-free first-order logic. It subsumes numerous classical decidable fragments, including the equality-free monadic fragment, the equality-free two-variable fragment, and the Gödel class. It also captures the more recently introduced equality-free uniform one-dimensional fragment. Introduced over 50 years ago, the class K has been studied in automated deduction, primarily through resolution-based methods. Despite this long history, basic properties of K remained poorly understood until recently, when NExpTime-completeness of satisfiability and the finite model property were finally established. However, the proofs are highly non-trivial and technically sophisticated.

We present considerably simpler proofs of NExpTime-completeness and the finite model property for K. Our approach is based on a novel Skolemization procedure tailored to K. Moreover, we extend the class K by allowing a distinguished binary predicate interpreted as an equivalence relation, and prove that the resulting fragment has a 2-NExpTime-complete satisfiability problem. Finally, we discuss the possible addition of equality to the class K.

ABSTRACT. We investigate the proof-theoretic structure of incorrect/incomplete proofs, that is, derivations containing syntactic errors or incomplete inferential steps that nonetheless preserve partial semantic validity. Building on Hilbert’s epsilon calculus, we formalize how such derivations can be corrected through semantic projection and weakest preconditions, leading to valid Herbrand disjunctions. We show that the epsilon calculus provides a natural framework for analyzing tolerance of falsity in proofs and for identifying conditions under which an incorrect proof can be semantically repaired. This approach extends Hilbert’s program beyond correctness, toward a logic of error and recovery. Moreover we show that the extended first epsilon theorem is false-tolerant.

ABSTRACT. Model-theoretic semantics comes with a computational counterpart: to check validity is to search for a countermodel, and tableaux, resolution, and satisfiability solvers make the semantics something one can run. Proof-theoretic semantics --- the younger paradigm in which meaning is given by inferential role rather than by denotation --- has no established counterpart. This paper proposes one: logic programming. We show that Sandqvist's base-extension semantics for intuitionistic propositional logic is executable in a precise sense. Bases are logic programs, and to each formula $\varphi$ we assign a goal $[[\varphi]]$ of a second-order hereditary Harrop language such that $\varphi$ is supported in a base $\mathcal{B}$ exactly when $[[\varphi]]$ is operationally derivable from $\mathcal{B}$ read as a program. The encoding is the Russell--Prawitz translation of the connectives with quantification restricted to atoms, and this restriction is not a limitation but the point: it is what the support clauses themselves demand. The correspondence is exact base by base, not merely at the level of validity, so that intuitionistic validity becomes the success of a single query against the empty program. Logic programming stands to proof-theoretic semantics as tableaux and satisfiability solvers stand to model-theoretic semantics.

ABSTRACT. Description Logics (DLs) are a family of formal languages used for representing and reasoning about structured knowledge in terms of concepts and their relationships. The expressive power of a DL depends on the constructors available for building complex concepts.

In this work, we investigate subsumption in the restricted description logic FL_⊥reg and the related fragments FL_reg, FL_⊥, and FL_0. These formalisms support value restrictions over role names, where the subscript reg indicates the use of regular expressions over roles.

Subsumption between two concept descriptions in FL_⊥reg and FL_reg is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. These results can be derived either from complexity bounds established for more expressive logics or from algorithms designed for harder reasoning problems.

We reprove the PSpace-completeness result and provide a new proof of ExpTime-completeness for FL_reg and FL_⊥reg with TBoxes via a novel reduction to parity pushdown games. Our algorithm relies only on the constructs available in these logics and may therefore be implemented more easily.

ABSTRACT. This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance of primo is achieved by a systematic literature survey, repeated profiling, and parameter tuning. The resulting solver outperforms the winner of the QF-LRA track of SMT-COMP 2026. This confirms that vibe-coding of automated reasoning tools will enable us to make great strides in the future.

ABSTRACT. We present a solver for $N$-Queens Completion puzzles in Lean~4 that applies collaborative neurodynamic optimization algorithms over discrete Hopfield networks or Boltzmann machines. We prove the translation from the puzzles to the networks correct, and implement the algorithms that search those networks inside the prover. We report experiments on a corpus of completable and blocked boards, against a backtracking baseline proved to return only completions.

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. We provide a translation from problems of the Thousands of Problems for Theorem Provers (TPTP) Problem Library to Lean expressions. This makes the TPTP Problem Library available as a benchmark set for proof automation tactics inside Lean. We evaluate our tool by comparing its performance with that of the Lean compiler on equivalent inputs. Furthermore, we use our tool to compare different Lean proof automation tactics.

ABSTRACT. Reactive systems interact with their environment and have to satisfy their specifications in all environments also in settings with partial visibility. Researchers have extensively studied settings in which assignments to some input signals are hidden throughout the interaction. We introduce and study {\em blinking synthesis} -- synthesis in settings in which the assignment to all input signals is hidden in some rounds of the interaction. Blinking synthesis is relevant for systems with sensor failures, communication disruptions, or scheduling constraints.

The input to the blinking synthesis problem includes, in addition to a specification language $L_\spec$ over the input and output signals, also a hiding language $L_\H$, describing behaviors that trigger hiding of input signals. The goal is to generate a system that satisfies $L_\spec$ in all environments that hide the assignment to input signals whenever the computation so far is in $L_\H$.

We show that while for LTL specifications the problem is 2EXPTIME-complete, a careful and parameterized analysis reveals it is harder than LTL synthesis: blinking synthesis of EXPTIME-complete for specifications given by deterministic automata and when one of its parameters, namely $L_\spec$ or $L_\H$, is fixed. We study cases where the hiding language $L_\H$ can be synthesized too, aiming to either reduce sensing costs or maintain privacy of the environment.

ABSTRACT. Substructural logics are defined by dropping some of the structural properties of intuitionistic logic such as commutativity (exchange), contraction, or weakening. Substructural logics with contraction and without weakening can have very high complexity: in particular, FLec, the Full Lambek calculus with exchange and contraction, is complete for the Ackermannian complexity class. Here, `Full' refers to the presence of additive (lattice) connectives; these are used to simulate zero tests in the lower bounding argument. Indeed, Schmitz (2016) showed that its multiplicative fragment Lec has much lower complexity: provability and deduction are 2EXPTIME-complete. In this paper, we investigate the effect of adding the standard modal rules K, 4, and T to this multiplicative setting.

We show that provability in Lec+K and Lec+4 remains in 2EXPTIME by extending Schmitz’s expansive BVASS argument. We also obtain Ackermannian lower bounds for Lec+K deducibility, by constructing a reduction from an expansive counter machine; the main point here is that the K rule can be used to simulate zero tests. Some of these results hold even in the presence of the T rule. Combined with known results, this yields a tight classification: Lec+K(+T) and Lec+4 provability is 2EXPTIME-complete, Lec+K(+T) deducibility is Ackermannian-complete.

ABSTRACT. We present a benchmark suite and an accompanying experimental study that assesses the capabilities of modern Automated Theorem Provers (ATPs) for hyperproperty reasoning. Existing tools for reasoning about hyperproperties typically rely on specialised model checkers or a custom encoding to satisfiability modulo theories (SMT) solvers or first-order provers. Our suite constitutes the first systematic collection of SMT-LIB encodings spanning hyperproperty satisfiability, model checking, and software verification via Constrained Horn Clauses (CHCs). Using this suite, we evaluate state-of-the-art ATPs, including SMT solvers and first-order theorem provers, that support both arithmetic and quantified reasoning. Beyond measuring how different solvers perform, we summarize lessons we learned on what makes a good encoding and solver configuration for hyperproperties. The benchmark suite, translation scripts, and experimental setup are released as an open artifact, enabling reproducible evaluation and providing a foundation for future improvements in automated reasoning about hyperproperties.

ABSTRACT. In this article, we present a formalization of a general many-sorted hybrid polyadic modal logic within the Lean proof assistant. We provide a machine-checked proof of its soundness theorem and demonstrate how specific formalisms can be derived as subsystems. To facilitate this, we implement a generic DSL that allows users to define many-sorted signatures using intuitive notation. We showcase the framework's versatility through several applications: an SMC-like language for program analysis, a logic for security protocols, and the modal system S5.

ABSTRACT. Control invariance validates that dynamical systems have a control input that preserves a given property at all times. This paper introduces a set of sound axioms and proof rules in differential dynamic logic (dL) that enable verification of control invariance. First, the scalar and vector comparison principles, relating a system of differential equations to a comparison system such that invariance properties can be established more easily, are axiomatized in dL. This axiomatization primarily utilizes differential ghosts, which are proof-theoretic generalizations of comparison systems. Next, with the comparison principles serving as the basis, comparison invariants are introduced, and sound axioms and proof rules are developed. Comparison invariants reduce the question of control invariance to a functional inequality on its Lie derivative for a suitable class of functions, moreover, the right choice of function can result in decidable arithmetic. Furthermore, the perennially popular control barrier functions (CBFs) used in safety-critical control are shown to be a special instance of comparison invariants. This yields an axiomatization of CBFs that leads to a dedicated set of proof rules. The rules allow for the verification of CBFs, which are traditionally used for synthesizing safe controllers without verification. Lastly, comparison invariants are shown to unify several other safety verification techniques, including Darboux invariants and differential invariants, further cementing their versatility.

ABSTRACT. We present RTEC_rct, an interval-based stream reasoning system. RTEC_rct inherits from its predecessor RTEC_s a compositional and associative sequencing operator. RTEC_rct extends RTEC_s with `Reasoning Cut-off Tuples' (RCTs), a mechanism allowing for monotonic output given a monotonic input. RTEC_rct is also equipped with a bookkeeping policy, guided by RCTs, that identifies the minimal information for correct reasoning. Our empirical, reproducible evaluation on real and synthetic data from three application domains demonstrates the efficacy of RTEC_rct.

ABSTRACT. The calculus ALASCA extends superposition-based saturation proving with reasoning in Uninterpreted Functions and Linear Real Arithmetic (UFLRA). As efficiency of saturation algorithms depend on literal selection, simplification, and redundancy elimination, this paper improves reasoning in Uflra by introducing theory-specific notions and methods for all of these techniques. The implementation of these methods in the first-order theorem prover Vampire shows substantial gains in every tested benchmark category, solving a number of problems previously unsolved by any system.

ABSTRACT. We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping theorem (OST) in the form of a specific novel precondition. This precondition requires the existence of a dominating function for the martingale expression, which is uniformly integrable; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the run-time of a linear loop, then we can automatically synthesize polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to be continuous and have unbounded support, which is a novel contribution to the field. We implemented and evaluated our method to symbolically compute upper and lower bounds for moments of program variables upon termination.

ABSTRACT. Boolos’ Curious Inference (BCI) is a well-known example of a class of first-order reasoning problems that require infeasibly many proof steps in a first-order proof calculus but exhibit short and elegant proofs in second-order (or higher-order) logic. Consequently, BCI remains intractable for contemporary first-order automated theorem provers. Although the original problem formulation is also beyond the capabilities of current higher-order provers, previous work by Benzmüller et al. demonstrates that augmenting the problem statement with suitable higher-order formulas allows these provers to succeed. Building on this work, we introduce a procedure for identifying and generating such candidate augmentations. This procedure is implemented in the new ciao tool. Using ciao as a pre-processing tool makes BCI fully automatically solvable for the very first time.

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 NxN chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis much further by comparing thousands of encodings for the same problem, which allows us to identify 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. Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 elementary identities. Surprisingly, Wilkie showed that the following identity is valid over the positive integers and yet does not follow from Tarski's axioms: \begin{align*} &\left((1+x)^y + (1+x+x^2)^y\right)^x \cdot \left((1+x^3)^x + (1+x^2+x^4)^x\right)^y = \\&\left((1+x)^x + (1+x+x^2)^x\right)^y \cdot \left((1+x^3)^y + (1+x^2+x^4)^y\right)^x. \end{align*} Gurevič gave an algebra on 59 elements that satisfies Tarski's axioms but not Wilkie's identity, and over the years several authors whittled down the size of such a countermodel, culminating in a countermodel of size 12 due to Burris and Yeats. On the other hand, Zhang proved that there is no countermodel with fewer than 11 elements. Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats. Moreover, we show that there are exactly 8,957,952 countermodels on 12 elements up to isomorphism and provide a simple classification of them. Our SAT approach outperforms dedicated tools for finding countermodels in equational theories, namely Mace4 and SEM. Furthermore, using autoformalization, we prove the correctness of our main result in Lean.

ABSTRACT. Large language models (LLMs) have achieved remarkable progress in formal mathematical reasoning. Mathematical competition problems fall into two broad types: theorem-proving problems ask for a proof of a fully specified statement, whereas answer-construction problems ask the solver to construct an answer object and prove that it satisfies the stated specification. Existing mathematical reasoning engines mainly target theorem-proving problems, yet answer-construction problems remain less studied. This setting is challenging because model capabilities are misaligned, with general LLMs better suited to answer construction and prover LLMs better suited to proof generation, and because Lean proof checking alone does not rule out inadmissible circular witnesses. To close this gap, we introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework for solving answer-construction problems in Lean. ECP uses general LLMs to perform bounded enumeration and construct candidate answers, and invokes prover LLMs to produce machine-checked proofs. ECP introduces admissibility checking to ensure that each answer is canonical and does not involve a circular argument. On PutnamBench and autoformalized MathArena answer-construction problems, ECP formally solves 17/346 and 18/75 answer-construction problem instances with admissible answers and proofs, respectively, outperforming LLM baselines at aligned inference budgets. Our code is available at https://github.com/sunjia72/ecp-lpar.

ABSTRACT. We describe the knowledge representation and proof search choices behind llmpipe, an English-to-logic question-answering pipeline. The system maps English assertions and questions to a controlled-predicate first-order representation, compiles it into prover-ready clauses, and uses GK, a saturation-based first-order prover extended for commonsense reasoning, to derive answers and render proofs back into English.

We distinguish between machinery that requires dedicated prover support, such as contradiction-tolerant search, numeric confidence handling, and defeasible reasoning with prioritized default blocks, and first-order encodings, such as context terms, Davidsonian events, modal classifiers, biconditional answer definitions, and canonicalized measurements. These choices affect clause shape, term depth, proof search branching, axiom selection, and other proof search strategies. We evaluate the pipeline on nlformtasks, a 1600-case English question-answering test set, across four LLM backends. The goal is to identify which representations are useful for different classes of English questions and how they affect automated reasoning performance.

ABSTRACT. We identify common challenges and requirements for verifying proofs of automated theorem provers in the Dedukti logical framework, and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to a large part of the calculus EP for higher-order logic, and integrate it into the automated theorem prover Leo-III, making it the first automated theorem prover for higher-order logic whose proofs can be independently checked and reused across systems. This uncovered and fixed several bugs in Leo-III.

ABSTRACT. Invertibility conditions are properties used by the cvc5 Satisfiability Modulo Theories (SMT) solver to reason about quantified bit-vector formulas. Previous work has proven 122 of 160 invertibility conditions for arbitrary bit-width. We prove the remaining 38 properties in the Rocq interactive theorem prover (ITP) with the help of Google Gemini and Claude Code. This paper presents our efforts in completing this set of proof goals and a case study for using AI assistants in proof projects.

ABSTRACT. Signal Temporal Logic (STL) is a widely used formalism for specifying temporal properties of real-valued signals generated by cyber-physical systems (CPS). In mission- and safety-critical domains, requirement specifications often comprise large collections of STL formulas, leading to significant challenges in requirement engineering. Ensuring the consistency of such requirements---i.e., verifying that they are not mutually contradictory---can be achieved through tableau-based satisfiability checking methods.

In this paper, we show that an existing tree-shaped tableau method for discrete-time STL with bounded temporal operators is unsound and provide a novel, corrected version of which we prove soundness and completeness. Additionally we introduce STLSat, an efficient Rust implementation of our tableau, that enables users to automatically verify the logical consistency of STL requirement sets, synthesize satisfying example signals, and analyse equivalence and implication relations among formulas. STLSat extends this requirements engineering framework with unsatisfiable core extraction, allowing users to identify minimal inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced First-Order Logic (FOL) and Satisfiability Modulo Theories (SMT) encodings for STL, which allow it to act as a portfolio solver. Experimental evaluations on an extended benchmark suite demonstrate that STLSat matches or outperforms state-of-the-art tools in speed and scalability, while maintaining correctness.