IWIL-2026: Papers with Abstracts

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 Σ^P_2. 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 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 in the Mizar60 evaluation, and speeds up 1567 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 in the Mizar60 evaluation.

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 φ we assign a goal [[φ]] of a second-order hereditary Harrop language such that φ is supported in a base B exactly when [[φ]] is operationally derivable from 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. 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 correctness of the translation from the puzzles to the networks, 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. This paper introduces a scheme to compare atoms and extract variable substitution bindings, as a part of unification, within the core loop of an automated theorem prover. The presented algorithm uses only linear algebraic transformations and no pointer operations and is designed to scale with parallelized hardware acceleration. Atoms are converted to a single 64-bit value using a fingerprint function, under which identity comparison is a single XOR and unifiability is dictated by membership in a linear span. Two mechanisms follow, blackout matching (reduced-basis membership) and power unification (recovering variable bindings by solving a linear system in GF(2^64)). Although the comparison is approximate, it serves as a prefilter whose candidate matches can be verified syntactically before inference. When correctly tuned, it achieves substantial candidate reduction during a simulated unification pass on randomly selected axioms with zero observed false negatives in targeted ground/pattern and pattern/pattern validation.

Abstract. In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational definitions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms. Both approaches have complementary applications and show very promising results.

Abstract. We report on automated reasoning infrastructure for the Elixir ecosystem and the BEAM virtual machine. Four packages supply the components a higher-order reasoning tool on this platform would otherwise write from scratch: data structures for higher-order terms and proof problems, parsing of the TPTP THF dialects, higher-order unification, a decidable term ordering, and uniform access to external provers. On top of them sits a fifth, Shot, a higher-order free-variable tableau prover organised around the actor model, and an interactive environment for teaching automated reasoning. The platform choice also carried the hypothesis that concurrency would repay the constant factor a managed runtime costs on the symbolic inner loop. We report that our current procedure for computing simultaneous closure bottlenecks concurrency. On the TPTP TH0 and TH1 problems a worker pool multiplies inference by a factor of 3.27 over a single worker, the rate of global closure attempts does not follow, and coverage is unchanged. The cause lies in the component that reconciles closure across branches. The libraries are early and under revision, and we present them as such.

Abstract. We describe our implementation of the linear model building calculus first presented in "First-Order Automatic Literal Model Generation" at IJCAR 2024: Given a finite consistent set of ground literals, a so-called trail, we want to extend it to a complete Herbrand-style interpretation represented by linear literals. Moreover, we give an algorithm to evaluate arbitrary clauses in the resulting linear model. We provide concrete data structures for efficiently implementing model building and clause evaluation. The resulting model building procedure runs in time linear in the size of the trail for a fixed signature. Even though checking whether a clause is false in a linear model is worst-case NP-complete, we provide a lazy backtracking algorithm that avoids materializing intermediate substitutions and is efficient in practice.
Our proposed algorithms are implemented as part of the SPASS(SCL) solver. Our experimental evaluation on all equality-free first-order TPTP problems shows that model building scales linearly in practice and, together with clause evaluation, accounts for less than one percent of the solver runtime on average on nontrivial runs. The generated models establish satisfiability for roughly a third of the satisfiable TPTP problems considered. If a generated interpretation is not a model of the input clauses, clause evaluation provides a concrete counterexample for extending the trail.

Abstract. We propose the TPTP World as a benchmark for evaluating LLMs' reasoning in which success is a TPTP derivation verified by independent verifiers. We describe the design of Proof Assistant for Agents (PAFA), an interface in which an AI agent states claims and premises, justified by a primitive rule or by automation of configurable strength. A finished proof is serialized directly as the TPTP derivation. We give the operation set for PAFA, a pipeline, and an evaluation protocol, and leave the underlying proof system, the automation boundary, and the proof state's retrieval mechanism open.

Abstract. An automata-theoretic implementation of a first-order theory of integers is discussed. It has addition, absolute values, minimum and maximum, and some bitwise operations, but lacks other multiplication than multiplication by a constant. The implementation is used in a tool that gives first- and second-year university students feedback on their answers to mathematics and computer science problems. The focus of this paper is on features of the tool supported by the implementation, and design and programming details that make it run sufficiently fast.