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. © Springer-Verlag Berlin Heidelberg 2009.
CITATION STYLE
Gheerbrant, A., & Ten Cate, B. (2009). Complete axiomatizations of MSO, FO(TC 1) and FO(LFP 1) on finite trees. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5407 LNCS, pp. 180–196). https://doi.org/10.1007/978-3-540-92687-0_13
Mendeley helps you to discover research relevant for your work.