← All problems
Unverified
Investigate normalization by a canonical term rewrite system in the setting of second-order monadic logic
The source page states the original problem together with its recorded qualifications and progress updates as follows.
Consider a confluent and terminating term rewriting system and the mapping from a term to its normal form. When is this mapping a monadic second-order transduction? When does it preserve decidability of the monadic second-order theory of a set of terms?