Generalized Interpolation in First Order Logic

• Autorzy: Borzyszkowski T.
• Języki publikacji: EN

Abstrakty

EN

We consider the Craig Interpolation Property for many sorted first-order logic. The Craig Interpolation Property explored in this paper is inspired by the institution independent generalization of this property presented in [21]. In [3] the author presents the interpolation result for the institution of many sorted first-order logic, with both morphisms in the pushout square being injective on sort names. The author also shows that the Craig Interpolation Property does not hold when both morphisms are certain morphisms which are noninjective on sort names. An open question in that paper was whether the interpolation property holds with only one morphism being injective on sort names. In this paper we give answer to this question. Following the overall structure of the classical proof presented in [7] for single sorted first-order logic, but with new technicalities concerning the many sorted case, we show that many sorted first-order logic has the interpolation property when just one (left or right) morphism is injective on sort names.

Słowa kluczowe

EN

formal languages; formal semantics; specification languages; algebraic specification; interpolation property

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 66, nr 3
• Strony: 199--219
• Opis fizyczny: Bibliogr. 25 poz.

Twórcy

autor

Borzyszkowski T.

• Institute of Mathematics, University of Gdańsk Wit Stwosz 57, 80-952 Gdańsk, Poland,

Bibliografia

• [1] J. Bergstra, J. Heering, and P. Klint. Module algebra. Journal of the Association for Computing Machinery, 37(2):335–372, 1990.
• [2] T. Borzyszkowski. Completeness of the logical system for structured specifications. In F. Parisi Presicce, editor, Recent Trends in Algebraic Development Techniques. 12th InternationalWorkshop WADT’97. Tarquinia, Italy, June 1997. Selected papers, volume 1376 of Lecture Notes in Computer Science, pages 107–121. Springer-Verlag, 1998.
• [3] T. Borzyszkowski. Generalized interpolation in CASL. Information Processing Letters, 76:19–24, 2000.
• [4] T. Borzyszkowski. Logical Systems for Structured Specifications (in Polish). PhD thesis, Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Warsaw, 2000.
• [5] T. Borzyszkowski. Logical systems for structured specifications. Theoretical Computer Science, 286:197–245, 2002.
• [6] M. V. Cengarle. Formal Specifications with Higher Order Parameterization. PhD thesis, Institut f¨ur Informatik, Lidwig Maximilians Universit¨at, M¨unhen, 1994.
• [7] C. C. Chang and H. J. Keisler. Model Theory. North-Holland, Amsterdam, 1973.
• [8] R. Diaconescu. An institution-independent proof of craig interpolation theorem. Studia Logica, 76(3):1–21, 2003.
• [9] M. T. Dimitrakos T. On a generalized modularization theorem. Information Processing Letters, 74(1–2):65–71, 2000.
• [10] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Undergraduate Texts in Mathematics. Springer-Verlag, 1984.
• [11] J. Farrés Casals. Verification in ASL and related specification languages. Technical Report CST-92-92, University of Edinburgh, 1992.
• [12] J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39:95–146, 1992.
• [13] H. J. Keisler. Model Theory for Infinitary Logic, volume 62 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1971.
• [14] G. Kreisel and J. L. Krivine. Elements of mathematical logic (Model theory). North-Holland, 1967.
• [15] K. Lambert. Philosophical applications of free logic. Oxford University Press, 1991.
• [16] S. MacLane. Categories for the Working Mathematician, volume 5 of Springer Graduate Texts in Mathematics. Springer-Verlag, 1971.
• [17] T. Mossakowski. Foundations of heterogeneous specification. In H. D. Wirsing M., Pattinson D., editor, Recent Trends in Algebraic Development Techniques, 16th International Workshop, Frauenchiemsee, Germany, 2002, Revised Selected Papers, volume 2755 of Lecture Notes in Computer Science, pages 359–375. Springer-Verlag, 2003.
• [18] P. D.Mosses, editor. CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
• [19] D. T. Sannella, S. Sokołowski, and A. Tarlecki. Towards formal development of programs from algebraic specifications: parameterization revisited. Acta Informatica, 29:689–736, 1992.
• [20] D. T. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:164–210, 1988.
• [21] A. Tarlecki. Bits and pieces of the theory of institutions. In Proc. Workshop on Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 334–363. Springer-Verlag, 1986.
• [22] A. Tarlecki. Moving between logical systems. In Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types joint with the 8th general COMPASS workshop. Oslo, Norway, September 1995. Selected papers, volume 1130 of Lecture Notes in Computer Science, pages 461–485. Springer-Verlag, 1996.
• [23] A. Tarlecki. Towards heterogenous specifications. In D. Gabbay and M. van Rijke, editors, Proc. International Workshop Frontiers of Combining Systems FroCoS’98, Amsterdam October 1998, pages 337–360. Research Studies Press, 2000.
• [24] A. Tarski. The semantic conception of truth. Philos. Phenomenological Research, 4:13–47, 1944.
• [25] M. Wirsing. Structured specifications: syntax, semantics and proof calculus. In F. Bauer, H. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, volume 94 of NATO ASI Series F: Computer and Systems Sciences, pages 411–442. Springer-Verlag, 1991.