Composition Theorem for Generalized Sum

• Autorzy: Rabinovich A.
• Języki publikacji: EN

Abstrakty

EN

Composition theorems are tools which reduce sentences about some compound structure to sentences about its parts. A seminal example of such a theorem is the Feferman-Vaught Theorem [3] which reduces the first-order theory of generalized products to the first order theory of its factors and the monadic second-order theory of index structure. Shelah [23] used the composition theorem for linear orders as one of the main tools for obtaining very strong decidability results for the monadic second-order theory of linear orders. The main technical contribution of our paper is (1) a definition of a generalized sum of structures and (2) a composition theorem for first-order logic over the generalized sum. One of our objectives is to emphasize the work-out of the composition method.

Słowa kluczowe

EN

composition theorem; first-order logic; expressibility; decidability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 1-2
• Strony: 137--167
• Opis fizyczny: bibliogr. 27 poz.

Twórcy

autor

Rabinovich A.

• School of Computer Science, Sackler Faculty of Exact Sciences, Tel Aviv University, Tel Aviv, Israel 69978,

Bibliografia

• [1] V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995
• [2] H.-D. Ebbinghaus and J. Flum (1995). Finite Model Theory. Springer Perspectives in Mathematical Logic.
• [3] S. Feferman and R.L. Vaught (1959). The first-order properties of products of algebraic systems. Fundamenta Mathematica 47:57-103.
• [4] D. Gabbay, I. Hodkinson and M. Reynolds (1994). Temporal Logic. Oxford University Press.
• [5] Y. Gurevich (1979).Modest theory of short chains I. Journal of Symbolic Logic 44:481-490.
• [6] Y. Gurevich (1985).Monadic second-order theories. InModel-Theoretic Logics, (J. Barwise and S. Feferman, eds.), 479-506, Springer-Verlag.
• [7] Y. Gurevich and A. Rabinovich. Definability and Undefinability with Real Order at the Background, J. Symb. Log. 65(2): 946-958 (2000).
• [8] Y. Gurevich and S. Shelah (1979).Modest theory of short chains II. Journal of Symbolic Logic 44:491-502.
• [9] Y. Gurevich and S. Shelah (1979). Rabin's uniformization problem. Journal of Symbolic Logic 48:1105-1119.
• [10] Y. Gurevich and S. Shelah (1985). The decision problem for branching time logic. Journal of Symbolic Logic 50(3):668-681.
• [11] Y. Gurevich and S. Shelah. On the strength of the interpretation method. The Journal of Symbolic Logic, 54:305-323, 1989.
• [12] T. Hafer and W. Thomas (1987). Computation tree logic CTL_ and path quantifiers in the monadic theory of the binary tree. In Proceedings of ICALP'87: International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 267:269-279, Springer-Verlag.
• [13] N. Immerman (1998).Descriptive Complexity, Springer Verlag, 1998.
• [14] H. Laüchli (1968). A decision procedure for the weak second-order theory of linear order. In "Contributions to Mathematical Logic", eds. H. A. Schmidt et al., North Holland, 1968, 189-197.
• [15] S. Lifsches and S. Shelah. Peano Arithmetic may not be interpretable in the monadic theory of orders. J Symbolic Logic 62 (1997) 848-872.
• [16] S. Lifsches and S. Shelah. Uniformization, choice functions and well orders in the class of trees. Journal of Symbolic Logic, 61:1206-1227, 1996.
• [17] S. Lifsches and S. Shelah. Uniformization and Skolem Functions in the Class of Trees. Journal of Symbolic Logic, 63:103-127, 1998.
• [18] J. Makowsky. Translations, Interpretations and Reduction. Course given at ESSLLI'97, August 12-22, 1997
• [19] MAKOWSKY, J. A. 2004. Algorithmic aspects of the Feferman-Vaught theorem. Annals of Pure and Applied Logic 126(1-3), 159-213.
• [20] F. Moller and A. Rabinovich. On the expressive power of CTL*. LICS 1999, 360-369.
• [21] A. Rabinovich. Composition Theorems for Recursively Defined Structures. Technical Report, Tel Aviv University, 1999.
• [22] A. Rabinovich. Composition Theorems for Generalized Sum and Recursively Defined Types. Electr. Notes Theor. Comput. Sci. 123: 209-211 (2005).
• [23] S. Shelah (1975). The monadic theory of order. Annals of Mathematics 102:379-419.
• [24] S. Shelah (1996). On the very weak 0 - 1 law for random graphs with orders. Journal of Logic and Computation 6:137-159.
• [25] W. Thomas. Classifying regular events in symbolic logic. J. Computer and System Sciences, 25, pp. 360-376, 1982.
• [26] W. Thomas (1997). Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, Lecture Notes in Computer Science 1261:118-143, Springer-Verlag.
• [27] S. Zeitman. "The Composition Method", PhD thesis, Wayne State Univ., Detroit, Michigan 1994.