Twee: An Equational Theorem Prover
AUTOMATED DEDUCTION, CADE 28（2021）
摘要
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.
更多查看译文
关键词
Automated theorem proving, unit equality, completion
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要