Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles

Presentamos un algoritmo de unificación general módulo Presburger Arithmetic para una clase restringida de teorías especificadas modularmente donde los símbolos de función de la teoría objetivo tienen clases de codominio no aritméticas. Además, comentamos las condiciones que garantizan la decidibili...

Full description

Autores:
Ayala Rincón, Mauricio
Tavares Araújo, Ivan E.
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2001
Institución:
Universidad Autónoma de Bucaramanga - UNAB
Repositorio:
Repositorio UNAB
Idioma:
spa
OAI Identifier:
oai:repository.unab.edu.co:20.500.12749/9069
Acceso en línea:
http://hdl.handle.net/20.500.12749/9069
Palabra clave:
Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Algebraic specification
Equational unification
Algebraic specification
Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de Sistemas
Investigación
Unificación ecuacional
Razonamiento automatizado
Especificación algebraica
Rights
License
Derechos de autor 2001 Revista Colombiana de Computación
id UNAB2_17c9af2432ab88fb0d09a1a44b0bf5df
oai_identifier_str oai:repository.unab.edu.co:20.500.12749/9069
network_acronym_str UNAB2
network_name_str Repositorio UNAB
repository_id_str
dc.title.none.fl_str_mv Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
dc.title.translated.none.fl_str_mv Unification modulo presburger arithmetic and other decidable theories
title Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
spellingShingle Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Algebraic specification
Equational unification
Algebraic specification
Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de Sistemas
Investigación
Unificación ecuacional
Razonamiento automatizado
Especificación algebraica
title_short Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
title_full Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
title_fullStr Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
title_full_unstemmed Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
title_sort Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
dc.creator.fl_str_mv Ayala Rincón, Mauricio
Tavares Araújo, Ivan E.
dc.contributor.author.spa.fl_str_mv Ayala Rincón, Mauricio
Tavares Araújo, Ivan E.
dc.contributor.googlescholar.spa.fl_str_mv Ayala Rincón, Mauricio [hd3UcpsAAAAJ]
dc.contributor.orcid.spa.fl_str_mv Ayala Rincón, Mauricio [0000-0003-0089-3905]
Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]
dc.contributor.researchgate.spa.fl_str_mv Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]
dc.subject.none.fl_str_mv Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
topic Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Algebraic specification
Equational unification
Algebraic specification
Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de Sistemas
Investigación
Unificación ecuacional
Razonamiento automatizado
Especificación algebraica
dc.subject.keywords.eng.fl_str_mv Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Algebraic specification
Equational unification
Algebraic specification
dc.subject.lemb.spa.fl_str_mv Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de Sistemas
Investigación
dc.subject.proposal.spa.fl_str_mv Unificación ecuacional
Razonamiento automatizado
Especificación algebraica
description Presentamos un algoritmo de unificación general módulo Presburger Arithmetic para una clase restringida de teorías especificadas modularmente donde los símbolos de función de la teoría objetivo tienen clases de codominio no aritméticas. Además, comentamos las condiciones que garantizan la decidibilidad de problemas de emparejamiento y unificación módulo teorías más generales que las aritméticas, que aparecen cuando se implementa la deducción automática combinando técnicas de reescritura condicional y algoritmos de decisión para predicados incorporados.
publishDate 2001
dc.date.issued.none.fl_str_mv 2001-12-01
dc.date.accessioned.none.fl_str_mv 2020-10-27T00:21:33Z
dc.date.available.none.fl_str_mv 2020-10-27T00:21:33Z
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.driver.none.fl_str_mv info:eu-repo/semantics/article
dc.type.local.spa.fl_str_mv Artículo
dc.type.coar.none.fl_str_mv http://purl.org/coar/resource_type/c_7a1f
dc.type.redcol.none.fl_str_mv http://purl.org/redcol/resource_type/CJournalArticle
format http://purl.org/coar/resource_type/c_7a1f
dc.identifier.issn.none.fl_str_mv 2539-2115
1657-2831
dc.identifier.uri.none.fl_str_mv http://hdl.handle.net/20.500.12749/9069
dc.identifier.instname.spa.fl_str_mv instname:Universidad Autónoma de Bucaramanga UNAB
dc.identifier.repourl.none.fl_str_mv repourl:https://repository.unab.edu.co
identifier_str_mv 2539-2115
1657-2831
instname:Universidad Autónoma de Bucaramanga UNAB
repourl:https://repository.unab.edu.co
url http://hdl.handle.net/20.500.12749/9069
dc.language.iso.spa.fl_str_mv spa
language spa
dc.relation.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1112/1083
dc.relation.uri.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1112
dc.relation.references.none.fl_str_mv M. Ayala-Rinc on. Expressiveness of Conditional Equational Systems with Builtin Predicates. PhD thesis, Universit at Kaiserslautern, Kaiserslautern (Germany), December 1993.
M. Ayala-Rinc on. Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises. In D. M. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, Studies on Logic and Computation, 7, chapter 2, pages 17{38. Research Studies Press/Wiley, 2000.
M. Ayala-Rinc on and L. M. R. Gadelha. Some Applications of (Semi-)Decision Algorithms for Presburger Arithmetic in Automated Deduction based on Rewriting Techniques. La Revista de La Sociedad Chilena de Ciencia de la Computaci on, 2(1):14{23, 1997.
J. Barwise, editor. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the foundations of Mathematics. North-Holland, 1977.
F. Baader and W. Nutt. Combination Problems for Commutative/Monoidal Theories or How Algebra Can Help in Equational Uni cation. Journal of Applicable Algebra in Engineering, Communication and Computing, 7(4):309{337, 1996.
F. Baader and J. H. Siekmann. Uni cation Theory. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Arti cial Intel ligence and Logic Programming, pages 41{125. Oxford University Press, 1994.
F. Baader and K. U. Schulz. Uni cation in the Union of Disjoint Equational Theories: Combining Decision Procedures. Journal of Symbolic Computation, 21:211{243, 1996.
F. Baader and W. Snyder. Uni cation Theory. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999.
D. C. Cooper. Theorem Proving in Arithmetic without Multiplication. Machine Intel ligence, 7:91{99, 1972.
I. E. T. de Ara ujo and M. Ayala-Rinc on. An Algorithm for General Uni cation Modulo Presburger Arithmetic. In I Brazilian Workshop on Formal Methods, Porto Alegre, Brazil, pages 146{151, October 1998.
N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume 2, chapte
C. Hosono and Y. Ikeda. A Formal Derivation of the Theory SA. Theoretical Computer Science, 127:1{23, 1994.
Y. Ikeda, K. Tomita, and C. Hosono. A Programming Language SAMPL and its Interpreter. Unpublished document.
D. Kapur and M. Subramaniam. New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. Journal of Automated Reasoning, 16(1/2), 1996.
W. Nutt. Uni cation in Monoidal Theories is Solving Linear Equations over Semirings. Research Report RR-92-01, Deutsche Forschungszentrum f ur K unstliche Intelligenz, DFKI GmbH, Stuhlsatzenhausweg 3, D-66123 Saarbr ucken, Germany, 1992.
M. Presburger. Uber die V ollst andigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In 1. Kongres matematyk ow krajow slowia nskich, Warsaw, pages 92{101, 1929. In German.
R. E. Shostak. On the SUP-INF Method for Proving Presburger Formulas. Journal of the Association for Computing Machinery, 24(4):529{543, October 1977.
R. E. Shostak. A Practical Decision Procedure for Arithmetic with Function Symbols. Journal of the Association for Computing Machinery, 26(2):351{360, April 1979.
dc.rights.none.fl_str_mv Derechos de autor 2001 Revista Colombiana de Computación
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.uri.*.fl_str_mv http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rights.uri.none.fl_str_mv http://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.rights.creativecommons.*.fl_str_mv Attribution-NonCommercial-ShareAlike 4.0 International
rights_invalid_str_mv Derechos de autor 2001 Revista Colombiana de Computación
http://creativecommons.org/licenses/by-nc-sa/4.0/
http://creativecommons.org/licenses/by-nc-nd/2.5/co/
Attribution-NonCommercial-ShareAlike 4.0 International
http://purl.org/coar/access_right/c_abf2
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.none.fl_str_mv Universidad Autónoma de Bucaramanga UNAB
publisher.none.fl_str_mv Universidad Autónoma de Bucaramanga UNAB
dc.source.none.fl_str_mv Revista Colombiana de Computación; Vol. 2 Núm. 2 (2001): Revista Colombiana de Computación; 1-14
institution Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv https://repository.unab.edu.co/bitstream/20.500.12749/9069/1/Modulo%20de%20unificaci%c3%b3n%20aritm%c3%a9tica%20pre-hamburguesa%20y%20otras%20teor%c3%adas%20decidibles.pdf
https://repository.unab.edu.co/bitstream/20.500.12749/9069/2/Modulo%20de%20unificaci%c3%b3n%20aritm%c3%a9tica%20pre-hamburguesa%20y%20otras%20teor%c3%adas%20decidibles.pdf.jpg
bitstream.checksum.fl_str_mv e1f109291d992fcea94c2ae30627bf34
7fcf39ccf0ea8e9e1e7e9224dadb2fb3
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
repository.name.fl_str_mv Repositorio Institucional | Universidad Autónoma de Bucaramanga - UNAB
repository.mail.fl_str_mv repositorio@unab.edu.co
_version_ 1814277313349550080
spelling Ayala Rincón, Mauriciof681e303-3263-42cb-a9d5-96197d20d516Tavares Araújo, Ivan E.0f85b692-42cc-4fbc-85ac-9b3bf3efa202Ayala Rincón, Mauricio [hd3UcpsAAAAJ]Ayala Rincón, Mauricio [0000-0003-0089-3905]Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]2020-10-27T00:21:33Z2020-10-27T00:21:33Z2001-12-012539-21151657-2831http://hdl.handle.net/20.500.12749/9069instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coPresentamos un algoritmo de unificación general módulo Presburger Arithmetic para una clase restringida de teorías especificadas modularmente donde los símbolos de función de la teoría objetivo tienen clases de codominio no aritméticas. Además, comentamos las condiciones que garantizan la decidibilidad de problemas de emparejamiento y unificación módulo teorías más generales que las aritméticas, que aparecen cuando se implementa la deducción automática combinando técnicas de reescritura condicional y algoritmos de decisión para predicados incorporados.We present a general uni cation algorithm modulo Presburger Arithmetic for a re- stricted class of modularly speci ed theories where function symbols of the target theory have non arithmetic codomain sorts. Additionally, we comment on conditions guaran-teeing decidability of matching and uni cation problems modulo more general theories than the arithmetic ones, which appear when automated deduction is implemented by combining conditional rewriting techniques and decision algorithms for built-in predi- cates.application/pdfspaUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/1112/1083https://revistas.unab.edu.co/index.php/rcc/article/view/1112M. Ayala-Rinc on. Expressiveness of Conditional Equational Systems with Builtin Predicates. PhD thesis, Universit at Kaiserslautern, Kaiserslautern (Germany), December 1993.M. Ayala-Rinc on. Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises. In D. M. Gabbay and M. de Rijke, editors, Frontiers of Combining Systems 2, Studies on Logic and Computation, 7, chapter 2, pages 17{38. Research Studies Press/Wiley, 2000.M. Ayala-Rinc on and L. M. R. Gadelha. Some Applications of (Semi-)Decision Algorithms for Presburger Arithmetic in Automated Deduction based on Rewriting Techniques. La Revista de La Sociedad Chilena de Ciencia de la Computaci on, 2(1):14{23, 1997.J. Barwise, editor. Handbook of Mathematical Logic, volume 90 of Studies in Logic and the foundations of Mathematics. North-Holland, 1977.F. Baader and W. Nutt. Combination Problems for Commutative/Monoidal Theories or How Algebra Can Help in Equational Uni cation. Journal of Applicable Algebra in Engineering, Communication and Computing, 7(4):309{337, 1996.F. Baader and J. H. Siekmann. Uni cation Theory. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Arti cial Intel ligence and Logic Programming, pages 41{125. Oxford University Press, 1994.F. Baader and K. U. Schulz. Uni cation in the Union of Disjoint Equational Theories: Combining Decision Procedures. Journal of Symbolic Computation, 21:211{243, 1996.F. Baader and W. Snyder. Uni cation Theory. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999.D. C. Cooper. Theorem Proving in Arithmetic without Multiplication. Machine Intel ligence, 7:91{99, 1972.I. E. T. de Ara ujo and M. Ayala-Rinc on. An Algorithm for General Uni cation Modulo Presburger Arithmetic. In I Brazilian Workshop on Formal Methods, Porto Alegre, Brazil, pages 146{151, October 1998.N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume 2, chapteC. Hosono and Y. Ikeda. A Formal Derivation of the Theory SA. Theoretical Computer Science, 127:1{23, 1994.Y. Ikeda, K. Tomita, and C. Hosono. A Programming Language SAMPL and its Interpreter. Unpublished document.D. Kapur and M. Subramaniam. New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. Journal of Automated Reasoning, 16(1/2), 1996.W. Nutt. Uni cation in Monoidal Theories is Solving Linear Equations over Semirings. Research Report RR-92-01, Deutsche Forschungszentrum f ur K unstliche Intelligenz, DFKI GmbH, Stuhlsatzenhausweg 3, D-66123 Saarbr ucken, Germany, 1992.M. Presburger. Uber die V ollst andigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In 1. Kongres matematyk ow krajow slowia nskich, Warsaw, pages 92{101, 1929. In German.R. E. Shostak. On the SUP-INF Method for Proving Presburger Formulas. Journal of the Association for Computing Machinery, 24(4):529{543, October 1977.R. E. Shostak. A Practical Decision Procedure for Arithmetic with Function Symbols. Journal of the Association for Computing Machinery, 26(2):351{360, April 1979.Derechos de autor 2001 Revista Colombiana de Computaciónhttp://creativecommons.org/licenses/by-nc-sa/4.0/http://creativecommons.org/licenses/by-nc-nd/2.5/co/Attribution-NonCommercial-ShareAlike 4.0 Internationalhttp://purl.org/coar/access_right/c_abf2Revista Colombiana de Computación; Vol. 2 Núm. 2 (2001): Revista Colombiana de Computación; 1-14Innovaciones tecnológicasCiencia de los computadoresDesarrollo de tecnologíaIngeniería de sistemasInvestigacionesTecnologías de la información y las comunicacionesTIC´sTechnological innovationsComputer scienceTechnology developmentSystems engineeringInvestigationsInformation and communication technologiesICT'sAlgebraic specificationEquational unificationAlgebraic specificationInnovaciones tecnológicasCiencias de la ComputaciónDesarrollo tecnológicoIngeniería de SistemasInvestigaciónUnificación ecuacionalRazonamiento automatizadoEspecificación algebraicaMódulo de unificación aritmética pre-hamburguesa y otras teorías decidiblesUnification modulo presburger arithmetic and other decidable theoriesinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticleORIGINALModulo de unificación aritmética pre-hamburguesa y otras teorías decidibles.pdfModulo de unificación aritmética pre-hamburguesa y otras teorías decidibles.pdfArtículoapplication/pdf550159https://repository.unab.edu.co/bitstream/20.500.12749/9069/1/Modulo%20de%20unificaci%c3%b3n%20aritm%c3%a9tica%20pre-hamburguesa%20y%20otras%20teor%c3%adas%20decidibles.pdfe1f109291d992fcea94c2ae30627bf34MD51open accessTHUMBNAILModulo de unificación aritmética pre-hamburguesa y otras teorías decidibles.pdf.jpgModulo de unificación aritmética pre-hamburguesa y otras teorías decidibles.pdf.jpgIM Thumbnailimage/jpeg7852https://repository.unab.edu.co/bitstream/20.500.12749/9069/2/Modulo%20de%20unificaci%c3%b3n%20aritm%c3%a9tica%20pre-hamburguesa%20y%20otras%20teor%c3%adas%20decidibles.pdf.jpg7fcf39ccf0ea8e9e1e7e9224dadb2fb3MD52open access20.500.12749/9069oai:repository.unab.edu.co:20.500.12749/90692022-11-24 14:56:49.601open accessRepositorio Institucional | Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Publicaciones similares