ABSTRACT. This is the opening of IWIL.

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. 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.

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 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.