cl-banner

Multi-Completion with Termination Tools (System Description)

Haruhiko Sato, Sarah Winkler, Masahito Kurihara, and Aart Middeldorp

Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 306 – 312, 2008.

Abstract

In this paper we describe a new tool for performing Knuth-Bendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006) and implemented in the Slothrop system. Our tool can be used with any termination tool that satisfies certain minimal requirements. Preliminary experimental results show the potential of our tool.

 

  PDF |    doi:10.1007/978-3-540-71070-7_26  |  © Springer

BibTeX 

@inproceedings{HSSWMKAM-IJCAR08,
author = "Haruhiko Sato and Sarah Winkler and Masahito Kurihara and Aart Middeldorp",
title = "Multi-Completion with Termination Tools (System Description)",
booktitle = "Proceedings of the 4th International Joint Conference on Automated Reasoning",
series = "Lecture Notes in Artificial Intelligence",
volume = "5195",
pages = "306--312",
publisher = "Springer-Verlag",
year = 2008
}
Nach oben scrollen