What is a Horn clause?
Q: What is a Horn clause?
A: A Horn clause is a logic disjunction of literals, where at most one of the literals is positive and all the others are negative.
Q: Who first described them?
A: Alfred Horn first described them in an article in 1951.
Q: What is a definite clause?
A: A Horn clause with exactly one positive literal is called a definite clause.
Q: What is a fact?
A: A definite clause with no negative literals is sometimes referred to as a "fact".
Q: What is a goal clause?
A: A Horn clause without a positive literal is sometimes called a goal clause.
Q: How do variables in non-propositional cases work?
A: In the non-propositional case, all variables in a clause are implicitly universally quantified with scope the entire clause. This means that they apply to every part of the statement.
Q: What role do Horn clauses play in constructive logic and computational logic? A: Horn clauses play an important role in automated theorem proving by first-order resolution because the resolvent of two Horn clauses or between one goal and one definite clausse can be used to create greater efficiencies when proving something represented as the negation of its goal clausse. They are also used as basis for logic programming languages such as Prolog, where they behave like goal reduction procedures.
