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\}$.
-
$\begingroup$ I omit goal clauses because they never change the output. $\endgroup$– MaxSep 21, 2013 at 9:03
-
4$\begingroup$ It's called finding a minimal model of a set of Horn clauses. (Or "the", because there's only one.) $\endgroup$– Radu GRIGoreSep 21, 2013 at 19:51
-
$\begingroup$ or it can be seen as the backbone of the formula $\endgroup$– MikolasSep 22, 2013 at 23:29
-
$\begingroup$ @RaduGRIGore: make that an answer? $\endgroup$– MaxOct 30, 2013 at 18:42
2 Answers
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 \}$
-
$\begingroup$ 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$). $\endgroup$– GuidoSep 29, 2013 at 1:34
-
$\begingroup$ It's trivial to obtain the subset of literals from $Cn(\Gamma)$. $\endgroup$– AtamiriSep 30, 2013 at 21:09
-
$\begingroup$ That's true, but it does demonstrate that the name of this concept is not the closure. $\endgroup$– MaxOct 30, 2013 at 18:41
-
$\begingroup$ @Max Right. The appropriate name is "finding a model that satisfies the formulae" (as suggested above). $\endgroup$– AtamiriOct 30, 2013 at 18:51
-
$\begingroup$ @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. $\endgroup$– Vijay DNov 7, 2013 at 9:31