Mostrar el registro sencillo del ítem

dc.contributor.authorRocha, Camilo
dc.date.accessioned2021-12-01T20:19:13Z
dc.date.available2021-12-01T20:19:13Z
dc.date.issued2015
dc.identifier.isbn9783319231648
dc.identifier.isbn9783319231655
dc.identifier.urihttps://repositorio.escuelaing.edu.co/handle/001/1881
dc.description.abstractThe logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding this logic to the point in which, for some time, it was not considered a logic, as logicians use the word. The main objections arise from the fact that: (i) symbolic manipulations seem to be based on the meaning of the terms involved, and (ii) some notation and the proof style of the logic are different, to some extent, from those found in the traditional use of logic. This paper presents the Dijkstra-Scholten logic as a formal system, and explains its proof-theoretic foundations as a formal system, thus avoiding any confusion regarding term manipulation, notation, and proof style. The formal system is shown to be sound and complete, mainly, by using rewriting and narrowing based decision and semi-decision procedures for, respectively, propositional and first-order logic previously developed by C. Rocha and J. Meseguer.eng
dc.description.abstractSe ha demostrado que la lógica de EW Dijkstra y CS Scholten es útil en las pruebas de corrección de programas y ha atraído a muchos seguidores en la investigación, la enseñanza y la programación. Sin embargo, existe confusión respecto a esta lógica hasta el punto de que, durante algún tiempo, no se consideró una lógica, como los lógicos usan la palabra. Las principales objeciones surgen del hecho de que: (i) las manipulaciones simbólicas parecen estar basadas en el significado de los términos involucrados, y (ii) alguna notación y el estilo de prueba de la lógica son diferentes, hasta cierto punto, de los que se encuentran en el uso tradicional de la lógica. Este artículo presenta la lógica de Dijkstra-Scholten como un sistema formal y explica sus fundamentos teóricos de prueba como un sistema formal, evitando así cualquier confusión con respecto a la manipulación de términos, la notación y el estilo de prueba. El sistema formal se muestra sólido y completo, principalmente, mediante el uso de procedimientos de decisión y semidecisión basados ​​en reescritura y estrechamiento para la lógica proposicional y de primer orden, respectivamente, desarrollados previamente por C. Rocha y J. Meseguer.
dc.format.extent17 páginas.spa
dc.format.mimetypeapplication/pdfspa
dc.language.isoengspa
dc.publisherSpringer.spa
dc.relation.ispartofseriesLecture Notes in Computer Science (LNCS);9200
dc.rights© Springer International Publishing Switzerland 2015eng
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/spa
dc.titleThe Formal System of Dijkstra and Scholteneng
dc.typeCapítulo - Parte de Librospa
dc.type.versioninfo:eu-repo/semantics/publishedVersionspa
oaire.accessrightshttp://purl.org/coar/access_right/c_16ecspa
oaire.versionhttp://purl.org/coar/version/c_970fb48d4fbd8a85spa
dc.contributor.researchgroupInformáticaspa
dc.publisher.placeSpringer, Cham.spa
dc.relation.citationendpage597spa
dc.relation.citationstartpage580spa
dc.relation.indexedN/Aspa
dc.relation.ispartofbookLogic, Rewriting, and Concurrency.eng
dc.relation.referencesBackhouse, R.: Program Construction: Calculating Implementations from Specifications. Wiley, New York (2003)spa
dc.relation.referencesBijlsma, L., Nederpelt, R.: Dijkstra-Scholten predicate calculus: concepts and misconceptions. Acta Informatica 35(12), 1007–1036 (1998)spa
dc.relation.referencesBohórquez, J.: Intuitionistic logic according to Dijkstra’s calculus of equational deduction. Notre Dame J. Formal Log. 49(4), 361–384 (2008)spa
dc.relation.referencesBohórquez, J.: An elementary and unified approach to program correctness. Formal Aspects Comput. 22(5), 611–627 (2010)spa
dc.relation.referencesBruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoret. Comput. Sci. 360(1–3), 386–414 (2006)spa
dc.relation.referencesDijkstra, E.: A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Upper Saddle River (1976)spa
dc.relation.referencesDijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, New York (1990)spa
dc.relation.referencesMeseguer, J., Durán, F.: On the and coherence properties of conditional rewrite theories. J. Log. Algebraic Program. 81(7), 816–850 (2011)spa
dc.relation.referencesGries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, New Yok (1993)spa
dc.relation.referencesGries, D., Schneider, F.B.: Equational propositional logic. Inf. Process. Lett. 53(3), 145–152 (1995)spa
dc.relation.referencesGrundy, J.: Window inference in the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA, pp. 177–189. IEEE Computer Society (1992)spa
dc.relation.referencesHoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)spa
dc.relation.referencesHodel, R.: An Introduction to Mathematical Logic. Dover Books on Mathematics Series. Dover Publications Incorporated, New York (2013)spa
dc.relation.referencesHsiang, J.: Topics in automated theorem proving and program generation. Ph.D. thesis, University of Illinois at Urbana-Champaign, Computer Science Department (1982)spa
dc.relation.referencesLifschitz, V.: On calculational proofs. Annals Pure Appl. Log. 113(1–3), 207–224 (2001)spa
dc.relation.referencesLucas, S., Meseguer, J.: Operational termination of membership equational programs: the order-sorted way. Electron. Notes Theo. Comput. Sci. 238(3), 207–225 (2009)spa
dc.relation.referencesMeseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, Francesco (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)spa
dc.relation.referencesMeseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order Symbolic Comput. 20(1–2), 123–160 (2007)spa
dc.relation.referencesRocha, C., Meseguer, J.: Five isomorphic Boolean theories and four equational decision procedures. Technical report 2007–2818, University of Illinois at Urbana-Champaign (2007)spa
dc.relation.referencesRocha, C., Meseguer, J.: Theorem proving modulo based on Boolean equational procedures. Technical report 2007–2922, University of Illinois at Urbana-Champaign (2007)spa
dc.relation.referencesRocha, C., Meseguer, J.: Theorem proving modulo based on boolean equational procedures. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS/AKA 2008. LNCS, vol. 4988, pp. 337–351. Springer, Heidelberg (2008)spa
dc.relation.referencesSocher-Ambrosius, R., Johann, P.: Deduction Systems (Texts in Computer Science). Springer-Verlag, New York (1996)spa
dc.relation.referencesSimmons, G.: Introduction to Topology and Modern Analysis. International Series in Pure and Applied Mathematics. Krieger Publishing Company, Malabar (1963)spa
dc.relation.referencesTourlakis, G.: On the soundness and completeness of equational predicate logics. J. Log. Comput. 11(4), 623–653 (2001)spa
dc.relation.referencesViry, P.: Equational rules for rewriting logic. Theoret. Comput. Sci. 285, 487–517 (2002)spa
dc.rights.accessrightsinfo:eu-repo/semantics/closedAccessspa
dc.rights.creativecommonsAtribución 4.0 Internacional (CC BY 4.0)spa
dc.subject.armarcSistema Formalspa
dc.subject.armarcRegla de inferenciaspa
dc.subject.armarcLógica proposicionalspa
dc.subject.armarcSímbolo de predicadospa
dc.subject.armarcCuantificación Universalspa
dc.subject.proposalFormal Systemeng
dc.subject.proposalInference Ruleeng
dc.subject.proposalPropositional Logiceng
dc.subject.proposalPredicate Symboleng
dc.subject.proposalUniversal Quantificationeng
dc.type.coarhttp://purl.org/coar/resource_type/c_3248spa
dc.type.contentTextspa
dc.type.driverinfo:eu-repo/semantics/bookPartspa
dc.type.redcolhttp://purl.org/redcol/resource_type/ARTspa


Ficheros en el ítem

Thumbnail

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem

© Springer International Publishing Switzerland 2015
Excepto si se señala otra cosa, la licencia del ítem se describe como © Springer International Publishing Switzerland 2015