×

Complete axiomatizations of MSO, FO(TC\(^{1} )\) and FO(LFP\(^{1} )\) on finite trees. (English) Zbl 1211.03049

Artemov, Sergei (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3–6, 2009. Proceedings. Berlin: Springer (ISBN 978-3-540-92686-3/pbk). Lecture Notes in Computer Science 5407, 180-196 (2009).
Summary: We propose axiomatizations of monadic second-order logic (MSO), monadic transitive closure logic (FO(TC\(^{1} ))\) and monadic least fixpoint logic (FO(LFP\(^{1} ))\) on finite node-labeled sibling-ordered trees. We show by a uniform argument, that our axiomatizations are complete, i.e., in each of our logics, every formula which is valid on the class of finite trees is provable using our axioms. We are interested in this class of structures because it allows to represent basic structures of computer science such as XML documents, linguistic parse trees and treebanks. The logics we consider are rich enough to express interesting properties such as reachability. On arbitrary structures, they are well known to be not recursively axiomatizable.
For the entire collection see [Zbl 1156.03004].

MSC:

03B70 Logic in computer science
03C07 Basic properties of first-order languages and structures
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Backofen, R., Rogers, J., Vijay-Shankar, K.: A first-order axiomatization of the theory of finite trees. Journal of Logic, Language and Information 4(4), 5–39 (1995) · Zbl 0833.03010 · doi:10.1007/BF01048403
[2] Bosse, U.: An Ehrenfeucht-Fraïssé game for fixpoint logic and stratified fixpoint logic. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 100–114. Springer, Heidelberg (1993) · Zbl 0808.03024 · doi:10.1007/3-540-56992-8_8
[3] Calo, A., Makowsky, J.A.: The Ehrenfeucht-Fraïssé games for transitive closure. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol. 620, pp. 57–68. Springer, Heidelberg (1992) · Zbl 0978.03525 · doi:10.1007/BFb0023863
[4] Doets, K.: Completeness and Definability: Applications of the Ehrenfeucht Game in Second-Order and Intensional Logic. PhD thesis, Universiteit van Amsterdam (1987)
[5] Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Perspectives in Mathematical Logic. Springer, Berlin (1995)
[6] Enderton, H.: A mathematical introduction to Logic. Academic Press, New York (1972) · Zbl 0298.02002
[7] Feferman, S., Vaught, R.: The first-order properties of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959) · Zbl 0088.24803
[8] Gottlob, G., Koch, C.: Monadic datalog and the expressive power of languages for web information extraction. In: Proceedings of PODS 2002, pp. 17–28 (2002) · Zbl 1316.68045 · doi:10.1145/543613.543617
[9] Grädel, E.: On transitive closure logic. In: Kleine Büning, H., Jäger, G., Börger, E., Richter, M.M. (eds.) CSL 1991. LNCS, vol. 626, pp. 149–163. Springer, Heidelberg (1992) · Zbl 0783.03012 · doi:10.1007/BFb0023764
[10] Henkin, L.: Completeness in the theory of types. The Journal of Symbolic Logic 15(2), 81–91 (1950) · Zbl 0039.00801 · doi:10.2307/2266967
[11] Kepser, S.: Querying linguistic treebanks with monadic second-order logic in linear time. J. of Logic, Lang. and Inf. 13(4), 457–470 (2004) · Zbl 1067.68154 · doi:10.1007/s10849-004-2116-8
[12] Kepser, S.: Properties of binary transitive closure logic over trees. In: Satta, G., Monachesi, P., Penn, G., Wintner, S. (eds.) Formal Grammar 2006, pp. 77–89 (2006)
[13] Lafitte, G., Mazoyer, J.: Théorie des modèles et complexité. Technical report, Ecole Normale Supérieure de Lyon (1998)
[14] Makowsky, J.A.: Algorithmic uses of the Feferman-Vaught theorem. Annals of Pure and Applied Logic 126(1-3), 159–213 (2004) · Zbl 1099.03009 · doi:10.1016/j.apal.2003.11.002
[15] Manzano, M.: Extensions of First-Order logic. Cambridge University Press, New York (1996) · Zbl 0848.03001
[16] Matz, O., Schweikardt, N.: Expressive power of monadic logics on words, trees, pictures, and graphs. In: Grädel, E., Flum, J., Wilke, T. (eds.) Logic and Automata: History and Perspectives, Texts in Logic and Games, pp. 531–552. Amsterdam University Press (2007) · Zbl 1244.03118
[17] Rogers, J.: Descriptive Approach to Language - Theoretic Complexity. CSLI Publications, Stanford (1998) · Zbl 0956.03030
[18] ten Cate, B., Marx, M.: Axiomatizing the logical core of XPath 2.0. In: Schwentick, T., Suciu, D. (eds.) ICDT 2007. LNCS, vol. 4353, pp. 134–148. Springer, Heidelberg (2006) · Zbl 1192.68224 · doi:10.1007/11965893_10
[19] ten Cate, B., Segoufin, L.: XPath, transitive closure logic, and nested tree walking automata. In: PODS 2008: Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pp. 251–260. ACM, New York (2008) · Zbl 1327.03024 · doi:10.1145/1376916.1376952
[20] Tiede, H.-J., Kepser, S.: Monadic second-order logic and transitive closure logics over trees. Electron. Notes Theor. Comput. Sci. 165, 189–199 (2006) · Zbl 1262.03050 · doi:10.1016/j.entcs.2006.05.044
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.