cl-banner

Decreasing Diagrams and Relative Termination

Nao Hirokawa and Aart Middeldorp

Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 487 – 501, 2010.

Abstract

In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and the critical pair steps are relatively terminating with respect to R. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are present-ed.

 

  PDF |    doi:10.1007/978-3-642-14203-1_41  |  © Springer

BibTeX 

@inproceedings{NHAM-IJCAR10,
author = "Nao Hirokawa and Aart Middeldorp",
title = "Decreasing Diagrams and Relative Termination",
booktitle = "Proceedings of the 5th International Joint Conference on Automated Reasoning",
series = "Lecture Notes in Artificial Intelligence",
volume = 6173,
pages = "487--501",
publisher = "Springer-Verlag",
year = 2010
}
Nach oben scrollen