# All literals implied by a set of horn clauses

What is the name of this problem: given a set of Horn clauses (in fact just definite clauses and facts), find the set of literals which can be deduced from it. E.g. given $\{a, a \Rightarrow b, b \wedge c \Rightarrow d\}$, output $\{a, b\}$.

• I omit goal clauses because they never change the output.
– Max
Sep 21, 2013 at 9:03
• It's called finding a minimal model of a set of Horn clauses. (Or "the", because there's only one.) Sep 21, 2013 at 19:51
• or it can be seen as the backbone of the formula Sep 22, 2013 at 23:29
– Max
Oct 30, 2013 at 18:42

It's called finding a minimal model of a Horn formula.

This model is unique because the intersection of two models of a Horn formula is itself a model. In fact, [Horn, On sentences which are true of direct unions of algebras, 1951] proved the following: A boolean function can be expressed as a conjunction of Horn clauses if and only if its set of models is closed under intersection.

It's finding a closure of a set of formulae. In abstract logic, it's what a Tarskian consequence operator does: $Cn(\Gamma)=\{\varphi : \Gamma \vdash \varphi \}$

• The question asked for the literals, the closure under the consequence operator includes Boolean combinations of literals (for the given example it includes $d\vee b$). Sep 29, 2013 at 1:34
• It's trivial to obtain the subset of literals from $Cn(\Gamma)$. Sep 30, 2013 at 21:09
• That's true, but it does demonstrate that the name of this concept is not the closure.
– Max
Oct 30, 2013 at 18:41
• @Max Right. The appropriate name is "finding a model that satisfies the formulae" (as suggested above). Oct 30, 2013 at 18:51
• @Atamiri, In addition to a different name, there are differences in terms of complexity, decidability etc. when you start considering these problems for richer logics, so it's not useful to think of it in terms of closure. Nov 7, 2013 at 9:31