Can someone explain to me this logic sentence using entailment?

Question

Can someone please explain me what does it exactly mean?

$KB \wedge B^- \not\models\square$

I understand the entailment symbol in this example here : $T \models A $ is if there's no model of $FS$ in which all members of $T$ are true and A is false.

Negating the $\models$ symbol means the oposite like : $T \models A $ is if there IS a model of $FS$ in which all members of $T$ are true and A is false?... But what exactly means the square symbol in this case? Actually the title of the question is wrong, but I don't know what exactly mean this symbol, neither it's name. And $KB \wedge B^-$ is all formulas in commom between those two sets?

$KB$ is a set of horn clauses(Knowledge base)

$B^-$ is a set of facts(definite clauses without literals in the body) that, ideally, there's no intersection with the $KB$

Thanks.

Answer 1

In Resolution the "square" symbol : $\square$ is usually used to denote the empty clause, i.e. a contradiction.

The empty clause is always false; thus, the symbol:

$T \vDash \square$

means that the theory $T$ is unsatisfiable.

If so,

$KB ∧ B ⊭ \square$

must mean that the Knowledge base $KB$ plus the set of facts $B$ is satisfiable.