<p>It's called finding a minimal model of a Horn formula.</p>

<p>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.</p>

CC BY-SA 3.0
2013-11-07T07:53:34.093Z
2013-11-07T07:53:34.093Z
Radu GRIGore
<p>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 \}$</p>

CC BY-SA 3.0
2013-09-29T01:34:59.953Z
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$).
Guido
CC BY-SA 3.0
2013-09-30T21:09:17.197Z
It's trivial to obtain the subset of literals from $Cn(\Gamma)$.
Atamiri
CC BY-SA 3.0
2013-10-30T18:41:11.823Z
That's true, but it does demonstrate that the name of this concept is not the closure.
Max
CC BY-SA 3.0
2013-10-30T18:51:11.260Z
@Max Right. The appropriate name is "finding a model that satisfies the formulae" (as suggested above).
Atamiri
CC BY-SA 3.0
2013-11-07T09:31:29.710Z
@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.
Vijay D
CC BY-SA 3.0
2013-11-07T10:52:15.050Z
@VijayD To get all implied literals you need a closure. There are papers on transitive closures to build up models. Generally decidability won't be different.
Atamiri
CC BY-SA 3.0
2013-09-22T00:24:13.230Z
2013-09-22T00:24:13.230Z
Atamiri
<p>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\}$.</p>

CC BY-SA 3.0
2013-09-21T09:03:33.720Z
I omit goal clauses because they never change the output.
Max
CC BY-SA 3.0
2013-09-21T19:51:55.027Z
It's called finding a minimal model of a set of Horn clauses. (Or "the", because there's only one.)
Radu GRIGore
CC BY-SA 3.0
2013-09-22T23:29:46.820Z
or it can be seen as the backbone of the formula
Mikolas
CC BY-SA 3.0
2013-10-30T18:42:19.797Z
@RaduGRIGore: make that an answer?
Max
<lo.logic><terminology>
All literals implied by a set of horn clauses
Max
# All literals implied by a set of horn clauses

(Asked by: username_0 on 2013-09-21)

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

**Tags:** lo.logic, terminology
> **Comments:**
> **username_0**: I omit goal clauses because they never change the output.  
> **username_1**: It's called finding a minimal model of a set of Horn clauses. (Or "the", because there's only one.)  
> **username_2**: or it can be seen as the backbone of the formula  
> **username_0**: @RaduGRIGore: make that an answer?  

---

## 2 answers

### Answer by username_1 on 2013-11-07. Score: 4 | Accepted answer

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.


---

### Answer by username_3 on 2013-09-22. Score: 2

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

> **Comments:**
> **username_4**: 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$).  
> **username_3**: It's trivial to obtain the subset of literals from $Cn(\Gamma)$.  
> **username_0**: That's true, but it does demonstrate that the name of this concept is not the closure.  
> **username_3**: @Max Right. The appropriate name is "finding a model that satisfies the formulae" (as suggested above).  
> **username_5**: @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.  
> **username_3**: @VijayD To get all implied literals you need a closure. There are papers on transitive closures to build up models. Generally decidability won't be different.  

---

