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.
Abstract
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
Germany
frank@sfs.nphil.uni-tuebingen.de