Abstract
Proof calculi for structured specifications have been developed independently of the underlying logical system (formalised as institution). Typically, completeness of these calculi requires interpolation properties of the underlying logic. We develop a relatively complete calculus for structured heterogeneous specifications that does not need interpolation.
This work has been partially supported by the German Research Foundation (DFG) via the SFB/TR 8 “Spatial Cognition”, project I1-[OntoSpace] (TM) and by the Polish Ministry of Science and Higher Education, grant N206 493138 (AT).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Borzyszkowski, T.: Generalized interpolation in CASL. Information Processing Letters 79, 19–24 (2000)
Borzyszkowski, T.: Logical systems for structured specifications. Theoretical Computer Science 286, 197–245 (2002)
Cengarle, M.V., Knapp, A., Tarlecki, A., Wirsing, M.: A heterogeneous approach to UML semantics. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 383–402. Springer, Heidelberg (2008)
Cerioli, M., Meseguer, J.: I borrow your logic? (transporting logical structures along maps). Theor. Comput. Sci. 173(2), 311–347 (1997)
Codescu, M., Mossakowski, T., Maeder, C.: Checking conservativity with Hets. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 315–321. Springer, Heidelberg (2013)
Mosses, P.D. (ed.): Casl Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004), http://www.cofi.info
Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285, 289–318 (2002)
Diaconescu, R.: Grothendieck institutions. J. Applied Categorical Structures 10, 383–402 (2002)
Diaconescu, R.: Interpolation in Grothendieck Institutions. Theoretical Computer Science 311(1-3), 439–461 (2004)
Diaconescu, R.: Institution-independent Model Theory. Birkhäuser (2008)
Dimitrakos, T., Maibaum, T.: On a generalized modularization theorem. Information Processing Letters 74, 65–71 (2000)
Fine, K.: Failures of the Interpolation Lemma in Quantified Modal Logic. J. of Symbolic Logic 44(2), 201–206 (1979)
Fiadeiro, J., Sernadas, A.: Structuring theories on consequence. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol. 332, pp. 44–72. Springer, Heidelberg (1988)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)
Goguen, J.A., Rosu, G.: Institution morphisms. Formal Aspects of Computing 13(3-5), 274–307 (2002)
Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Annals of Pure and Applied Logic 67, 113–160 (1994)
Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Springer (1998)
Mossakowski, T., Autexier, S., Hutter, D.: Development graphs – proof management for structured specifications. J. of Logic and Algebraic Programming 67(1-2), 114–145 (2006)
Meseguer, J.: General logics. In: Logic Colloquium 1987, pp. 275–329. North Holland (1989)
Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)
Mossakowski, T.: Relating CASL with other specification languages: the institution level. Theoretical Computer Science 286, 367–475 (2002)
Mossakowski, T.: Heterogeneous Specification and the Heterogeneous Tool Set. Habilitation thesis, Universität Bremen (2005)
Mossakowski, T.: Institutional 2-cells and grothendieck institutions. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 124–149. Springer, Heidelberg (2006)
Mossakowski, T., Tarlecki, A.: Heterogeneous logical environments for distributed specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 266–289. Springer, Heidelberg (2009)
Sannella, D., Burstall, R.: Structured theories in LCF. In: Ausiello, G., Protasi, M. (eds.) CAAP 1983. LNCS, vol. 159, pp. 377–391. Springer, Heidelberg (1983)
Shoenfield, J.: Mathematical Logic. Addison-Wesley (1967)
Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation 76, 165–210 (1988)
Sannella, D., Tarlecki, A.: Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica 25, 233–281 (1988)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer (2012)
Sannella, D., Tarlecki, A.: Property-oriented semantics of structured specifications. In: Mathematical Structures in Computer Science (2013)
Tarlecki, A.: Towards heterogeneous specifications. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems 2, Studies in Logic and Computation, pp. 337–360. Research Studies Press (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T., Tarlecki, A. (2014). A Relatively Complete Calculus for Structured Heterogeneous Specifications. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)