Arctic termination ... below zero

A. Koprowski, J. Waldmann

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    19 Citaten (Scopus)
    2 Downloads (Pure)


    We introduce the arctic matrix method for automatically proving termination of term rewriting. We use vectors and matrices over the arctic semi-ring: natural numbers extended with -8,with the operations "max" and "plus". This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the Dependency Pairs transformation, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers "below zero": integers extended with -8.This allows to treat some termination problems with symbols that require a predecessor semantics. The contents of the paper has been formally verified in the Coq proof assistant and the formalization has been contributed to the CoLoR library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method. We also report on experiments with an implementation of this method which, compared to results from 2007, outperforms TPA (winner of the certified termination competition for term rewriting), and in the string rewriting category is as powerful as Matchbox was but now all of the proofs are certified.
    Originele taal-2Engels
    TitelRewriting Techniques and Applications (19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings)
    RedacteurenA. Voronkov
    Plaats van productieBerlin
    ISBN van geprinte versie978-3-540-70588-8
    StatusGepubliceerd - 2008

    Publicatie series

    NaamLecture Notes in Computer Science
    ISSN van geprinte versie0302-9743


    Duik in de onderzoeksthema's van 'Arctic termination ... below zero'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit