DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)

Matt Kaufmann
(UT Austin)

We present a tool that automates termination proofs for recursive definitions by mining existing termination theorems.

In Shilpi Goel and Matt Kaufmann: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2018), Austin, Texas, USA, November 5-6, 2018, Electronic Proceedings in Theoretical Computer Science 280, pp. 161–163.
Published: 29th October 2018.
ArXived at: http://dx.doi.org/10.4204/EPTCS.280.12 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org