Termination of Integer Term Rewriting

C. Fuhs; J. Giesl; M. Plücker; P. Schneider-Kamp; S. Falke

Termination of Integer Term Rewriting

C. Fuhs
, J. Giesl
, M. Plücker
, P. Schneider-Kamp
, S. Falke

Department of Mathematics and Computer Science

RWTH Aachen University
University of New Mexico

Research output: Contribution to journal › Conference article › Research › peer-review

Abstract

When using rewrite techniques for termination analysis of programs, a main problem are predefined data types like integers. We extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically.

Original language	English
Journal	Dagstuhl Seminar Proceedings
Volume	9411
ISSN	1862-4405
Publication status	Published - 2010
Event	Interaction Versus Automation: The Two Faces of Deduction 2009 - Wadern, Germany Duration: 4. Oct 2009 → 9. Oct 2009

Conference

Conference	Interaction Versus Automation: The Two Faces of Deduction 2009
Country/Territory	Germany
City	Wadern
Period	04/10/2009 → 09/10/2009

Bibliographical note

Publisher Copyright:
© 2010 Dagstuhl Seminar Proceedings. All Rights Reserved.

SDU Link

Check access to the material in SDU Library's search engine

Cite this

@inproceedings{dfc97e74a9584316844ec87781bfdc4f,

title = "Termination of Integer Term Rewriting",

abstract = "When using rewrite techniques for termination analysis of programs, a main problem are predefined data types like integers. We extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically.",

author = "C. Fuhs and J. Giesl and M. Pl{\"u}cker and P. Schneider-Kamp and S. Falke",

note = "Publisher Copyright: {\textcopyright} 2010 Dagstuhl Seminar Proceedings. All Rights Reserved.; Interaction Versus Automation: The Two Faces of Deduction 2009 ; Conference date: 04-10-2009 Through 09-10-2009",

year = "2010",

language = "English",

volume = "9411",

journal = "Dagstuhl Seminar Proceedings",

issn = "1862-4405",

}

TY - GEN

T1 - Termination of Integer Term Rewriting

AU - Fuhs, C.

AU - Giesl, J.

AU - Plücker, M.

AU - Schneider-Kamp, P.

AU - Falke, S.

PY - 2010

Y1 - 2010

N2 - When using rewrite techniques for termination analysis of programs, a main problem are predefined data types like integers. We extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically.

AB - When using rewrite techniques for termination analysis of programs, a main problem are predefined data types like integers. We extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically.

UR - https://www.scopus.com/pages/publications/85174552334

M3 - Conference article

AN - SCOPUS:85174552334

SN - 1862-4405

VL - 9411

JO - Dagstuhl Seminar Proceedings

JF - Dagstuhl Seminar Proceedings

T2 - Interaction Versus Automation: The Two Faces of Deduction 2009

Y2 - 4 October 2009 through 9 October 2009

ER -

Termination of Integer Term Rewriting

Abstract

Conference

Bibliographical note

SDU Link

Other files and links

Fingerprint

Cite this