Twitch: Learning Abstractions for Equational Theorem Proving

Guy Axelrod, Moa Johansson, Nicholas Smallbone

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…