ABSTRACT. Equational Theories Project is a collaborative effort, which explores the validity of certain first-order logic implications of certain kind. The project has been completed but triggered further research. This report investigates how much can be automatically proven and disproven by the automated theorem prover Vampire. An interesting conclusion is that Vampire can prove all the considered implications that hold and also is able to refute a vast majority of those that do not hold. A downside is that proofs coming out of Vampire do not give a direct proof artifact for models.

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 defintions 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 that shows very promissing results.

ABSTRACT. Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after a failed attempt. SATCoP addresses this by retaining grounded tableau clauses in an incremental SAT solver, allowing the prover to refute the problem once the accumulated ground clauses become propositionally unsatisfiable. We introduce SATResetCoP, which relies more directly on this persistent SAT state by not backtracking on unproductive tableaux and instead starting new ones to generate further ground clauses for the SAT solver. On TPTP, SATResetCoP improves over our leanCoP-style baseline by 54% and our SATCoP-style baseline by 18%. On the bushy MPTP2078 benchmark, it solves 616 problems, a 49% improvement over our leanCoP-style baseline and a 12% improvement over our SATCoP-style baseline. These results suggest that changing tableau guidance to accumulate useful ground clauses faster improves the performance of the prover.

ABSTRACT. Machine-learned clause-selection heuristics for saturation-based theorem provers seem to follow a simple rule: prefer clauses similar to those that appeared in successful proofs before. Unfortunately, proof search is rarely that cooperative. A closer inspection of Vampire's successful runs reveals a number of surprises. Clauses may contribute to a proof without ever being selected themselves, thanks to simplifications. Under the AVATAR architecture, the situation may become stranger still, with moments in time with literally no future proof clause in sight (i.e., on the passive set). This talk showcases a collection of such phenomena and discusses their implications for learning-guided theorem proving. As we shall see, things can get surprisingly wild in just a few seconds of proof search.

ABSTRACT. We present ProofAtlas, an open-source saturation-based theorem prover for first-order logic with equality, built as an extensible platform for experimenting with neural clause selection. ProofAtlas implements the given-clause algorithm with superposition, and replaces the usual hand-tuned clause-selection heuristic with a neural encoder--scorer that embeds each clause and ranks the unprocessed set against the current proof state. The system is organised as a single Rust proving core exposed through three runtimes: native Python bindings for the command-line prover, the training pipeline, and large-scale evaluation; a WebAssembly build that runs the prover entirely in the browser; and a socket-based deployment that lets many prover workers share a small pool of GPU inference servers. A companion web interface offers both server-side and in-browser proving together with an interactive derivation inspector. We describe the architecture, the integration of neural inference into the saturation loop, and the supporting tooling, and we calibrate ProofAtlas's proving engine against the established provers Vampire and SPASS.

