Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent...

Full description

Autores:
Rocha, Camilo
Meseguer, José
Tipo de recurso:
Part of book
Fecha de publicación:
2010
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1901
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1901
Palabra clave:
Término de tierra
árbol autómata
Lógica Ecuacional
Tipo de datos abstractos
Reescribir la teoría
Ground Term
Tree Automaton
Equational Logic
Abstract Data Type
Rewrite Theory
Rights
closedAccess
License
© Springer-Verlag Berlin Heidelberg 2010
id ESCUELAIG2_a02fce13966e6955636aeadbed10d6a3
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1901
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
title Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
spellingShingle Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
Término de tierra
árbol autómata
Lógica Ecuacional
Tipo de datos abstractos
Reescribir la teoría
Ground Term
Tree Automaton
Equational Logic
Abstract Data Type
Rewrite Theory
title_short Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
title_full Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
title_fullStr Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
title_full_unstemmed Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
title_sort Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
dc.creator.fl_str_mv Rocha, Camilo
Meseguer, José
dc.contributor.author.none.fl_str_mv Rocha, Camilo
Meseguer, José
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.spa.fl_str_mv Término de tierra
árbol autómata
Lógica Ecuacional
Tipo de datos abstractos
Reescribir la teoría
topic Término de tierra
árbol autómata
Lógica Ecuacional
Tipo de datos abstractos
Reescribir la teoría
Ground Term
Tree Automaton
Equational Logic
Abstract Data Type
Rewrite Theory
dc.subject.proposal.eng.fl_str_mv Ground Term
Tree Automaton
Equational Logic
Abstract Data Type
Rewrite Theory
description Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.
publishDate 2010
dc.date.issued.none.fl_str_mv 2010
dc.date.accessioned.none.fl_str_mv 2021-12-03T20:28:45Z
dc.date.available.none.fl_str_mv 2021-12-03T20:28:45Z
dc.type.spa.fl_str_mv Artículo de revista
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.version.spa.fl_str_mv info:eu-repo/semantics/publishedVersion
dc.type.coar.spa.fl_str_mv http://purl.org/coar/resource_type/c_3248
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/bookPart
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/ART
format http://purl.org/coar/resource_type/c_3248
status_str publishedVersion
dc.identifier.isbn.none.fl_str_mv 9783642162428
9783642162411
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1901
identifier_str_mv 9783642162428
9783642162411
url https://repositorio.escuelaing.edu.co/handle/001/1901
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.ispartofseries.none.fl_str_mv Lecture Notes in Computer Science;6397
dc.relation.citationendpage.spa.fl_str_mv 609
dc.relation.citationstartpage.spa.fl_str_mv 594
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.ispartofbook.eng.fl_str_mv Logic for Programming, Artificial Intelligence, and Reasoning
dc.relation.references.spa.fl_str_mv Avenhaus, J., Hillenbrand, T., Löchner, B.: On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation 36(1-2), 217–233 (2003)
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Kaci, A.H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. 2, pp. 1–30. Academic Press, New York (1989)
Becker, K.: Proving ground confluence and inductive validity in constructor based equational specifications. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 46–60. Springer, Heidelberg (1993) ISBN 3-540-56610-4
Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science 170(1-2), 245–276 (1996)
Bouhoula, A.: Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Transactions on Computational Logic 10(3) (2009)
Bouhoula, A., Jacquemard, F.: Automated induction with constrained tree automata. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 539–554. Springer, Heidelberg (2008)
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236(1-2), 35–132 (2000)
Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Comon, H.: Sufficient completness, term rewriting systems and “anti-unification”. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 3–540. Springer, Heidelberg (1986), ISBN 3-540-16780-3
Comon, H.: An effective method for handling initial algebras. In: Grabowski, J., Wechler, W., Lescanne, P. (eds.) ALP 1988. LNCS, vol. 343, pp. 108–118. Springer, Heidelberg (1989), ISBN 3-540-50667-5
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007)
Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Information and Computation 187(1), 123–153 (2003)
Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Bossi, A., Maher, M.J. (eds.) PPDP, pp. 121–132. ACM, New York (2006) ISBN 1-59593-388-3
Guttag, J.: The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, Computer Science Department (1975)
Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978)
Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)
Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005), ISBN 3-540-25596-6
Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229–245. Springer, Heidelberg (2007), ISBN 978-3-540-73447-5
Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 50–65. Springer, Heidelberg (2006), ISBN 3-540-36834-5
Huet, G.P., Hullot, J.-M.: Proofs by induction in equational theories with constructors. In: FOCS, pp. 96–107. IEEE, Los Alamitos (1980)
Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation 82(1), 1–33 (1989)
Kapur, D., Narendran, P., Otto, F.: On ground-confluence of term rewriting systems. Information and Computation 86(1), 14–31 (1990)
Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)
Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24(4), 395–415 (1987)
Kounalis, E.: Testing for the ground (co-)reducibility property in term-rewriting systems. Theoretical Computer Science 106(1), 87–117 (1992)
Lazrek, A., Lescanne, P., Thiel, J.-J.: Tools for proving inductive equalities, relative completeness, and omega-completeness. Information and Computation 84(1), 47–70 (1990)
Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366–380. Springer, Heidelberg (1990), ISBN 3-540-52885-7
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) GI-TCS 1983. LNCS, vol. 145, pp. 257–268. Springer, Heidelberg (1982), ISBN 3-540-11973-6
Plaisted, D.: Semantic confluence tests and completion methods. Information and Control 65, 182–215 (1985)
Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of generalized rewrite theories. Technical report, University of Illinois at Urbana-Champaign (2010)
Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)
dc.rights.eng.fl_str_mv © Springer-Verlag Berlin Heidelberg 2010
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_14cb
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/closedAccess
rights_invalid_str_mv © Springer-Verlag Berlin Heidelberg 2010
http://purl.org/coar/access_right/c_14cb
eu_rights_str_mv closedAccess
dc.format.extent.spa.fl_str_mv 16 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv Springer
dc.publisher.place.spa.fl_str_mv Berlín
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1901/3/Constructors%2c%20Sufficient%20Completeness%2c%20and%20Deadlock%20Freedom%20of%20Rewrite%20Theories.png
https://repositorio.escuelaing.edu.co/bitstream/001/1901/4/Constructors%2c%20Sufficient%20Completeness%2c%20and%20Deadlock%20Freedom%20of%20Rewrite%20Theories.png.jpg
https://repositorio.escuelaing.edu.co/bitstream/001/1901/1/Constructors%2c%20Sufficient%20Completeness%2c%20and%20Deadlock%20Freedom%20of%20Rewrite%20Theories.png
https://repositorio.escuelaing.edu.co/bitstream/001/1901/2/license.txt
bitstream.checksum.fl_str_mv a76443d19093f0d5e1f61f3afc8740a2
e3bcb0fc3d60b66dfdd30ccff1c8ffe1
3f0747fcd06557bd8818f21345266072
5a7ca94c2e5326ee169f979d71d0f06e
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Escuela Colombiana de Ingeniería Julio Garavito
repository.mail.fl_str_mv repositorio.eci@escuelaing.edu.co
_version_ 1814355595330846720
spelling Rocha, Camiloebfd407af468605647a49186059da397600Meseguer, José6da02984a567cfba226ed9b8bf7c47c0600Informática2021-12-03T20:28:45Z2021-12-03T20:28:45Z201097836421624289783642162411https://repositorio.escuelaing.edu.co/handle/001/1901Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.Se ha estudiado a fondo la integridad suficiente para las especificaciones de ecuaciones, donde los símbolos de función se clasifican en constructores y símbolos definidos. Pero, ¿qué debería significar suficiente completitud para reescribir la teoría R=(Σ,E,R) con ecuaciones E y reglas no ecuacionales R que describen transiciones concurrentes en un sistema? Este trabajo argumenta que una teoría de reescritura tiene naturalmente dos nociones de constructor: la habitual para sus ecuaciones E, y otra diferente para sus reglas R. La suficiente completitud de constructores para las reglas R resulta estar íntimamente relacionada con la libertad de interbloqueo, es decir, R no tiene interbloqueos fuera de los constructores de R. La relación entre estas dos nociones se estudia en el marco de las teorías de reescritura ordenadas por orden incondicional. Se dan condiciones suficientes que permiten la comprobación automática de la integridad suficiente, la libertad de interbloqueo y otras propiedades relacionadas, mediante axiomas ecuacionales de módulos de autómatas proposicionales como la asociatividad, la conmutatividad y la identidad. Se utilizan para extender el verificador de integridad suficiente de Maude desde la verificación de teorías ecuacionales hasta la de teorías ecuacionales y de reescritura. Finalmente, se caracteriza e ilustra con un ejemplo la utilidad de la noción de constructores propuesta para probar teoremas inductivos sobre la relación de reescritura de alcanzabilidad →R asociada a una teoría de reescritura R (y también sobre la relación de capacidad de unión ↓R).16 páginas.application/pdfengSpringerBerlínLecture Notes in Computer Science;6397609594N/ALogic for Programming, Artificial Intelligence, and ReasoningAvenhaus, J., Hillenbrand, T., Löchner, B.: On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation 36(1-2), 217–233 (2003)Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Kaci, A.H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. 2, pp. 1–30. Academic Press, New York (1989)Becker, K.: Proving ground confluence and inductive validity in constructor based equational specifications. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 46–60. Springer, Heidelberg (1993) ISBN 3-540-56610-4Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science 170(1-2), 245–276 (1996)Bouhoula, A.: Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Transactions on Computational Logic 10(3) (2009)Bouhoula, A., Jacquemard, F.: Automated induction with constrained tree automata. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 539–554. Springer, Heidelberg (2008)Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236(1-2), 35–132 (2000)Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)Comon, H.: Sufficient completness, term rewriting systems and “anti-unification”. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 3–540. Springer, Heidelberg (1986), ISBN 3-540-16780-3Comon, H.: An effective method for handling initial algebras. In: Grabowski, J., Wechler, W., Lescanne, P. (eds.) ALP 1988. LNCS, vol. 343, pp. 108–118. Springer, Heidelberg (1989), ISBN 3-540-50667-5Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007)Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Information and Computation 187(1), 123–153 (2003)Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Bossi, A., Maher, M.J. (eds.) PPDP, pp. 121–132. ACM, New York (2006) ISBN 1-59593-388-3Guttag, J.: The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, Computer Science Department (1975)Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978)Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005), ISBN 3-540-25596-6Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229–245. Springer, Heidelberg (2007), ISBN 978-3-540-73447-5Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 50–65. Springer, Heidelberg (2006), ISBN 3-540-36834-5Huet, G.P., Hullot, J.-M.: Proofs by induction in equational theories with constructors. In: FOCS, pp. 96–107. IEEE, Los Alamitos (1980)Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation 82(1), 1–33 (1989)Kapur, D., Narendran, P., Otto, F.: On ground-confluence of term rewriting systems. Information and Computation 86(1), 14–31 (1990)Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24(4), 395–415 (1987)Kounalis, E.: Testing for the ground (co-)reducibility property in term-rewriting systems. Theoretical Computer Science 106(1), 87–117 (1992)Lazrek, A., Lescanne, P., Thiel, J.-J.: Tools for proving inductive equalities, relative completeness, and omega-completeness. Information and Computation 84(1), 47–70 (1990)Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366–380. Springer, Heidelberg (1990), ISBN 3-540-52885-7Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) GI-TCS 1983. LNCS, vol. 145, pp. 257–268. Springer, Heidelberg (1982), ISBN 3-540-11973-6Plaisted, D.: Semantic confluence tests and completion methods. Information and Control 65, 182–215 (1985)Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of generalized rewrite theories. Technical report, University of Illinois at Urbana-Champaign (2010)Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)© Springer-Verlag Berlin Heidelberg 2010info:eu-repo/semantics/closedAccesshttp://purl.org/coar/access_right/c_14cbConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite TheoriesArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85Término de tierraárbol autómataLógica EcuacionalTipo de datos abstractosReescribir la teoríaGround TermTree AutomatonEquational LogicAbstract Data TypeRewrite TheoryTHUMBNAILConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.pngConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.pngimage/png132542https://repositorio.escuelaing.edu.co/bitstream/001/1901/3/Constructors%2c%20Sufficient%20Completeness%2c%20and%20Deadlock%20Freedom%20of%20Rewrite%20Theories.pnga76443d19093f0d5e1f61f3afc8740a2MD53open accessConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.png.jpgConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.png.jpgGenerated Thumbnailimage/jpeg2213https://repositorio.escuelaing.edu.co/bitstream/001/1901/4/Constructors%2c%20Sufficient%20Completeness%2c%20and%20Deadlock%20Freedom%20of%20Rewrite%20Theories.png.jpge3bcb0fc3d60b66dfdd30ccff1c8ffe1MD54open accessORIGINALConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.pngConstructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories.pngimage/png7252https://repositorio.escuelaing.edu.co/bitstream/001/1901/1/Constructors%2c%20Sufficient%20Completeness%2c%20and%20Deadlock%20Freedom%20of%20Rewrite%20Theories.png3f0747fcd06557bd8818f21345266072MD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1901/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open access001/1901oai:repositorio.escuelaing.edu.co:001/19012022-12-13 03:01:17.527open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK

Publicaciones similares