Frank Morawietz:

    Compiling MSO Logic into Tree Automata

    Abstract

    In this talk I will present possible applications of a system which uses automata-based theorem-proving techniques drawing on the decidability proof for weak monadic second-order (MSO) logic on trees to implement linguistic processing and theory verification. Despite a staggering complexity bound, the success of and the continuing work on these techniques in computer science promises a usable tool to test formalizations of grammars. The advantages are readily apparent. The direct use of a succinct and flexible description language together with an environment to test the formalizations with the resulting finite, deterministic tree automata offers a way of combining the needs of both formalization and processing. The talk will address three issues. Firstly I will show how to use this technique for the verification of separate modules of a Principles-and-Parameters (P&P) grammar and secondly for the approximation of an entire P&P theory. And thirdly, if time permits, I will extend the language of the MSO tree logic with inductive relations to overcome some of the remaining engineering problems.