Complete Axiomatizations of MSO, FO(TC 1 ) and FO(LFP 1 ) on Finite Trees

DOI10.1007/978-3-540-92687-0_13zbMath1211.03049OpenAlexW1771000901MaRDI QIDQ3605529

Amélie Gheerbrant, Balder ten Cate

Publication date: 24 February 2009

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-92687-0_13

zbMATH Keywords

TreesFeferman-Vaught theoremsEhrenfeucht-Fraïssé gamesHenkin semanticsAxiomatizationsFragments of MSO

Mathematics Subject Classification ID

Logic in computer science (03B70) Basic properties of first-order languages and structures (03C07)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithmic uses of the Feferman-Vaught theorem
• Querying linguistic treebanks with monadic second-order logic in linear time
• A first-order axiomatization of the theory of finite trees
• Axiomatizing the logical core of XPath 2.0
• The first order properties of products of algebraic systems
• Transitive closure logic, nested tree walking automata, and XPath
• Monadic Second-Order Logic and Transitive Closure Logics over Trees
• Monadic datalog and the expressive power of languages for Web information extraction
• Completeness in the theory of types

This page was built for publication: Complete Axiomatizations of MSO, FO(TC 1 ) and FO(LFP 1 ) on Finite Trees