IWIL-2026: Keyword Index

Keyword	Papers
a
automated theorem proving	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop Some Experiments with Twee-Style Goal-Directedness Building Blocks for Reasoning on the BEAM Benchmarking LLMs Against TPTP: A Vision for the Near Future
b
base-extension semantics	Towards an Operational Proof-theoretic Semantics
BCH codes	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
Benchmarking	Benchmarking LLMs Against TPTP: A Vision for the Near Future
bitwise operations	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
c
concurrency	Building Blocks for Reasoning on the BEAM
conjecturing	Neural Conjecturing for Saturation Theorem Provers
e
E prover	Neural Conjecturing for Saturation Theorem Provers
education tool	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
ELIXIR	Building Blocks for Reasoning on the BEAM
epsilon calculus	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
error correction	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
f
finite automata	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
first-order logic	Efficient Linear Model Building and Clause Evaluation
g
goal-directed search	Some Experiments with Twee-Style Goal-Directedness
h
Herbrand disjunctions	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
hereditary Harrop formulae	Towards an Operational Proof-theoretic Semantics
higher-order logic	Building Blocks for Reasoning on the BEAM
i
incomplete proofs	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
incorrect proofs	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Inferentialism	Towards an Operational Proof-theoretic Semantics
integer Presburger arithmetic	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
intuitionistic logic	Towards an Operational Proof-theoretic Semantics
l
large language models	Benchmarking LLMs Against TPTP: A Vision for the Near Future
lemma introduction	Neural Conjecturing for Saturation Theorem Provers
logic programming	Towards an Operational Proof-theoretic Semantics
m
machine learning	Neural Conjecturing for Saturation Theorem Provers
Mizar	Neural Conjecturing for Saturation Theorem Provers
model building	Efficient Linear Model Building and Clause Evaluation
p
Parallelization	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
proof theory	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
proof verification	Benchmarking LLMs Against TPTP: A Vision for the Near Future
proof-theoretic semantics	Towards an Operational Proof-theoretic Semantics
s
saturation	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
SCL(FOL)	Efficient Linear Model Building and Clause Evaluation
search heuristics	Some Experiments with Twee-Style Goal-Directedness
secure computing	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
shared terms	Some Experiments with Twee-Style Goal-Directedness
SPASS(SCL)	Efficient Linear Model Building and Clause Evaluation
t
tableaux	Towards an Operational Proof-theoretic Semantics Building Blocks for Reasoning on the BEAM
TPTP	Benchmarking LLMs Against TPTP: A Vision for the Near Future
u
unification	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
Uniform Proofs	Towards an Operational Proof-theoretic Semantics
v
Vampire	Neural Conjecturing for Saturation Theorem Provers
w
weakest preconditions	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs