Twee: An Equational Theorem Prover
Nicholas Smallbone · Lecture notes in computer science · 2021
Abstract Twee is an automated theorem prover for equational logic. It implements unfailing Knuth-Bendix completion with ground joinability testing and a connectedness-based redundancy criterion. It came second in the UEQ division of CASC-J10, solving some problems that no other system solved. This paper describes Twee’s design and implementation.