Eine entscheidbare Klasse n-stelliger Horn-Prädikate
Jochen Burghardt · arXiv (Cornell University) · 2014
Similar to a tree grammar, a Horn theory can be used to describe an infinite set of terms. In this paper, we present a class of Horn theories such that the set of definable predicates is closed wrt. conjunction and such that the satisfiability of a predicate is decidable. This extends previous results on Horn clauses with unary predicates.