Amélie Gheerbrant ; Balder ten Cate - 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 - https://doi.org/10.2168/LMCS-8(4:12)2012
Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite TreesArticle

Authors: Amélie Gheerbrant ; Balder ten Cate

    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.


    Volume: Volume 8, Issue 4
    Published on: October 23, 2012
    Imported on: April 6, 2011
    Keywords: Computer Science - Logic in Computer Science,E.1,F.4.1,F.4.3
    Funding:
      Source : OpenAIRE Graph
    • Abstract Computational Logic: abstract model theory meets computational logic; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 639.021.508
    • III: Medium: Data Interoperability via Schema Mappings; Funder: National Science Foundation; Code: 0905276
    • Foundations of XML - Safe Processing of Dynamic Data over the Internet; Funder: European Commission; Code: 233599

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1443 times.
    This article's PDF has been downloaded 264 times.