3
$\begingroup$

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\}$.

$\endgroup$
4
  • $\begingroup$ I omit goal clauses because they never change the output. $\endgroup$
    – Max
    Sep 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$ Sep 21, 2013 at 19:51
  • $\begingroup$ or it can be seen as the backbone of the formula $\endgroup$
    – Mikolas
    Sep 22, 2013 at 23:29
  • $\begingroup$ @RaduGRIGore: make that an answer? $\endgroup$
    – Max
    Oct 30, 2013 at 18:42

2 Answers 2

4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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 \}$

$\endgroup$
6
  • $\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$
    – Guido
    Sep 29, 2013 at 1:34
  • $\begingroup$ It's trivial to obtain the subset of literals from $Cn(\Gamma)$. $\endgroup$
    – Atamiri
    Sep 30, 2013 at 21:09
  • $\begingroup$ That's true, but it does demonstrate that the name of this concept is not the closure. $\endgroup$
    – Max
    Oct 30, 2013 at 18:41
  • $\begingroup$ @Max Right. The appropriate name is "finding a model that satisfies the formulae" (as suggested above). $\endgroup$
    – Atamiri
    Oct 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 D
    Nov 7, 2013 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.