Why horn formulas matter in computer science: Initial structures and generic examples

摘要

We introduce the notion of generic examples as a unifying principle for various phenomena in computer science such as initial structures in the area of abstract data types, and Armstrong relations in the area of data bases. Generic examples are also useful in defining the semantics of logic programming, in the formal theory of program testing and in complexity theory. We characterize initial structures in terms of their genericity properties and give a syntactic characterization of first-order theories admitting initial .structures. The latter can be used to explain why Horn formulas have gained such a predominant role in various areas of computer science.