2009 | OriginalPaper | Buchkapitel
Decidable Extensions of Church’s Problem
verfasst von : Alexander Rabinovich
Erschienen in: Computer Science Logic
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
For a two-variable formula B(X,Y) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of a finite-state operator Y=F(X) such that B(X,F(X)) is universally valid over Nat.
Büchi and Landweber (1969) proved that the Church synthesis problem is decidable.
We investigate a parameterized version of the Church synthesis problem. In this extended version a formula B and a finite-state operator F might contain as a parameter a unary predicate P.
A large class of predicates P is exhibited such that the Church problem with the parameter P is decidable.
Our proofs use Composition Method and game theoretical techniques.