Abstract:
We calculate the complexity of the existence problem for a Horn sentence equivalent to a given one. It is proved that for a signature consisting of one unary function symbol and any finite number of unary predicate symbols, the problem is computable. For a signature with at least two unary function symbols, it is stated that the problem mentioned is an $m$-complete $\Sigma^0_1$-set.