PROPOSITIONAL LOGIC AND HORN CLAUSES

PROPOSITIONAL LOGIC
AND
HORN CLAUSE

First-order logic—also known as first-order predicate calculus and predicate logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science.

In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. A Horn clause is composed of at least one native negative clauses and at only one affirmative clause, all bound by disjunctive operators. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.

Likewise, Horn clauses play a fundamental role in both constructive logic and computational logic. Indeed, they are important in automated theorem proving by first-order resolution, because the resolvent of two Horn clauses is itself a Horn clause, and the resolvent of a goal clause and a definite clause is a goal clause. These properties of Horn clauses can lead to greater efficiencies in proving a theorem (represented as the negation of a goal clause).

Besides, naturally, propositional Horn clauses are also of great interest in general computability and computational complexity. The problem of finding truth value assignments to make a conjunction of propositional Horn clauses true is a simple P‑complete problem, solvable in linear time, and sometimes called HORNSAT. (Nevertheless, the unrestricted Boolean satisfiability problem is an NP-complete problem.) Of great concern is the fact that satisfiability of first-order Horn clauses is undecidable.  Furthermore, Horn clauses are also the basis of logic programming, where it is common to write definite clauses in the form of an implication, thus, a Horn Normal Form (HNF) can be easily transformed into Conjunctive Normal Form (CNF). The representation and subsequent solution of the problem is a substitution of terms for the variables in the goal clause, which can be extracted from the proof of contradiction. Used in this way, goal clauses are similar to conjunctive queries in relational databases, and, likewise, a Horn clause logic is equivalent in computational power to a universal Turing machine.  Again, solving the problem amounts to deriving a contradiction, which is represented by the empty clause (or "false"), as in the logic programming language Prolog.

Indeed, the Prolog notation can actually be ambiguous, and the term “goal clause” is likewise sometimes also used ambiguously. The variables in a goal clause can be read as universally or existentially quantified, and deriving “false” can be strategically interpreted either as deriving a contradiction or as deriving a successful solution of the problem to be solved.

In this lecture, I further introduce Propositional Logic and Horn Clause and presented a fundamental conceptual framework. To download these slides in Adobe pdf format, click here