NAISS
SUPR
NAISS Projects
SUPR
Twee abstraction experiment outputs
Dnr:

NAISS 2025/23-661

Type:

NAISS Small Storage

Principal Investigator:

Guy Axelrod

Affiliation:

Chalmers tekniska högskola

Start Date:

2025-11-14

End Date:

2026-07-01

Primary Classification:

10201: Computer Sciences

Allocation

Abstract

We have been running experiments to evaluate various strategies for automating the discovery of abstractions with the goal of assisting twee (an automated equational theorem prover, see linked webpage) in discovering shorter or unknown proofs of abstract algebraic theorems. The previous project storage is ending, and we need a new storage allocation to keep the existing and future experiment logs. Preliminary results were reported at the 10th Conference on Artificial Intelligence and Theorem Proving (AITP 2025, slides available at https://aitp-conference.org/2025/). All compute for these experiments was done on the e-infrastructure compute allocation for CSE vera project.