Horn clauses, theory of

First-order Horn clause logic is a fragment of first-order logic (cf. also Mathematical logic; Logical calculus) which has remarkable properties otherwise not shared by first-order logic. It consists of formulas of the form

where and are atomic formulas (and could also be or ). (Strict) propositional Horn clauses are propositional formulas of the form

or, equivalently,

where and are propositional variables or . In the strict case is excluded. A Horn theory is a set of Horn clauses.

First-order clauses of this form were first introduced by J.C.C. McKinsey in 1943 in the context of decision problems. Their name, Horn clauses, alludes to a paper by A. Horn, who in 1951 was the first to point out some of their algebraic properties. Between 1956 and 1970, A.I. Mal'tsev [a1] studied systematically the algebraic properties of model classes of Horn theories and showed that Horn clause logic is the right framework for the study of quasi-varieties in universal algebra (cf. also Quasi-variety; Model theory). Model-theoretic properties of Horn theories which allow arbitrary quantifier prefixes were studied by F. Galvin in 1970. Such Horn formulas are intimately related to logical properties preserved under various forms of generalized products of structures. An in-depth treatment may be found in [a2].

Already in the 1950s, R. Smullyan noted that every recursive enumerable set of natural numbers can be represented by some finite strict Horn clause theory (cf. also Recursive set theory). But this observation only bore fruit much later in the framework of programming languages. [a3] is an elegant introduction to recursion theory based on this approach.

The proof theory of first-order Horn clause logic has particularly simple features in that unification of terms and unit resolution (a simple case of modus ponens) provide a complete and easily implementable proof system. Interpreting Horn clauses with free variables as rules of the form'

<tbody> </tbody> IF AND AND , THEN

and atomic formulas with a sequence of constants as facts, R. Kowalski, building on work of many others, moulded this into a logic for problem solving [a4], which is the basis of the programming language PROLOG and the database query language DATALOG, [a5]. At the same time, Horn clause logic was also advocated as a specification language for abstract data types by J. Goguen and his collaborators, [a6], and M. Vardi and R. Fagin used them for the specification of relational databases, [a7].

In the 1980s, the fifth-generation computer project launched by the Japanese advocated the use of Horn clause logic and the programming language PROLOG as the ultimate language for building expert systems and for formulating and solving problems in artificial intelligence. This enthusiasm for Horn clause logic has been dampened by the absence of spectacular breakthroughs. Nevertheless, Horn clause logic is today widely used in computer science as a well understood tool. In-depth theoretical expositions of Horn clause logic can be found in [a8], [a9].

The satisfiability problem for propositional logic consists in finding, for a set of clauses , a truth assignment for the propositional variables occurring in which makes all the clauses simultaneously true, if such an assignment exists. In general, it is not known whether this problem can be solved in polynomial time (measured in the size of ), in fact the problem is -complete (cf. also ; Algorithm, computational complexity of an), and it is widely believed that in the worst case an exponential amount of time is needed to solve it, cf. [a10]. Propositional Horn clauses have a polynomial-time solvable satisfiability problem. In fact, linear time solutions have been proposed in [a11], [a12].

Second-order Horn logic is defined like its first-order counterpart but allows also quantification over relation variables. It has been used by E. Grädel to give a logical characterization of classes of finite ordered structures which are recognizable in polynomial time. Other characterizations of these model classes in terms of fixed-point logics were given earlier by N. Immerman, V. Sazanov and M. Vardi. Logical characterizations of complexity classes belong to the rapidly expanding subdisciplines of descriptive complexity theory (or finite model theory), cf. [a13], which belongs to complexity theory of theoretical computer science, [a12].

References

[a1]	A.I. Mal'tsev, "The metamathematics of algebraic systems. Collected Papers 1936-1967" , North-Holland (1971)
[a2]	C.C. Chang, H.J. Keisler, "Model theory" , North-Holland (1973)
[a3]	M. Fitting, "Computability theory, semantics and logic programming" , Oxford Univ. Press (1987)
[a4]	R. Kowalski, "Logic for problem solving" , North-Holland (1997)
[a5]	S. Ceri, G. Gottlob, L. Tanca, "Logic programming and databases" , Springer (1990)
[a6]	P. Padawitz, "Computing in Horn clause theories" , Springer (1988)
[a7]	R. Fagin, Ma.Y. Vardi, "The theory of data dependencies: A survey" , Math. of Information Processing , Proc. Symp. Appl. Math. , 34 , Amer. Math. Soc. (1986) pp. 19–71
[a8]	W. Hodges, "Logical features of Horn clauses" , Handbook of Logic in Artificial Intelligence and Logic Programming: Logical Foundations , 1 , Oxford Sci. Publ. (1993)
[a9]	J.A. Makowsky, "Why Horn formulas matter in computer science: initial structures and generic examples" J. Comput. System Sci. , 34 (1987) pp. 266–292
[a10]	C. Papadimitriou, "Computational complexity" , Addison-Wesley (1994)
[a11]	A. Itai, J.A. Makowsky, "Unification as a complexity measure for logic programming" J. Logic Programming , 4 (1987) pp. 105–117
[a12]	W.F. Dowling, J.H. Gallier, "Linear-time algorithms for testing the satisfiability of propositional Horn formulae" J. Logic Programming , 3 (1984) pp. 267–284
[a13]	H.-D. Ebbinghaus, J. Flum, "Finite model theory" , Springer (1995)