Now to the actual definition of Horn clause. First, some standard logical terminology. A term is simply an expression built out of variables and function symbols. For example, x y-1 z is a term in the language of groups. An atomic formula is a formula that consists of relation symbols (including equality) applied to terms. So xy = yx is an example of an atomic formula in the language of groups. What makes an atomic formula atomic is that it’s not built out of smaller logical formulas.
A Horn clause is built out of atomic formulas in a particular way. Let A_1, … A_n and B
be atomic formulas. Then a Horn clause is a logical formula of the form
A_1 and … and A_n implies B.
As a degenerate special case, the left-hand side of the implication can be empty, which is the same as asserting formula B holds unconditionally.
http://rjlipton.wordpress.com/2010/01/05/an-approach-to-pnp-via-descriptive-complexity/
An approach to P not equal to NP based on descriptive complexity and HORNSAT
Alfred Horn was a logician who in 1951 discovered the important notion that we now call Horn clauses, in his honor. This class of special clauses has played a foundational role in the area of logic programming—for example, are a key part of the programming language Prolog. I used a picture of one of Horn’s PhD students, Dr. Ali Amir-Moez, who created the Horn-Moez Prize. I was unable to find a picture of Horn—even after a very long search—so I hope that this is okay.
Today I want to talk about an old idea, based on Horn clauses, that may be relevant to the P=NP question.
Years ago David Dobkin, Steven Reiss and I worked on a problem that used Horn Clauses. We proved that Linear Programming (LP) is complete for P with respect to logspace reductions—our proof used, in today’s terminology, an LP relaxation of Horn clauses. At the end of our paper we said:
This theorem is especially interesting since it is not known whether linear programming belongs to P or no? (see [3] for more details on this problem).
The reference “[3]” was to a paper of Dobkin and Reiss that was in preparation; they had found many interesting problems that were equivalent to LP—all in a hope to better understand the problem. I think that they, and others, probably had guessed at the time that LP might be NP-complete, but I am not sure anymore what the conventional wisdom was at that time. Of course it still could be NP-complete, but that would imply that P is equal to NP.
Let’s turn to talking about Horn clauses and the P=NP problem. By the way this whole discussion is joint work with Ken Regan.emanating growth
Is there (except the usual P vs. NP and stuff) any mathematical motivation for horn clauses? They are used in Prolog and some Databases, but from a mathematical point of view, well, they may be a special case of inductive definitons or geometrical formulas, but is there any explicit motivation for them?
I’ll try to answer that question in greater length as I go, but quickly I see two motivations for the concept. One is that deduction with Horn clauses means you never have to split up into cases. If you’re working with a logical statement like “C implies A or B”, then at some point you may have to consider case A and case B separately. Too many cases like that and you get an exponential explosion. With Horn clauses, once the satisfy the premises of the clause, you draw a definite conclusion.
Another is that subjects given by Horn clauses can be given a strong algebraic flavor. You can define “free” objects (like free groups). If you only allow equality (so no other relation symbols), quotients are defined by congruences like in universal algebra. From the category point of view, the class of objects that obey the axioms form a complete and cocomplete category, etc. Basically the part of algebra that is not specific to any subject — the things that groups, rings, etc. have in common — comes from the general Horn clause nature of the axioms we usually consider.