Gheerbrant, Amélie and Cate, Balder ten - Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees

lmcs:1017 - Logical Methods in Computer Science, October 23, 2012, Volume 8, Issue 4
Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees

Authors: Gheerbrant, Amélie and Cate, Balder ten

We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.


Source : oai:arXiv.org:1210.2620
DOI : 10.2168/LMCS-8(4:12)2012
Volume: Volume 8, Issue 4
Published on: October 23, 2012
Submitted on: April 6, 2011
Keywords: Computer Science - Logic in Computer Science,E.1,F.4.1,F.4.3


Share

Consultation statistics

This page has been seen 75 times.
This article's PDF has been downloaded 17 times.