1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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][σ]}$ $\endgroup$ Feb 26 at 7:56
  • $\begingroup$ 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$. $\endgroup$ Feb 26 at 8:09

0

You must log in to answer this question.

Browse other questions tagged .