Max Scheler
Gesellschaft

Repository | Series | Buch | Kapitel

225408

Completion is an instance of abstract canonical system inference

Guillaume BurelClaude Kirchner

pp. 497-520

Abstrakt

Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures.Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process.By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.

Publication details

Published in:

Futatsugi Kokichi, Jouannaud Jean-Pierre, Meseguer José (2006) Algebra, meaning, and computation: essays dedicated to Joseph A. Goguen on the occasion of his 65th birthday. Dordrecht, Springer.

Seiten: 497-520

DOI: 10.1007/11780274_26

Referenz:

Burel Guillaume, Kirchner Claude (2006) „Completion is an instance of abstract canonical system inference“, In: K. Futatsugi, J. Jouannaud & J. Meseguer (eds.), Algebra, meaning, and computation, Dordrecht, Springer, 497–520.