Automated termination proofs with AProVE

Jürgen Giesl*, René Thiemann, Peter Schneider-Kamp, Stephan Falke

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

We describe the system ProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient algorithms based on classical simplification orders, dependency pairs, and the size-change principle. In particular, it contains many new improvements of the dependency pair approach that make automated termination proving more powerful and efficient. In ProVE, termination proofs can be performed with a user-friendly graphical interface and the system is currently among the most powerful termination provers available.

OriginalsprogEngelsk
BogserieLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind3091
Sider (fra-til)210-220
Antal sider11
ISSN0302-9743
StatusUdgivet - 1. dec. 2004

Fingeraftryk

Graphical user interfaces
Termination
Graphical User Interface
Simplification
Efficient Algorithms
Verify
Term

Citer dette

@article{5e15b25beb0b4bb1abb06cc9991889ad,
title = "Automated termination proofs with AProVE",
abstract = "We describe the system ProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient algorithms based on classical simplification orders, dependency pairs, and the size-change principle. In particular, it contains many new improvements of the dependency pair approach that make automated termination proving more powerful and efficient. In ProVE, termination proofs can be performed with a user-friendly graphical interface and the system is currently among the most powerful termination provers available.",
author = "J{\"u}rgen Giesl and Ren{\'e} Thiemann and Peter Schneider-Kamp and Stephan Falke",
year = "2004",
month = "12",
day = "1",
language = "English",
volume = "3091",
pages = "210--220",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Heinemann",

}

Automated termination proofs with AProVE. / Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan.

I: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 3091, 01.12.2004, s. 210-220.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Automated termination proofs with AProVE

AU - Giesl, Jürgen

AU - Thiemann, René

AU - Schneider-Kamp, Peter

AU - Falke, Stephan

PY - 2004/12/1

Y1 - 2004/12/1

N2 - We describe the system ProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient algorithms based on classical simplification orders, dependency pairs, and the size-change principle. In particular, it contains many new improvements of the dependency pair approach that make automated termination proving more powerful and efficient. In ProVE, termination proofs can be performed with a user-friendly graphical interface and the system is currently among the most powerful termination provers available.

AB - We describe the system ProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient algorithms based on classical simplification orders, dependency pairs, and the size-change principle. In particular, it contains many new improvements of the dependency pair approach that make automated termination proving more powerful and efficient. In ProVE, termination proofs can be performed with a user-friendly graphical interface and the system is currently among the most powerful termination provers available.

UR - http://www.scopus.com/inward/record.url?scp=35048887144&partnerID=8YFLogxK

M3 - Journal article

AN - SCOPUS:35048887144

VL - 3091

SP - 210

EP - 220

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -