Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos

Presentamos un procedimiento de decisión ecuacional a la Dijkstra & Scholten para la 'Lógica Silogística con Complementos'. Primero, damos una axiomatización ecuacional de la lógica proposicional de Dijkstra & Scholten y mostramos cómo da un procedimiento de decisión para la lógica...

Full description

Autores:
Rocha, Camilo
Meseguer, José
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2007
Institución:
Universidad Autónoma de Bucaramanga - UNAB
Repositorio:
Repositorio UNAB
Idioma:
spa
OAI Identifier:
oai:repository.unab.edu.co:20.500.12749/8996
Acceso en línea:
http://hdl.handle.net/20.500.12749/8996
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
Syllogistic logic with complements
Decision procedure
Equational logic
Rewriting logic
Maude
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
Lógica silogística con complementos
Procedimiento de decisión
Lógica ecuacional
Reescritura de lógica
Rights
License
Derechos de autor 2007 Revista Colombiana de Computación
id UNAB2_1adb645511af80a3d6d03bc0e5fb0030
oai_identifier_str oai:repository.unab.edu.co:20.500.12749/8996
network_acronym_str UNAB2
network_name_str Repositorio UNAB
repository_id_str
dc.title.spa.fl_str_mv Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
dc.title.translated.eng.fl_str_mv A rewriting decision procedure for Dijkstra-Scholten's syllogistic logic with complements
title Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
spellingShingle Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
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
Syllogistic logic with complements
Decision procedure
Equational logic
Rewriting logic
Maude
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
Lógica silogística con complementos
Procedimiento de decisión
Lógica ecuacional
Reescritura de lógica
title_short Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
title_full Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
title_fullStr Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
title_full_unstemmed Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
title_sort Un procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementos
dc.creator.fl_str_mv Rocha, Camilo
Meseguer, José
dc.contributor.author.spa.fl_str_mv Rocha, Camilo
Meseguer, José
dc.contributor.googlescholar.spa.fl_str_mv Rocha, Camilo [s5LVBc8AAAAJ]
Meseguer, José [KZFo7ZkAAAAJ]
dc.contributor.orcid.spa.fl_str_mv Rocha, Camilo [0000-0003-4356-7704]
Meseguer, José [0000-0003-4779-3848]
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
Syllogistic logic with complements
Decision procedure
Equational logic
Rewriting logic
Maude
Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
Lógica silogística con complementos
Procedimiento de decisión
Lógica ecuacional
Reescritura de lógica
dc.subject.keywords.eng.fl_str_mv Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Syllogistic logic with complements
Decision procedure
Equational logic
Rewriting logic
Maude
dc.subject.lemb.spa.fl_str_mv Innovaciones tecnológicas
Ciencias de la computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y la comunicación
dc.subject.proposal.spa.fl_str_mv Lógica silogística con complementos
Procedimiento de decisión
Lógica ecuacional
Reescritura de lógica
description Presentamos un procedimiento de decisión ecuacional a la Dijkstra & Scholten para la 'Lógica Silogística con Complementos'. Primero, damos una axiomatización ecuacional de la lógica proposicional de Dijkstra & Scholten y mostramos cómo da un procedimiento de decisión para la lógica proposicional mediante la reescritura de términos ecuacionales. También mostramos cómo se pueden obtener de manera eficiente ciertos modelos proposicionales (es decir, asignaciones de verdad sobre variables proposicionales) a partir de las formas canónicas dadas por el sistema. Luego presentamos la Lógica Silogística con Complementos y mostramos cómo el procedimiento de decisión para la lógica proposicional puede extenderse fácilmente para obtener un procedimiento de decisión para este subconjunto de la Lógica Primero•Onier. Además, se presenta una especificación ejecutable de ambos procedimientos de decisión en el sistema de Maude y se dan ejemplos que ilustran el uso de ambos sistemas ecuacionales canónicos.
publishDate 2007
dc.date.issued.none.fl_str_mv 2007-12-01
dc.date.accessioned.none.fl_str_mv 2020-10-27T00:20:58Z
dc.date.available.none.fl_str_mv 2020-10-27T00:20:58Z
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/8996
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/8996
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/1038/1011
dc.relation.uri.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1038
dc.relation.references.none.fl_str_mv Leo Bachmair and Nachum Dershowitz. Inference rules for rewrite-based first-order theorem proving. In LICS, pages 331 {337. IEEE Computer Society, 1987.
D. Basin, M. Clavel, and J. Meseguer. Rewriting logic as a metalogical framework. ACM Transactions on Computational Logic, 5:528 (576, 2004.
George S. Boolos, John P. Burgas, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, 4th edition, 2002.
Mel Bouhoula, Jean-Pierre Jouannaud, and Jose Meseguer. Specification and proof in membership equational logic. Theor. Comput. Sci.,236( I -2):35 (132,2000.
M. Clavel, F. Duren, S. Eker, J. Meseguer, P. Lincoln, N. Mani¬Oliet, and C. Talcott. All About Maude - A High-Performance Logical Framework. Springer LNCS Vol. 43501st edition, 2007.
Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Mani-Oliet, Jose Meseguer, and Jose Quesada. Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285:187 (243, 2002.
Manuel Clavel, Jose Meseguer, and Miguel Palomino. Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic. Electr. Notes Theor. Comput. Sci., 71, 2002.
John Corcoran. Completeness of an ancient logic. J. Symb. Log., 37(4):696 (702, 1972.
Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, 1990.
dc.rights.none.fl_str_mv Derechos de autor 2007 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 2007 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. 8 Núm. 2 (2007): Revista Colombiana de Computación; 101-130
institution Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv https://repository.unab.edu.co/bitstream/20.500.12749/8996/1/2007_Articulo_Un%20procedimiento%20de%20decisi%c3%b3n%20de%20reescritura%20de%20la%20logica%20silogistica.pdf
https://repository.unab.edu.co/bitstream/20.500.12749/8996/2/2007_Articulo_Un%20procedimiento%20de%20decisi%c3%b3n%20de%20reescritura%20de%20la%20logica%20silogistica.pdf.jpg
bitstream.checksum.fl_str_mv 6e21c8f325478089960a6fb91cdfed68
510f7843e9b02ffc0eb5d0c932223990
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_ 1814278024025079808
spelling Rocha, Camiloeb2f6c10-76de-461f-9029-f98650724186Meseguer, José06d2dce5-1dfb-4cd5-b498-dbd99aed370dRocha, Camilo [s5LVBc8AAAAJ]Meseguer, José [KZFo7ZkAAAAJ]Rocha, Camilo [0000-0003-4356-7704]Meseguer, José [0000-0003-4779-3848]2020-10-27T00:20:58Z2020-10-27T00:20:58Z2007-12-012539-21151657-2831http://hdl.handle.net/20.500.12749/8996instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coPresentamos un procedimiento de decisión ecuacional a la Dijkstra & Scholten para la 'Lógica Silogística con Complementos'. Primero, damos una axiomatización ecuacional de la lógica proposicional de Dijkstra & Scholten y mostramos cómo da un procedimiento de decisión para la lógica proposicional mediante la reescritura de términos ecuacionales. También mostramos cómo se pueden obtener de manera eficiente ciertos modelos proposicionales (es decir, asignaciones de verdad sobre variables proposicionales) a partir de las formas canónicas dadas por el sistema. Luego presentamos la Lógica Silogística con Complementos y mostramos cómo el procedimiento de decisión para la lógica proposicional puede extenderse fácilmente para obtener un procedimiento de decisión para este subconjunto de la Lógica Primero•Onier. Además, se presenta una especificación ejecutable de ambos procedimientos de decisión en el sistema de Maude y se dan ejemplos que ilustran el uso de ambos sistemas ecuacionales canónicos.We present an equational decision procedure a la Dijkstra & Scholten for the 'Syllogistic Logic with Complements'. First, we give an equational axiomatization of Dijkstra & Scholten's propositional logic and show how it gives a decision procedure for propositional logic by equational term rewriting. We also show how one can efficiently obtain certain propositional models (i.e., truth assignments over propositional variables) from the canonical forms given by the system. We then present the Syllogistic Logic with Complements and show how the decision procedure for propositional logic can be easily extended to obtain a decision procedure for this subset of First•Onier Logic. Moreover, an executable specification of both decision procedures is presented in the Maude system, and examples illustrating the use of both canonical equational systems are given.application/pdfspaUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/1038/1011https://revistas.unab.edu.co/index.php/rcc/article/view/1038Leo Bachmair and Nachum Dershowitz. Inference rules for rewrite-based first-order theorem proving. In LICS, pages 331 {337. IEEE Computer Society, 1987.D. Basin, M. Clavel, and J. Meseguer. Rewriting logic as a metalogical framework. ACM Transactions on Computational Logic, 5:528 (576, 2004.George S. Boolos, John P. Burgas, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, 4th edition, 2002.Mel Bouhoula, Jean-Pierre Jouannaud, and Jose Meseguer. Specification and proof in membership equational logic. Theor. Comput. Sci.,236( I -2):35 (132,2000.M. Clavel, F. Duren, S. Eker, J. Meseguer, P. Lincoln, N. Mani¬Oliet, and C. Talcott. All About Maude - A High-Performance Logical Framework. Springer LNCS Vol. 43501st edition, 2007.Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Mani-Oliet, Jose Meseguer, and Jose Quesada. Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285:187 (243, 2002.Manuel Clavel, Jose Meseguer, and Miguel Palomino. Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic. Electr. Notes Theor. Comput. Sci., 71, 2002.John Corcoran. Completeness of an ancient logic. J. Symb. Log., 37(4):696 (702, 1972.Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, 1990.Derechos de autor 2007 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. 8 Núm. 2 (2007): Revista Colombiana de Computación; 101-130Innovaciones 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'sSyllogistic logic with complementsDecision procedureEquational logicRewriting logicMaudeInnovaciones tecnológicasCiencias de la computaciónDesarrollo tecnológicoIngeniería de sistemasInvestigacionesTecnologías de la información y la comunicaciónLógica silogística con complementosProcedimiento de decisiónLógica ecuacionalReescritura de lógicaUn procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementosA rewriting decision procedure for Dijkstra-Scholten's syllogistic logic with complementsinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticleORIGINAL2007_Articulo_Un procedimiento de decisión de reescritura de la logica silogistica.pdf2007_Articulo_Un procedimiento de decisión de reescritura de la logica silogistica.pdfArtículoapplication/pdf17440196https://repository.unab.edu.co/bitstream/20.500.12749/8996/1/2007_Articulo_Un%20procedimiento%20de%20decisi%c3%b3n%20de%20reescritura%20de%20la%20logica%20silogistica.pdf6e21c8f325478089960a6fb91cdfed68MD51open accessTHUMBNAIL2007_Articulo_Un procedimiento de decisión de reescritura de la logica silogistica.pdf.jpg2007_Articulo_Un procedimiento de decisión de reescritura de la logica silogistica.pdf.jpgIM Thumbnailimage/jpeg8197https://repository.unab.edu.co/bitstream/20.500.12749/8996/2/2007_Articulo_Un%20procedimiento%20de%20decisi%c3%b3n%20de%20reescritura%20de%20la%20logica%20silogistica.pdf.jpg510f7843e9b02ffc0eb5d0c932223990MD52open access20.500.12749/8996oai:repository.unab.edu.co:20.500.12749/89962023-01-10 09:19:44.037open accessRepositorio Institucional | Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Publicaciones similares