\input zb-basic
\input zb-ioport
\iteman{io-port 01771757}
\itemau{Talbot, Jean-Marc}
\itemti{The $\exists\forall^2$ fragment of the first-order theory of atomic set constraints is $\Pi_1^0$-hard.}
\itemso{Inf. Process. Lett. 74, No.1-2, 27-33 (2000).}
\itemab
Summary: Set constraints are logical formulas involving inclusions between expressions denoting sets of trees. For atomic set constraints, set expressions do not contain any set operators. In this article we show that valid formulas of the $\exists\forall^2$ fragment of the first-order theory of atomic set constraints is $\Pi^0_1$-hard, i.e., co-recursively enumerable hard. This is proved by the encoding of a 2-register machine with a recursively enumerable-complete domain into the dual $\forall\exists^2$2 fragment. This improves a result from Charatonik (1998).
\itemrv{~}
\itemcc{D.1.6}
\itemut{set constraints}
\itemli{doi:10.1016/S0020-0190(00)00030-2}
\end