Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.06849 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908871412416512 |
|---|---|
| author | Axelrod, Guy Johansson, Moa Smallbone, Nicholas |
| author_facet | Axelrod, Guy Johansson, Moa Smallbone, Nicholas |
| contents | Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_06849 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Twitch: Learning Abstractions for Equational Theorem Proving Axelrod, Guy Johansson, Moa Smallbone, Nicholas Logic in Computer Science Artificial Intelligence I.2.3 Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems. |
| title | Twitch: Learning Abstractions for Equational Theorem Proving |
| topic | Logic in Computer Science Artificial Intelligence I.2.3 |
| url | https://arxiv.org/abs/2603.06849 |