Monadic Second Order Logic, Tree Automata and Constraint Logic Programming

Frank Morawietz

Monadic Second Order Logic, Tree Automata and Constraint Logic Programming

Draft, 44pp. DVI (158kb); Postscript (390kb)1-up; Postscript gzip-komprimiert (143kb) 1-up , 2-up.

Abstract

In this paper we present a first step toward the development of a constraint logic programming (CLP) language R(MSO) based on monadic second order (MSO) logic. We apply the scheme proposed by Höhfeld und Smolka (1988) to obtain a relational extension of MSO logic with a corresponding sound and complete operational semantics. The solutions to constraints expressed in monadic second order logic are represented by tree automata recognizing the assignment trees satisfying the formulas. Since this allows a compact and efficient representation of constraints, we can use MSO theorem provers as constraint solvers for the CLP interpreter. Building on the detailed investigation of MSO logic in Rogers (1994) as a tree description language in the Principles and Parameter (P&P) paradigm, we present as motivation and applications details from the realm of P&P-based parsing.

To appear in The Mathematics of Syntactic Structure by H.-P. Kolb and U. Mönnich, 199x.

In case of problems or for comments, please contact: frank@sfs.uni-tuebingen.de
Last updated: 13-Mar-2000