Certification extends Termination Techniques

There are termination proofs that are produced by termination tools for which certifiers are not powerful enough. However, a similar situation also occurs in the other direction. We have formalized termination techniques in a more general setting as they have been introduced. Hence, we can certify p...

Full description

Bibliographic Details
Main Authors: Sternagel, Christian, Thiemann, René
Format: Text
Language:unknown
Published: 2012
Subjects:
Computer Science - Logic in Computer Science
Arctic
Online Access:http://arxiv.org/abs/1208.1594
id ftarxivpreprints:oai:arXiv.org:1208.1594
record_format openpolar
spelling ftarxivpreprints:oai:arXiv.org:1208.1594 2023-09-05T13:17:09+02:00 Certification extends Termination Techniques Sternagel, Christian Thiemann, René 2012-08-08 http://arxiv.org/abs/1208.1594 unknown http://arxiv.org/abs/1208.1594 Computer Science - Logic in Computer Science text 2012 ftarxivpreprints 2023-08-16T12:47:55Z There are termination proofs that are produced by termination tools for which certifiers are not powerful enough. However, a similar situation also occurs in the other direction. We have formalized termination techniques in a more general setting as they have been introduced. Hence, we can certify proofs using techniques that no termination tool supports so far. In this paper we shortly present two of these formalizations: Polynomial orders with negative constants and Arctic termination. Comment: 5 pages, International Workshop on Termination 2010 Text Arctic ArXiv.org (Cornell University Library) Arctic
institution Open Polar
collection ArXiv.org (Cornell University Library)
op_collection_id ftarxivpreprints
language unknown
topic Computer Science - Logic in Computer Science
spellingShingle Computer Science - Logic in Computer Science
Sternagel, Christian
Thiemann, René
Certification extends Termination Techniques
topic_facet Computer Science - Logic in Computer Science
description There are termination proofs that are produced by termination tools for which certifiers are not powerful enough. However, a similar situation also occurs in the other direction. We have formalized termination techniques in a more general setting as they have been introduced. Hence, we can certify proofs using techniques that no termination tool supports so far. In this paper we shortly present two of these formalizations: Polynomial orders with negative constants and Arctic termination. Comment: 5 pages, International Workshop on Termination 2010
format Text
author Sternagel, Christian
Thiemann, René
author_facet Sternagel, Christian
Thiemann, René
author_sort Sternagel, Christian
title Certification extends Termination Techniques
title_short Certification extends Termination Techniques
title_full Certification extends Termination Techniques
title_fullStr Certification extends Termination Techniques
title_full_unstemmed Certification extends Termination Techniques
title_sort certification extends termination techniques
publishDate 2012
url http://arxiv.org/abs/1208.1594
geographic Arctic
geographic_facet Arctic
genre Arctic
genre_facet Arctic
op_relation http://arxiv.org/abs/1208.1594
_version_ 1776198442172809216

Similar Items