DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)
arXiv:1810.05666 · doi:10.4204/EPTCS.280.12
Abstract
We present a tool that automates termination proofs for recursive definitions by mining existing termination theorems.
In Proceedings ACL2 2018, arXiv:1810.03762