Merge in mathematical logic

Question

I am studying mathematical logic and the study material is Introduction to Logic website. There is a section about using merge in linear resolution. It says:

"A merge is a resolvent that inherits a literal from each parent such that this literal is collapsed to a singleton by the most general unifier. The completeness of linear resolution is preserved even if the ancestors that are used are limited to merges. Note that, in this example, the first resolvent (i.e., clause $\{q\}$) is a merge."

I am curious whether I correctly understood the meaning of merge. For example, if there are two clauses $\{x\}$ and $\{y\}$, then $\{x\}$ (or $\{y\}$) alone can be called a merge because we can collapse them into a singleton by using an MGU $\{y$ <- $x\}$ (or $\{x$ <- $y\}$, respectively)?

Answer 1

I think we need to look at the parents of the deduced clause.

Suppose P and Q binary predicates, a is a constant, x and y are variables, and we have the clauses:

P(a, y) | Q(x, y). (Genesereth would write {P(a, y), Q(x, y)} instead)

and

-Q(a, a) | P(a, a).

The most general unifier yields P(a, a) | P(a, a). P(a, a) comes from each parent. But, P(a, a) | P(a, a) collapses to P(a, a) by the idempotence of '|'. Thus, the merge here is P(a, a).

I think a merge can inherit parts from each clause also. On p. 229-230 of J. A. Kalman's Automated Reasoning with OTTER, there exists an example in a section on "merging" where the clauses

-P(x, y) | Q(x) | Q(y).

and

P(a, a).

get used and says that Q(a) | Q(a), but only Q(a) gets kept (and I think we can call Q(a) the 'merge'). Here, the constant 'a' comes from the second parent, while the predicate 'Q' comes from the first parent. Though, maybe that indicates the above definition inconsistent with Kalman's, I'm not sure.

I don't think that the clauses {x} and {y} collapse via a merge, since I think merges only happen from a disjunction collapsing to a single formula.

In Genesereth's he writes that {q} is the first resolvent. If you scroll up, the first two clauses listed are {p, q} and {$\lnot$p, q}. So, resolution yields {q, q} which collapses to just {q}. If you know any set theory, this perhaps suggests why Genesereth uses the notation that he does, since in set theory {x, x} = {x}.

{x} and {y} do NOT merge because there is no resolution of those clauses. There does not exist a resolvent, since a resolvent can only exist when at least one literal is positive and one is negative. So, the answer to your question is 'no'. {x, y} also won't merge, because the variables there are distinct.