# In logic, how can "safe" mean "ground?"

I'm working through an [automated reasoning paper]1. Thy make a statement (shown here in bold) that I can't figure out on page 9:

The hypertableau calculus (Baumgartner et al., 1996) is based on the observation that,if the literals in $$C_1σ\lor...\lor C_n σ$$ do not share variables, we can replace the clause with a nondeterministically chosen atom $$C_iσ$$ that we assume to be true. If we assume that all clauses are safe (i.e., that each variable occurring in a clause also occurs in the clause's antecedent), then $$A_i\lor D_i$$ and $$C_1σ\lor...\lor Cnσ$$ are always ground, so they can always be nondeterministically split into atoms. Such a hypertableau inference is written as $$\frac{A_1\ldots A_m\quad B_1\land\ldots\ \to C_1\lor\ldots\lor C_k}{C_1σ|\ldots|C_kσ}$$ where $$σ$$ is the most general unifier of $$(A_1,B_1),\ldots,(A_m,B_m)$$ and $$|$$ represents or-branching.On Horn clauses, each inference is deterministic,6 and the calculus exhibits a "minimal" amount of don’t-known nondeterminism on general clauses.

6. As mentioned before, the order in which inferences are applied is nevertheless don’t-care nondeterministic.

I don't see how an assumption that clauses are safe, a term which permits variables, leads to a natural conclusion that such clauses are ground, which forbids them. How do they claim that the former leads to the latter? It strikes me a clause such as $$P(x)\to Q(x)$$ where $$x$$ is a variable is safe (the only variable occurring, $$x$$ is found in the antecedent), but it isn't ground.

• Symbolism cumbersome, terminology idiosyncratic... quite difficult. In a nutshell, the rule is the "good, old" Resolution: $\frac{A_1\lor D_1 \quad \lnot A_1\lor ( C_1\lor\ldots\lor C_k)}{D_1[\sigma] \lor C_1[σ] \lor \ldots \lor C_k][σ]}$ Feb 26 at 7:56
• Maybe useful Peter Baumgartner etc Hyper Tableaux (1996): it seems that if the "safe" condition is satisfied, we can resolve also a case $Px$ and $\lnot Py$. Feb 26 at 8:09