English

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

Logic in Computer Science 2018-10-16 v1
Authors: Matt Kaufmann
View on arXiv ↗ PDF ↗ DOI ↗

Abstract

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

Keywords

termination proof recursive definition automation tool theorem mining

Cite

@article{arxiv.1810.05666,
  title  = {DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)},
  author = {Matt Kaufmann},
  journal= {arXiv preprint arXiv:1810.05666},
  year   = {2018}
}

Comments

In Proceedings ACL2 2018, arXiv:1810.03762

Related papers

View all related →
Logic in Computer Science · Computer Science
Automated verification of termination certificates
Frédéric Blanqui, Kim Quyen Ly
2012-12-12
Logic in Computer Science · Computer Science
TTT2 with Termination Templates for Teaching
Jonas Schöpf, Christian Sternagel
2018-06-14
Logic in Computer Science · Computer Science
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
2019-08-27
Programming Languages · Computer Science
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, Eric W. Smith
2017-05-04
Logic in Computer Science · Computer Science
Automated Termination Proofs for C Programs with Lists (Short WST Version)
Jera Hensel, Jürgen Giesl
2023-07-21
Logic in Computer Science · Computer Science
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
Frédéric Blanqui, Adam Koprowski
2012-03-01
Logic in Computer Science · Computer Science
A Conjecture Equivalent to the Collatz Conjecture
Ashish Tiwari
2021-08-17
Programming Languages · Computer Science
Preliminary Notes on Termination and Non-Termination Reasoning
Ton Chanh Le
2013-09-13
Machine Learning · Computer Science
Neural Termination Analysis
Mirco Giacobbe, Daniel Kroening, Julian Parsert
2022-09-07
Programming Languages · Computer Science
Polytool: polynomial interpretations as a basis for termination analysis of Logic programs
Manh Thang Nguyen, Danny De Schreye, Jürgen Giesl, Peter Schneider-Kamp
2009-12-23
Logic in Computer Science · Computer Science
Automated Termination Proofs for Logic Programs by Term Rewriting
P. Schneider-Kamp, J. Giesl, A. Serebrenik, R. Thiemann
2008-09-01
Programming Languages · Computer Science
Automatic Termination Analysis of Programs Containing Arithmetic Predicates
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
2007-05-23
Logic in Computer Science · Computer Science
Proving Termination of C Programs with Lists
Jera Hensel, Jürgen Giesl
2023-06-06
Programming Languages · Computer Science
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori +2
2021-09-02
Logic in Computer Science · Computer Science
Automated Termination Analysis for Logic Programs with Cut
Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik +1
2010-07-29
Programming Languages · Computer Science
Termination Analysis Without the Tears
Shaowei Zhu, Zachary Kincaid
2021-09-16
Logic in Computer Science · Computer Science
CeTA - A Tool for Certified Termination Analysis
Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl
2012-08-09
Logic in Computer Science · Computer Science
Termination Analysis by Learning Terminating Programs
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2022-10-18
Logic in Computer Science · Computer Science
Proving Termination of Probabilistic Programs Using Patterns
Javier Esparza, Andreas Gaiser, Stefan Kiefer
2012-04-16
Programming Languages · Computer Science
Termination Analysis of Linear-Constraint Programs
Amir M. Ben-Amram, Samir Genaim, Joël Ouaknine, James Worrell
2026-01-27
Logic in Computer Science · Computer Science
Nagoya Termination Tool
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
2014-04-29
Logic in Computer Science · Computer Science
AProVE: Modular Termination Analysis of Memory-Manipulating C Programs
Frank Emrich, Jera Hensel, Jürgen Giesl
2025-06-13
Human-Computer Interaction · Computer Science
A Theorem Prover for Scientific and Educational Purposes
Mario Frank, Christoph Kreitz
2018-03-06
Programming Languages · Computer Science
cTI: A constraint-based termination inference tool for ISO-Prolog
Fred Mesnard, Roberto Bagnara
2007-05-23
Programming Languages · Computer Science
The Probabilistic Termination Tool Amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
2021-07-29