The Generalized Subterm Criterion in TTT2
Christian Sternagel
TL;DR
This paper introduces an SMT encoding of a generalized subterm criterion and evaluates its implementation within the TTT2 termination tool, enhancing automated termination proofs.
Contribution
It presents a novel SMT encoding of a generalized subterm criterion and integrates it into TTT2, improving termination analysis capabilities.
Findings
Effective SMT encoding of the generalized subterm criterion
Successful implementation in TTT2
Enhanced termination proof automation
Abstract
We present an SMT encoding of a generalized version of the subterm criterion and evaluate its implementation in TTT2.
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
TopicsNatural Language Processing Techniques · Intelligent Tutoring Systems and Adaptive Learning · Multi-Agent Systems and Negotiation