- Complete axiomatizations of MSO, FO(TC1) and FO(LFP1) on finite trees
- Lecture Notes in Computer Science
- Pages (from-to)
- Document type
- Faculty of Science (FNWI)
Interfacultary Research Institutes
- Informatics Institute (IVI)
Institute for Logic, Language and Computation (ILLC)
We propose axiomatizations of monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixpoint logic (FO(LFP1)) 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.
- go to publisher's site
- Proceedings title: Logical Foundations of Computer Science: International Symposium, LFCS 2009, Deerfield Beach, FL, USA,
January 3-6, 2009: proceedings
Place of publication: Berlin
Editors: S. Artemov, A. Nerode
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.