Complete calculi for structured specifications in fork algebra

In previous articles we presented Arg entum, a tool for reasoning across heterogeneous specifications based on the language of fork algebras. Arg entum's foundations were formalized in the framework of institutions. The formalization made simple to describe a methodology capable of producing a...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Lopez Pombo, C.G
Otros Autores: Frias, M.F
Formato: Acta de conferencia Capítulo de libro
Lenguaje:Inglés
Publicado: 2010
Materias:
Acceso en línea:Registro en Scopus
DOI
Handle
Registro en la Biblioteca Digital
Aporte de:Registro referencial: Solicitar el recurso aquí
LEADER 07105caa a22007097a 4500
001 PAPER-7517
003 AR-BaUEN
005 20230518203716.0
008 190411s2010 xx ||||fo|||| 00| 0 eng|d
024 7 |2 scopus  |a 2-s2.0-78049447249 
040 |a Scopus  |b spa  |c AR-BaUEN  |d AR-BaUEN 
100 1 |a Lopez Pombo, C.G. 
245 1 0 |a Complete calculi for structured specifications in fork algebra 
260 |c 2010 
270 1 0 |m Lopez Pombo, C. G.; Department of Computer Science, Facultad de Ciencias Exactas Y Naturales, Universidad de Buenos AiresArgentina; email: clpombo@dc.uba.ar 
506 |2 openaire  |e Política editorial 
504 |a Booch, G., Rumbaugh, J., Jacobson, I., (1998) The Unified Modeling Language User Guide, , Addison-Wesley Longman Publishing Co., Inc., Boston 
504 |a Frias, M.F., Fork algebras in algebra, logic and computer science (2002) Advances in Logic, 2. , World Scientific Publishing Co., Singapore 
504 |a Frias, M.F., Baum, G.A., Maibaum, T.S.E., Interpretability of first-order dynamic logic in a relational calculus (2002) LNCS, 2561, pp. 66-80. , de Swart, H. (ed.) RelMiCS 2001. Springer, Heidelberg 
504 |a Frias, M.F., Lopez Pombo, C.G., Time is on my side (2003) Procs. of RelMiCS 7, pp. 105-111 
504 |a Frias, M.F., Lopez Pombo, C.G., Interpretability of first-order linear temporal logics in fork algebras (2006) JLAP, 66 (2), pp. 161-184 
504 |a Goguen, J.A., Burstall, R.M., Introducing institutions (1985) LNCS, 184, pp. 221-256. , Hutchison, D., Shepherd, W.D., Mariani, J.A. (eds.) Local Area Networks: An Advanced Course Springer, Heidelberg 
504 |a Meseguer, J., General logics (1989) Procs. of the Logic Colloquium 1987, 129, pp. 275-329. , North Holland, Amsterdam 
504 |a Tarlecki, A., Moving between logical systems (1996) LNCS, 1130, pp. 478-502. , Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. Springer, Heidelberg 
504 |a Lopez Pombo, C.G., Frias, M.F., Fork algebras as a sufficiently rich universal institution (2006) LNCS, 4019, pp. 235-247. , Johnson, M., Vene, V. (eds.) AMAST 2006 Springer, Heidelberg 
504 |a Borzyszkowski, T., Logical systems for structured specifications (2002) TCS, 286, pp. 197-245 
504 |a Tarski, A., On the calculus of relations (1941) JSL, 6 (3), pp. 73-89 
504 |a Maddux, R.D., Finitary algebraic logic (1989) Zeitschrift fur Mathematisch Logik und Grundlagen der Mathematik, 35, pp. 321-332 
504 |a Burris, S., Sankappanavar, H.P., A course in universal algebra (1981) Graduate Texts in Mathematics, , Springer, Berlin 
504 |a Sannella, D., Tarlecki, A., Specifications in an arbitrary institution (1988) Information and Computation, 76 (2-3), pp. 165-210 
504 |a Tarlecki, A., Abstract specification theory: An overview (2003) Procs. of the NATO Advanced Study Institute on Models, Algebras and Logic of Engineering Software, pp. 43-79. , NATO Science Series, IOS Press, Marktoberdorf 
504 |a Diaconescu, R., Institution-independent Model Theory, Studies in Universal Logic, 2. , Birkhäuser, Basel 
504 |a Mossakowski, T., Maeder, C., Luttich, K., The heterogeneous tool set, Hets (2007) LNCS, 4424, pp. 519-522. , Grumberg, O., Huth, M. (eds.) TACAS 2007 Springer, Heidelberg 
504 |a Tarlecki, A., Towards heterogeneous specifications (2000) Frontiers of Combining Systems. Studies in Logic and Computation, 2, pp. 337-360. , Gabbay, D., de Rijke, M. (eds.) Research Studies Press 
504 |a Cengarle, M.V., Knapp, A., Tarlecki, A., Wirsing, M., A heterogeneous approach to UML semantics (2008) LNCS, 5065, pp. 383-402. , Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models Springer, Heidelberg 
504 |a Roşu, G., Goguen, J.A., On equational craig interpolation (2000) Journal of Universal Computer Science, 6 (1), pp. 194-200 
504 |a Tarski, A., Givant, S., (1987) A Formalization of Set Theory Without Variables, , American Mathematical Society Colloqium Publications, Providence 
504 |a Lopez Pombo, C.G., (2007) Fork Algebras As a Tool for Reasoning Across Heterogeneous Specifications, , PhD thesis, Universidad de Buenos Aires 
520 3 |a In previous articles we presented Arg entum, a tool for reasoning across heterogeneous specifications based on the language of fork algebras. Arg entum's foundations were formalized in the framework of institutions. The formalization made simple to describe a methodology capable of producing a complete system desription from partial views, eventually written in different logical languages. Structured specifications were introduced by Sannella and Tarlecki and extensively studied by Borzyszkowski. The latter also presented conditions under which the calculus for structured specifications is complete. Using fork algebras as a "universal" institution capable of representing expressive logics (such as dynamic and temporal logics), requires using a fork language that includes a reflexive-transitive closure operator. The calculus thus obtained does not meet the conditions required by Borzyszkowski. In this article we present structure building operators (SBOs) over fork algebras, and provide a complete calculus for these operators. © 2010 Springer-Verlag.  |l eng 
593 |a Department of Computer Science, Facultad de Ciencias Exactas Y Naturales, Universidad de Buenos Aires, Argentina 
593 |a Department of Computer Engineering, Buenos Aires Institute of Technology (ITBA), Argentina 
593 |a CONICET, Argentina 
690 1 0 |a COMPLETE SYSTEM 
690 1 0 |a LOGICAL LANGUAGE 
690 1 0 |a PARTIAL VIEWS 
690 1 0 |a STRUCTURED SPECIFICATION 
690 1 0 |a TRANSITIVE CLOSURE 
690 1 0 |a BIOMINERALIZATION 
690 1 0 |a CALCULATIONS 
690 1 0 |a SPECIFICATIONS 
650 1 7 |2 spines  |a ALGEBRA 
700 1 |a Frias, M.F. 
711 2 |c Natal  |d 1 September 2010 through 3 September 2010  |g Código de la conferencia: 82192 
773 0 |d 2010  |g v. 6255 LNCS  |h pp. 290-305  |p Lect. Notes Comput. Sci.  |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)  |x 03029743  |w (AR-BaUEN)CENRE-983  |z 3642148077  |z 9783642148071  |t 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010 
856 4 1 |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-78049447249&doi=10.1007%2f978-3-642-14808-8_20&partnerID=40&md5=7c204899f6bf0bc94c89b8a147ae9732  |y Registro en Scopus 
856 4 0 |u https://doi.org/10.1007/978-3-642-14808-8_20  |y DOI 
856 4 0 |u https://hdl.handle.net/20.500.12110/paper_03029743_v6255LNCS_n_p290_LopezPombo  |y Handle 
856 4 0 |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6255LNCS_n_p290_LopezPombo  |y Registro en la Biblioteca Digital 
961 |a paper_03029743_v6255LNCS_n_p290_LopezPombo  |b paper  |c PE 
962 |a info:eu-repo/semantics/article  |a info:ar-repo/semantics/artículo  |b info:eu-repo/semantics/publishedVersion 
963 |a VARI 
999 |c 68470