Idioma:

Abstract Completion, Formalized

Nao Hirokawa ; Aart Middeldorp ; Christian Sternagel ; Sarah Winkler

Logical methods in computer science, 2019-01, Vol.15, Issue 3 [Periódico revisado por pares]

Texto completo disponível

Citações Citado por

Título:
Abstract Completion, Formalized
Autor: Nao Hirokawa ; Aart Middeldorp ; Christian Sternagel ; Sarah Winkler
Assuntos: computer science - logic in computer science
É parte de: Logical methods in computer science, 2019-01, Vol.15, Issue 3
Descrição: Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of M\'etivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
Editor: Logical Methods in Computer Science e.V
Idioma: Inglês

Voltar para lista de resultados

Resultado 1