caa a22 4500 463182677 CHVBK 20180406164843.0 cr unu---uuuuu 170326e20070501xx s 000 0 eng 10.1007/s10817-006-9065-7 doi (NATIONALLICENCE)springer-10.1007/s10817-006-9065-7 Structures for Abstract Rewriting [Elektronische Daten] [Marc Aiguier, Diane Bahrami] When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding theory, and we propose a Knuth-Bendix-style completion procedure in this abstract framework. Springer Science+Business Media, Inc., 2007 rewrite system nationallicence abstract rewriting nationallicence axiomatization nationallicence abstract deduction procedure nationallicence abstract completion procedure nationallicence Aiguier Marc Université d'Évry, IBISC CNRS FRE 2873, 523 pl. des Terrasses, 91000, Évry, France aut Bahrami Diane CEA/LIST Saclay, 91191, Gif sur Yvette Cedex, France aut Journal of Automated Reasoning Kluwer Academic Publishers 38/4(2007-05-01), 303-351 0168-7433 38:4<303 2007 38 10817 https://doi.org/10.1007/s10817-006-9065-7 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9065-7 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Aiguier Marc Université d'Évry, IBISC CNRS FRE 2873, 523 pl. des Terrasses, 91000, Évry, France aut NATIONALLICENCE 700 1- Bahrami Diane CEA/LIST Saclay, 91191, Gif sur Yvette Cedex, France aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/4(2007-05-01), 303-351 0168-7433 38:4<303 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer