# zbMATH — the first resource for mathematics

Structures for abstract rewriting. (English) Zbl 1125.03011
Summary: 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 the 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.

##### MSC:
 03B35 Mechanization of proofs and logical operations 68Q42 Grammars and rewriting systems 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text:
##### References:
 [1] Aiguier, M., Bahrami, D.: Structures for abstract rewriting. Technical report, IBISC, University of Evry, (2006) Long version of the present paper available at http://www.lami.univ-evry.fr/$$\sim$$aiguier/publications.php · Zbl 1125.03011 [2] Aiguier, M., Bahrami, D., Dubois, C.: On a generalised logicality theorem. In: Artificial Intelligence, Automated Reasoning, and Symbolic Computation (AISC). Lecture Notes in Artificial Intelligence, vol. 2385, pp. 51–64. Springer, Berlin Heidelberg New York (2002) · Zbl 1072.68536 [3] Aiguier, M., Boin, C., Longuet, D.: On generalized theorems for normalization of proof trees. Technical report, LaMI, University of Evry val-d’Essonne (2005) [4] Astesiano, E., Cerioli, M.: Free objects and equational deduction for partial conditional specifications. Theor. Comp. Sci. 152, 91–138 (1995) · Zbl 0872.68114 · doi:10.1016/0304-3975(95)00246-5 [5] Baader, F., Nipkow, T.: Term Rewriting and All That. C.U. Press (1998) · Zbl 0948.68098 [6] Bachmair, L.: Canonical Equational Proofs. Progress in Theoretical Computer Science. Birkhäuser Springer (1991) [7] Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236–276 (1994) · Zbl 0806.68095 · doi:10.1145/174652.174655 [8] Bachmair, L., Dershowitz, N., Plaisted, D.-A.: Resolution of Equations in Algebraic Structures. Rewriting Techniques, Chapter Completion without Failure, vol. II, pp. 1–30. Academic (1989) [9] Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: Proceedings of the Annual Symposium on Logic in Computer Science, pp. 384–393. IEEE Computer Society Press, Los Alamitos, CA (1994) · Zbl 0814.68117 [10] Bernot, G., Le Gall, P., Aiguier, M.: Label algebras and exception handling. Sci. Comput. Program. 23, 227–286 (1994) · Zbl 0830.68089 · doi:10.1016/0167-6423(94)00021-2 [11] Bonacina, M.-P., Dershowitz, N.: Abstract canonical inference. ACM Trans. Comput. Log. 8(1) (2008) · Zbl 1165.03309 [12] Bonacina, M.-P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theor. Comput. Sci. 146, 199–242 (1995) · Zbl 0873.68107 · doi:10.1016/0304-3975(94)00187-N [13] Buchberger, B.: Gröbner bases: An algorithmic method in polynomial ideal theory. In: Bose, N.-K.(ed.) Multidimensional Systems Theory, pp. 184–232 (1985) · Zbl 0587.13009 [14] Dershowitz, N.: Canonical sets of horn clauses. In: Leach, A., Monien, B., Rodriguez Artalejo, M. (eds.) Proceedings of the 18th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 510, pp. 267–278. Springer, Berlin Heidelberg New York (1991) · Zbl 0785.68079 [15] Dershowitz, N.: Ordering-based strategies for horn clauses. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence, pp. 118–124 (1991) · Zbl 0745.68089 [16] Dershowitz, N.: Canonicity. In: Dahn, I., Vigneron, L. (eds.) Proceedings of the Fourth International Worshop on First-Order Theorem Proving. Electronic Notes in Theoretical Computer Science, vol. 86. Elsevier, Amsterdam, The Netherlands (2003) [17] Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of TCS. Formal Models and Semantics, vol. B, pp. 243–320. Elsevier, Amsterdam, The Netherlands (1990) · Zbl 0900.68283 [18] Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theor. Comput. Sci. 357(1), 53–69 (2006) · Zbl 1099.03047 · doi:10.1016/j.tcs.2006.03.012 [19] Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theor. Comput. Sci. 75, 111–138 (1990) · Zbl 0702.68034 · doi:10.1016/0304-3975(90)90064-O [20] Dershowitz, N., Okada, M., Sivakumar, G.: Canonical conditional rewrite systems. In: Lusk, E., Overbeek, R. (eds.) CADE. Lecture Notes in Computer Science, vol. 310, pp. 538–549. Springer, Berlin Heidelberg New York (1988) · Zbl 0667.68043 [21] Ehrig, H., Grosse-Rhode, M., Wolter, U.: On the role of category theory in the area of algebraic specification. In: Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol. 1130, pp. 17–48. Springer, Berlin Heidelberg New York (1995) [22] Fiadeiro, J., Sernadas, A.: Structuring theories on consequence. In: Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol. 332, pp. 44–72. Springer, Berlin Heidelberg New York (1988) [23] Freese, R., Jecek, J., Nation, J.: Term rewriting system for lattice theory. J. Symb. Comput. 16(3), 279–288 (1993) · Zbl 0790.06008 · doi:10.1006/jsco.1993.1046 [24] Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524 [25] Gonthier, G., Lévy, J.-J., Melliès, P.-A.: An abstract standardisation theorem. In: Annual Symposium on Logic in Computer Science, pp. 72–81. IEEE Computer Society Press, Los Alamitos, CA (1992) [26] Hsiang, J.: Refutational theorem proving using term rewriting systems. Artif. Intell. 25, 255–300 (1985) · Zbl 0558.68072 · doi:10.1016/0004-3702(85)90074-8 [27] Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottman, Th. (ed.) Proceedings of the 14th International Conference on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 267, pp. 54–71. Springer, Berlin Heidelberg New York (1987) · Zbl 0625.68068 [28] Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155–1196 (1986) · Zbl 0665.03005 · doi:10.1137/0215084 [29] Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebras, pp. 263–297. Pergamon, New York (1970) · Zbl 0188.04902 [30] Kounalis, E., Rusinowitch, M.: On word problems in horn theories. J. Symb. Comput. 11(1-2), 113–128 (1991) · Zbl 0723.68100 · doi:10.1016/S0747-7171(08)80134-4 [31] Lankford, D.: Some approaches to equality for computational logic: A survey and assessment. Memo ATP-36, Automatic Theorem Proving Project. University of Texas, Austin (1977) [32] Levy, J., Agustí, J.: Bi-rewrite systems. J. Symb. Comput. 22, 279–314 (1996) · Zbl 0865.68070 · doi:10.1006/jsco.1996.0053 [33] Lévy, J.-J.: Réductions correctes et optimales dans le $$\lambda$$-calcul. Thèse de doctorat d’Etat, Université Paris 7 (1978) [34] Melliès, P.-A.: Description abstraite des systèmes de réécriture. Ph.D. thesis, Université Paris 7 (1996) [35] Melliès, P.-A.: A stability theorem in rewriting theory. In: Annual Symposium on Logic in Computer Science, pp. 287–299. IEEE Computer Society Press, Los Alamitos, CA (1998) · Zbl 0945.03529 [36] Meseguer, J.: General logics. In: Logic Colloq.’87, pp. 275–329. Holland (1989) [37] Peterson, G.-E., Stickel, M.-E.: Complete sets of reductions for some equational theories. J. ACM 28, 223–264 (1981) · Zbl 0479.68092 · doi:10.1145/322248.322251 [38] Salibra, A., Scollo, G.: A soft stairway to institutions. In: Bidoit, M., Choppy, C. (eds.) Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol. 655, pp. 310–329. Springer, Berlin Heidelberg New York (1993) [39] Schorlemmer, M.: Term rewriting in a logic of special relations. In: Proceedings of the Third International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science, vol. 15. North Holland, Amsterdam, The Netherlands (1998) · Zbl 0917.68109 [40] Schorlemmer, M.: On specifying and reasoning with special relations. In: Monografies de l’IIIA, vol. 10 of IIIA-CSIC Monograph. Institut d’Investigaciò en Intel$$\cdot$$ligència Artificial (CSIC) (1999) · Zbl 0924.03048 [41] Schorlemmer, M.: Term rewriting in a logic of special relations. In: Proceedings of Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, vol. 1546, pp. 178–195. Springer, Berlin Heidelberg New York (1999) · Zbl 0924.03048 [42] Struth, G.: Non-symmetric rewriting. Technical report, MPI für Informatik (1996) [43] Struth, G.: On the word problem for free lattices. In: Comon, H. (ed) Proceedings of Rewriting Techniques and Applications. Lecture Notes in Computer Science, vol. 1232, pp. 128–141. Springer, Berlin Heidelberg New York (1997) · Zbl 1379.06003 [44] Struth, G.: Canonical transformations in algebra, universal algebra and logic. Ph.D. thesis, Institut Für Informatik, University of Saarlandes (1998) [45] Struth, G.: Knuth-bendix completion for non-symmetric transitive relations. In: van den Brand, M., Verma, R. (eds.) Proceedings of the Second International Workshop on Rule-Based Programming (RULE2001). Electronic Notes in Theoretical Computer Science, vol. 59. Elsevier, Amsterdam, The Netherlands (2001) · Zbl 1268.68068
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.