Frank Morawietz & Tom Cornell

On the recognizability of relations over a tree definable in a monadic second order tree description language

Arbeitspapiere des SFB 340, Bericht Nr. 85 (1997), 58pp.
DVI (251kb); Postscript (581b)1-up; Postscript gzip-komprimiert (154kb) 1-up , 2-up.


In this technical report we describe both the theoretical background and the implementation of the prototype MoSeL, a theorem prover based on the monadic second order tree description language L2K,P (Rogers 1994). We make use of the results by Thatcher and Wright (1968) and Doner (1970) proving that the (weak) monadic theory of two successor functions is decidable. They show that formulas in monadic second order logic on trees are satisfiable if and only if the satisfying variable assignments can be recognized by a tree automaton. In the paper we provide the necessary background on tree automata and their constructions, redo the decidability proof and describe its realization in the Prolog implementation MoSeL.

Seminar für Sprachwissenschaft
Eberhard-Karls-Universität Tübingen
Wilhelmstraße 113
72074 Tübingen