The MSO logic–automaton connection in linguistics

Abstract

In this paper we discuss possible applications of a system which uses automata-based theorem-proving techniques drawing on the decidabi lity proof for weak monadic second-order (MSO) logic on trees to implement linguistic processing and theory verificati on. Despite a staggering complexity bound, the success of and the continuing work on these techniques in computer science promises a usable tool to test formaliz ations of grammars. The advantages are readily apparent. The direct use of a succinct and flexible description language together with an environment to test the formaliz ations with the resulting finite, deterministic tree automata offers a way of combining the needs of both formaliz ation 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 Principl es-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.