Argument filterings and usable rules for simply typed dependency pairs

Takahito Aoto, Toshiyuki Yamada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

Simply typed term rewriting (Yamada, 2001) is a framework of higher-order term rewriting without bound variables based on Lisp-like syntax. The dependency pair method for the framework has been obtained by extending the first-order dependency pair method and subterm criterion in (Aoto & Yamada, 2005). In this paper, we incorporate termination criteria using reduction pairs and related refinements into the simply typed dependency pair framework using recursive path orderings for S-expression rewriting systems (Toyama, 2008). In particular, we incorporate the usable rules criterion with respect to argument filterings, which is a key ingredient to prove the termination in a modular way. The proposed technique has been implemented in a termination prover and an experimental result is reported.

Original languageEnglish
Title of host publicationFrontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings
Pages117-132
Number of pages16
DOIs
Publication statusPublished - 2009 Dec 1
Event7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 - Trento, Italy
Duration: 2009 Sep 162009 Sep 18

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5749 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th International Symposium on Frontiers of Combining Systems, FroCoS 2009
CountryItaly
CityTrento
Period09/9/1609/9/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Argument filterings and usable rules for simply typed dependency pairs'. Together they form a unique fingerprint.

Cite this