文章基本信息

标题：Normalized Completion Revisited
本地全文：下载
作者：Sarah Winkler ; Aart Middeldorp
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：21
页码：319-334
DOI：10.4230/LIPIcs.RTA.2013.319
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Normalized completion (Marché 1996) is a widely applicable and efficient technique for com- pletion modulo theories. If successful, a normalized completion procedure computes a rewrite system that allows to decide the validity problem using normalized rewriting. In this paper we consider a slightly simplified inference system for finite normalized completion runs. We prove correctness, show faithfulness of critical pair criteria in our setting, and propose a different notion of normalizing pairs. We then show how normalized completion procedures can benefit from AC- termination tools instead of relying on a fixed AC-compatible reduction order. We outline our implementation of this approach in the completion tool mkbtt and present experimental results, including new completions.
关键词：term rewriting; completion