Church Synthesis Problem with Parameters

For a two-variable formula (X, Y ) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of an operator Y = F(X) such that (X, F(X)) is universally valid over Nat. B

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Alexander Moshe Rabinovich
• Keywords: Automated Reasoning, Church Synthesis Problem, CSL 2006, Monadic Logic, Parameterized Version