ABSTRACT. This work introduces a concurrent framework for lemma exploration over problems expressed in TPTP syntax. Given such a problem, the framework concurrently generates and performs proof search for multiple equivalent problem variants, where each variant is constructed by augmenting the original with sets of candidate lemmas. The aim of this approach is the effective discovery of proof-aiding lemmas. In this work, lemmas are generated by a large language model (LLM) and injected into their corresponding problem variant only if they are semantically certified using Vampire, i.e. provably entailed by the original problem axioms; Vampire is then used to perform proof search over these lemma-augmented problem variants. Concurrency is present within multiple levels of the framework: during the generation of candidate lemmas, the semantic certification of candidate lemmas, and proof search for lemma-augmented problem variants. This design is scalable and intended to provide a foundation for future work that will extend lemma exploration towards lemma mining, i.e. from the simple discovery of proof-aiding lemmas to their large-scale collection. Utilising GPT-5-mini as the underlying LLM, we evaluate our framework on $655$ group theory problems from the TPTP library. We find that candidate lemmas are: (a) very often syntactically correct, (b) often entailed by their original problem axioms, and (c) can reduce proof-search times. Additionally, we note several instances where a lemma-augmented problem variant obtains a proof, whilst the original problem does not -- including an instance for which Vampire had not previously recorded a proof\footnote{This work is currently under submission elsewhere, hence only the presenting author is included here. Before the Vampire workshop, we will likely expand upon the detailed experiments, such that a broader range of TPTP problems are accounted for, and a broader range of language models are evaluated.

ABSTRACT. Recent work on Vampire enabled checking of proofs in Lean end-to-end, greatly increasing trust in the found proof. This work presents an approach under development, which takes a generic TPTP proof in the CNF and FOF fragment, uses Vampire to reconstruct the inferences, and chain resulting Lean proofs to a single end-to-end Lean proof, transferring the increased trust to foreign ATP systems capable of producing suitable TSTP proofs.

ABSTRACT. The Thousands of Problems for Theorem Provers (TPTP) Problem Library constitutes the standard benchmark for automated theorem provers. We provide a tool that allows the import of TPTP Problem Library instances in first-order form (FOF), clause normal form (CNF) and monomorphic and polymorphic typed first-order form (TFF) as expressions in the interactive theorem prover Lean. This makes the TPTP Problem Library available as a benchmark for automation tools in Lean that aim to facilitate writing proofs in Lean. We compare the results of the tactics Duper, Lean-SMT and Grind with the results of Vampire.

ABSTRACT. First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence. We propose such methods based on both theoretical insights and existing tools, implement them, and report on experiments testing their effectiveness on a large educational data set with > 100.000 pairs of first-order formulas.

ABSTRACT. We present SigmaKEE-rs, a re-implementation of the Sigma Knowledge Engineering Environment (SigmaKEE) in the Rust programming language, designed to serve as an ontological datastore backed by embedded theorem proving. A key contribution of this work is the integration of the Vampire theorem prover as an embedded library rather than as an external process, via extended Rust–C++ Foreign Function Interface (FFI) bindings built on the vampire-rs Rust library. We extend these bindings with support for Vampire’s type system and clausification machinery. Using this strategy, the entire baseline ontology, the Suggested Upper Merged Ontology (SUMO), is eagerly normalized, deduplicated, and held in an in-memory datastore alongside an incrementally maintained SUMO Inference Engine (SInE) relevance index. Subsequent queries bypass Vampire’s parsing and the bulk of its preprocessing, invoking only clausification and the saturation engine on a relevance-filtered axiom set. We describe the engineering challenges encountered in adapting Vampire into a reusable component suitable for real-time, multi-query workloads, and report preliminary performance results comparing the embedded approach with the traditional process-based invocation model used in the original Java-based SigmaKEE.

ABSTRACT. Recent advances in automated reasoning have led to the development of powerful tools for solving complex problems in domains such as verification, theorem proving, and planning. A key component of many of these tools is tailored SAT solvers. Historically, SAT solvers have relied on a very aggressive backtracking strategy, called non-chronological backtracking. To preserve clean invariants, the addition of new clauses to the solver forces it to backtrack, even when the new clause is already satisfied. This can lead to significant performance degradation. Chronological backtracking is a more conservative approach. With weaker invariants, it is more resilient to the addition of new clauses. This scheme can be further improved to support the addition of arbitrary clauses non-falsified, without requiring any backtracking. While CB addresses inefficiencies at the SAT level, it is still ignorant of the cost of flipping literals. Graph Backtracking is a new technique for SAT solvers that allows the user to provide a cost heuristic to guide the backtracking process. The SAT engine is then dissuaded from undoing expensive literals. In this presentation, we explore how chronological and graph backtracking can be integrated into Vampire, and more specifically into AVATAR. AVATAR combines the strengths of SAT solvers with first-order saturation by splitting the search space into smaller, more manageable parts using a SAT solver. Graph backtracking can be used to guide the splitting process and preserve expensive literals as long as possible. We will discuss the challenges and benefits of integrating these techniques into AVATAR, and present preliminary results on their impact on the performance of the solver. This work is still in progress. As such, we will welcome suggestions and feedback from the community on how to best integrate these techniques.

ABSTRACT. Modern first-order theorem provers are usually presented as logical engines: they transform conjectures into clauses, saturate a search space under inference rules and terminate, when successful, with a proof or countermodel. This talk proposes a complementary view: a prover such as Vampire is also a highly structured combinatorial optimization system. Its central computational difficulty is not merely the validity of a formula, but the disciplined allocation of scarce search resources across an enormous space of possible clauses, inferences, simplifications, splittings, theory calls and strategy schedules. The starting point is the observation that saturation-based theorem proving already contains many objects familiar to combinatorial optimization and operations research. Clause selection resembles online scheduling under uncertainty; literal selection and term ordering resemble priority design in discrete search; redundancy elimination functions as dominance pruning; AVATAR-style splitting introduces a branch-and-cut like interaction between first-order reasoning and propositional control; portfolio modes instantiate algorithm-selection and resource-allocation problems. In this perspective, a successful Vampire run is not only a derivation in logic, but also an efficiently managed search process whose performance depends on implicit operational decisions. The proposed contribution is a research agenda for making these operational decisions explicit. I argue for treating prover strategy design as a mathematically analyzable optimization problem over proof-search policies. Rather than asking only which heuristic performs well on a benchmark class, we can ask which structural features of a problem justify a particular inference budget, splitting policy, simplification frequency or theory reasoning schedule. This reframes heuristic engineering as policy synthesis: a prover becomes a system that continuously solves a meta-level optimization problem while it searches for an object level proof. This viewpoint also suggests new application areas from algorithms and operations research. Many results in combinatorial optimization depend on certificates: infeasibility proofs, dominance arguments, valid inequalities, decomposition cuts, approximation bounds and correctness proofs for reductions. Vampire-like provers could serve as certificate auditors for optimization pipelines, checking whether a preprocessing rule preserves optimality, whether a decomposition cut is logically valid, or whether an algorithmic reduction from one discrete problem to another is sound under stated assumptions. Conversely, OR can contribute sharper evaluation methodology for theorem proving: performance profiles, ablation-aware benchmarking, budgeted portfolio design, robust strategy selection and instance-space analysis. The talk will focus on the implementation consequences of this synthesis. What prover internals must be exposed to support OR-guided strategy control? Which proof-search traces should be logged to make unsuccessful case studies scientifically useful? How should benchmarks be designed when the relevant object is not merely theorem/non-theorem status, but the cost structure of reaching a proof? Finally, I identify missing features in current provers: richer proof-search telemetry, optimization-aware strategy languages, interfaces for external policy learners and certificate formats that connect first-order derivations with optimization models. The broader claim is that substantial progress in theorem proving may require not only stronger calculi, but a more explicit theory of proof search as an optimization problem. Vampire is an especially natural testbed for this agenda because its architecture already sits at the intersection of saturation, SAT/SMT interaction, portfolio reasoning, finite model construction and practical proof engineering.

ABSTRACT. Forward subsumption and subsumption resolution are among the most performance-critical redundancy elimination techniques in saturation-based theorem proving. Vampire implements both using Clause Code Trees, where clauses from the search space are compiled into sequences of matching instructions (CodeOps) arranged in a trie. The trie structure allows common prefixes across different clauses to be merged, reducing the total number of CodeOps. In a standard Clause Code Tree, literals of the same clause form a path inside the trie. That means common prefixes between literals within the same clause cannot be merged. A Wide Clause Code Tree addresses this by flattening all literals into a single shared trie, enabling intra-clausal sharing. While this seems like an obvious optimization, it turns out to be surprisingly hard to implement efficiently. The core problem is that the standard Clause Code Tree structure allows for very efficient pruning techniques based on literal depth and matching compatibility. This structure is lost in Wide Trees. Pruning turns out to be essential, as the savings from exploiting inter-literal overlap are far smaller than those gained from pruning. Attempts to recover pruning via index interval propagation reduced executed CodeOps significantly, even below the original Clause Code Tree implementation, but the per-branch overhead of interval checking outweighed the savings. CodeOp execution is simply too cheap for any non-trivial bookkeeping to be affordable. Wide clause code trees remain an open problem and this talk discusses the above approaches and current directions.

ABSTRACT. In this paper, unification is considered as a simple theorem prover in which variables to be solved are directly represented by free logic variables. This approach is different from other works which consider unification as the application of a set of rewrite rules. The benefit of the approach this paper considers is naturalness, clearness and uniform framework. The theorem prover is not in full setting. Since programming formulas are fixed and simple a few rules, goal formulas are matched with the left hand-side of rewrite rules. The theorem prover acts like a term rewriting system. But when free logic variables are at the top, they are subject to search. This paper considers the solution of this technical problem.