DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)
Matt Kaufmann (UT Austin)
TL;DR
DefunT is a tool that automates the process of proving termination of recursive functions by leveraging existing termination theorems from community resources.
Contribution
It introduces an automated approach to termination proofs by mining community-shared termination theorems, streamlining the proof process.
Findings
Successfully automates termination proofs for recursive definitions.
Leverages community resources to enhance proof automation.
Reduces manual effort in termination proof development.
Abstract
We present a tool that automates termination proofs for recursive definitions by mining existing termination theorems.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies