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

Vista sencilla de ítem
dc.contributor.authorRocha, Camilospa
dc.contributor.authorMeseguer, Joséspa
dc.contributor.googlescholarRocha, Camilo [s5LVBc8AAAAJ]spa
dc.contributor.googlescholarMeseguer, José [KZFo7ZkAAAAJ]spa
dc.contributor.orcidRocha, Camilo [0000-0003-4356-7704]spa
dc.contributor.orcidMeseguer, José [0000-0003-4779-3848]spa
dc.date.accessioned2020-10-27T00:20:58Z
dc.date.available2020-10-27T00:20:58Z
dc.date.issued2007-12-01
dc.description.abstractPresentamos 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.spa
dc.description.abstractenglishWe 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.eng
dc.format.mimetypeapplication/pdfspa
dc.identifier.instnameinstname:Universidad Autónoma de Bucaramanga UNABspa
dc.identifier.issn2539-2115
dc.identifier.issn1657-2831
dc.identifier.repourlrepourl:https://repository.unab.edu.co
dc.identifier.urihttp://hdl.handle.net/20.500.12749/8996
dc.language.isospaspa
dc.publisherUniversidad Autónoma de Bucaramanga UNAB
dc.relationhttps://revistas.unab.edu.co/index.php/rcc/article/view/1038/1011
dc.relation.referencesLeo Bachmair and Nachum Dershowitz. Inference rules for rewrite-based first-order theorem proving. In LICS, pages 331 {337. IEEE Computer Society, 1987.
dc.relation.referencesD. Basin, M. Clavel, and J. Meseguer. Rewriting logic as a metalogical framework. ACM Transactions on Computational Logic, 5:528 (576, 2004.
dc.relation.referencesGeorge S. Boolos, John P. Burgas, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, 4th edition, 2002.
dc.relation.referencesMel Bouhoula, Jean-Pierre Jouannaud, and Jose Meseguer. Specification and proof in membership equational logic. Theor. Comput. Sci.,236( I -2):35 (132,2000.
dc.relation.referencesM. 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.
dc.relation.referencesManuel 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.
dc.relation.referencesManuel 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.
dc.relation.referencesJohn Corcoran. Completeness of an ancient logic. J. Symb. Log., 37(4):696 (702, 1972.
dc.relation.referencesEdsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, 1990.
dc.relation.urihttps://revistas.unab.edu.co/index.php/rcc/article/view/1038
dc.rightsDerechos de autor 2007 Revista Colombiana de Computación
dc.rights.accessrightsinfo:eu-repo/semantics/openAccessspa
dc.rights.creativecommonsAttribution-NonCommercial-ShareAlike 4.0 International*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/4.0/*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.sourceRevista Colombiana de Computación; Vol. 8 Núm. 2 (2007): Revista Colombiana de Computación; 101-130
dc.subjectInnovaciones tecnológicas
dc.subjectCiencia de los computadores
dc.subjectDesarrollo de tecnología
dc.subjectIngeniería de sistemas
dc.subjectInvestigaciones
dc.subjectTecnologías de la información y las comunicaciones
dc.subjectTIC´s
dc.subject.keywordsTechnological innovationseng
dc.subject.keywordsComputer scienceeng
dc.subject.keywordsTechnology developmenteng
dc.subject.keywordsSystems engineeringeng
dc.subject.keywordsInvestigationseng
dc.subject.keywordsInformation and communication technologieseng
dc.subject.keywordsICT'seng
dc.subject.keywordsSyllogistic logic with complementseng
dc.subject.keywordsDecision procedureeng
dc.subject.keywordsEquational logiceng
dc.subject.keywordsRewriting logiceng
dc.subject.keywordsMaudeeng
dc.subject.lembInnovaciones tecnológicasspa
dc.subject.lembCiencias de la computaciónspa
dc.subject.lembDesarrollo tecnológicospa
dc.subject.lembIngeniería de sistemasspa
dc.subject.lembInvestigacionesspa
dc.subject.lembTecnologías de la información y la comunicaciónspa
dc.subject.proposalLógica silogística con complementosspa
dc.subject.proposalProcedimiento de decisiónspa
dc.subject.proposalLógica ecuacionalspa
dc.subject.proposalReescritura de lógicaspa
dc.titleUn procedimiento de decisión de reescritura de la lógica silogística de Dijkstra-Scholten con complementosspa
dc.title.translatedA rewriting decision procedure for Dijkstra-Scholten's syllogistic logic with complementseng
dc.type.coarhttp://purl.org/coar/resource_type/c_7a1f
dc.type.driverinfo:eu-repo/semantics/article
dc.type.hasversioninfo:eu-repo/semantics/acceptedVersion
dc.type.localArtículospa
dc.type.redcolhttp://purl.org/redcol/resource_type/CJournalArticle

Archivos

Bloque original

Mostrando 1 - 1 de 1
Miniatura
Nombre:
2007_Articulo_Un procedimiento de decisión de reescritura de la logica silogistica.pdf
Tamaño:
16.63 MB
Formato:
Adobe Portable Document Format
Descripción:
Artículo
Descargar

Colecciones

Revista Colombiana de Computación