Horn clause
In plain wordsA simple, restricted form of logical rule ('if these conditions all hold, then this one conclusion holds') that computers can reason with very efficiently.
A disjunction of literals in which no more than one literal is unnegated — equivalently, an implication whose conditions are all positive atoms and whose conclusion is a single atom or nothing at all. Clauses that have a conclusion, called definite clauses, read as rules ('H if B1 and … and Bn') or, with no conditions, as facts; clauses without one serve as goals or integrity constraints. Satisfiability of propositional Horn formulas is decidable in linear time, unlike general SATBoolean satisfiability problem, n.: The puzzle of deciding whether a set of true-or-false conditions can all be met at once. It is famously hard in theory, yet modern solvers routinely handle millions of conditions., and every set of definite clauses has a unique least model, computable by forward chainingforward chaining, n.: A way of reasoning that starts from known facts and keeps applying rules to them, adding each new conclusion, until it reaches an answer or nothing new can be concluded.. These properties make Horn clauses the basis of logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction.: programs in PrologProlog, prop. n.: A programming language from 1972 in which you state facts and rules in logic and then ask questions; the computer finds answers by searching for proofs. and DatalogDatalog, prop. n.: A small logic language for asking questions of a database with rules, including rules that refer to themselves, such as 'X is an ancestor of Y if X is a parent of an ancestor of Y'. are sets of definite clauses executed by backward chainingbackward chaining, n.: A way of reasoning that starts from the question ('is this true?') and works backward, looking for rules that would prove it and then checking whether their conditions hold. or forward chaining.
Origin
Named after the logician Alfred Horn, who studied sentences of this form in 'On Sentences Which Are True of Direct Unions of Algebras' (Journal of Symbolic Logic, 1951). Their computational importance was recognized in the early 1970s by Robert Kowalski, Maarten van Emden and others developing logic programming.
Related
- logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction.
- PrologProlog, prop. n.: A programming language from 1972 in which you state facts and rules in logic and then ask questions; the computer finds answers by searching for proofs.
- DatalogDatalog, prop. n.: A small logic language for asking questions of a database with rules, including rules that refer to themselves, such as 'X is an ancestor of Y if X is a parent of an ancestor of Y'.
- resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.
- forward chainingforward chaining, n.: A way of reasoning that starts from known facts and keeps applying rules to them, adding each new conclusion, until it reaches an answer or nothing new can be concluded.
- propositional logicpropositional logic, n.: The simplest formal logic: whole statements that are either true or false, joined by 'and', 'or', 'not' and 'if… then', with exact rules for working out whether the combination is true.
Sources
- Horn, A. (1951). On Sentences Which Are True of Direct Unions of Algebras. Journal of Symbolic Logic 16(1), 14–21.
- van Emden, M. H. & Kowalski, R. A. (1976). The Semantics of Predicate Logic as a Programming Language. Journal of the ACM 23(4), 733–742.
Mentioned in
forward chainingforward chaining, n.: A way of reasoning that starts from known facts and keeps applying rules to them, adding each new conclusion, until it reaches an answer or nothing new can be concluded., logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction., propositional logicpropositional logic, n.: The simplest formal logic: whole statements that are either true or false, joined by 'and', 'or', 'not' and 'if… then', with exact rules for working out whether the combination is true., DatalogDatalog, prop. n.: A small logic language for asking questions of a database with rules, including rules that refer to themselves, such as 'X is an ancestor of Y if X is a parent of an ancestor of Y'., inductive logic programminginductive logic programming, n.: A kind of machine learning that discovers general logical rules — such as 'X is a grandparent of Z if X is a parent of a parent of Z' — from examples and background knowledge., resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.