The MSO logic-automaton connection in linguistics

In this paper we discuss 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 aim of this paper is threefold. Firstly we 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, we extend the language of the MSO tree logic to overcome remaining engineering problems.