Past exam of the computer science course of the University of Oxford / 2015 / Knowledge representation and reasoning (A12076W1)

Solutions cover all three questions.^[ref] Throughout, the vocabulary in question 1 is interpreted as specified in the paper; in particular, the intended meaning of $CountSupervise$ supplies the number of supervised students. Question 2 distinguishes EL from EL with bottom explicitly, since the convention about $\perp$ changes two answers.

The condition about taking the course restricts which students the first-order sentence talks about. Within that condition we need both an inclusive logical disjunction and a prohibition on satisfying both alternatives:The logical conjunction on the right expresses exactly one of the two categories. It does not prohibit unrelated individuals from belonging to both categories: the restriction applies to the students in the antecedent.

The supervisor can depend on the student, so the existential quantification belongs inside the universal quantification:The first-order sentence permits different students to share a supervisor. It requires neither that the supervisor be different from the student nor that the supervisor be a faculty member, since neither additional condition was given.

Using the supplied counting function, an appropriate first-order sentence isHere the counting comparison expresses the threshold and the existential quantification expresses teaching at least one course. The word “if” supplies this direction of logical implication; it does not assert that these are the only reasons a faculty member can be busy. With the intended meanings of the nonlogical symbols, no further counting axioms are needed for this translation. If those meanings were unspecified, the displayed first-order sentence alone would not define arithmetic or connect the counting function to the supervision relation.

Write $S,T,U,M,F,Q,J$ for the atomic formulas $Student(x)$, $Takes(x,KRR,2015)$, $Undergrad(x)$, $Masters(x)$, $FacultyMember(x)$, $GreaterOrEqual(CountSupervise(x),2)$, and $Teach(x,y)$, respectively. These are abbreviations for formulas, not new symbols in the vocabulary. In clausal normal form, with all remaining variables implicitly universally quantified, the three translations become:For (ii), Skolemization introduces the fresh Skolem function $f$. One supervisor suffices even when both categories hold, so the same $f$ can be used in both first-order clauses. For (iii), moving the existentially quantified course out of an antecedent produces a universally quantified variable in the resulting first-order clause:

The resolution with free selection calculus for first-order Horn clauses is sound and refutationally complete for the clause sets from $\boxed{\text{(ii) and (iii)}}$. For example, select the unique positive first-order literal in every definite first-order Horn clause, and select one negative first-order literal in every nonempty clause without a positive one. On the displayed definite first-order Horn clauses, this selects $SupervisedBy(x,f(x))$ or $Busy(x)$. A fair saturation must still consider all permitted inferences. Functions do not invalidate this completeness theorem, although they can prevent termination. ^[ref]

The first first-order clause of (i) has two positive first-order literals, so the Horn resolution with free selection theorem does not apply to that sentence. General first-order resolution, with its usual completeness requirements, can handle it. Soundness of an individual resolution inference is not the issue; the issue is applicability and completeness of this particular restricted calculus.

With existential rules understood as function-free tuple-generating dependencies, $\boxed{\text{only (ii)}}$ belongs to the fragment. Split its antecedent to obtainThese two existential rules have exactly the same meaning as (ii): either category requires a supervisor, and when both hold the same supervisor may witness both requirements.

Sentence (i) requires a genuine choice between two positive alternatives and also an exclusion condition. Positive existential rules cannot enforce that exclusion: interpreting all their relations as full relations on a one-element domain always satisfies them, whereas that interpretation violates (i). Sentence (iii), in the supplied vocabulary, uses the nonconstant function $CountSupervise$ and is therefore outside the function-free fragment. Introducing a new relation for the counting comparison would change the representation and require additional axioms; it is not an equivalent sentence in the stated vocabulary.

For ordinary function-free Datalog, $\boxed{\text{none of the three sentences}}$ has the required form. Sentence (i) is not a definite first-order Horn clause: the category choice gives two positive alternatives, and its second clause is a negative constraint. Even allowing constraints would not remove the positive choice. Semantically, the category-choice condition fails closure under intersection of interpretations with fixed domain and functions: one model can choose only the undergraduate category, another only the masters category, and their intersection chooses neither.

Sentence (ii) needs an existentially supplied supervisor. Function-free Datalog cannot demand such a witness without naming or otherwise fixing it in the rule. Its Skolemized form is a first-order Horn clause with a function, rather than a Datalog rule. Sentence (iii) also contains a nonconstant function. Being Horn is therefore insufficient for membership in Datalog.

The standard relational guarded fragment contains $\boxed{\text{(i) and (ii)}}$. In (i), $Student(x)$ guards the only quantified variable:The constants in the course-taking relation do not introduce additional free variables that need guarding.

For (ii), use the two implications from part (c)(i). Each outer universal quantification is guarded by its unary category predicate. The inner existential quantification can be writtenwhose guard contains both $x$ and $y$. Sentence (iii) uses a nonconstant function and so is outside the standard relational guarded fragment. This conclusion uses the original vocabulary; it does not silently replace the counting term by a fresh relation.

In ALC, $\boxed{\text{only (ii)}}$ is representable over the given symbols. It is the general concept inclusionEquivalently, use one general concept inclusion for each category. Unary predicates become description logic concepts and the supervision predicate becomes a description logic role.

Sentence (i) depends on a ternary predicate evaluated at two named constants. Basic ALC has unary description logic concepts and binary description logic roles, with no constructor for that course-and-year slice of a ternary predicate. Sentence (iii) uses a counting function and a comparison relation that basic ALC cannot express. Replacing these conditions by freshly named description logic concepts would give an informal encoding, but would not define their meanings or establish equivalence in the supplied vocabulary.

For resolution, a first-order sentence is in clausal normal form when it is a universally quantified logical conjunction of first-order clauses:where every $L_{ij}$ is a first-order literal, meaning an atomic formula or the logical negation of an atomic formula. The quantifiers are often left implicit and the first-order clauses treated as a set. The empty first-order clause represents falsity; an empty set of first-order clauses represents truth.

A convention that allows an arbitrary quantifier prefix followed by a conjunctive matrix is weaker: that is a prenex normal form with a conjunctive matrix. The elimination of existential quantifiers by Skolemization is the extra step relevant to resolution and to part (ii).

The usual transformation to clausal normal form preserves $\boxed{\text{equisatisfiability, but not necessarily logical equivalence}}$. Removing implications and distributing logical conjunction and logical disjunction preserve logical equivalence. Skolemization introduces new symbols and chooses witnesses as functions of preceding universally quantified variables.

For example,On the domain $\{0,1\}$, let $R$ be equality. Then $\phi$ is true. Expand this same first-order structure by interpreting $f$ as the constant function with value $0$. The resulting first-order structure falsifies $\psi$ at $x=1$. Interpreting $f$ as the identity instead satisfies $\psi$.

Thus every model of $\psi$ has a reduct satisfying $\phi$, and a model of $\phi$ can be expanded with suitable witnesses to satisfy $\psi$. That model-expansion property gives equisatisfiability, not logical equivalence for every interpretation of the added function. If “CNF” means a conjunctive matrix with existential quantifiers retained, Skolemization has not yet happened and an equivalent form is possible; this is why the convention must be specified.

An exponential increase is unavoidable for an equivalent conjunctive normal form over the original variables. Consider the linear-size Boolean formulaDistributing gives the $2^n$ Boolean clausesTo prove that the growth is necessary, fix one choice $r_i\in \{p_i,q_i\}$. Let ${\alpha }_r$ make every $r_i$ false and its partner true. Each pair then contains a false variable, so $F_n$ is false. Any equivalent conjunctive normal form must contain a Boolean clause $C$ falsified by ${\alpha }_r$ and entailed by $F_n$.

Every individual term $p_i\wedge q_i$ entails $C$, because that term implies $F_n$. After tautological Boolean clauses are discarded, this forces $C$ to contain a positive $p_i$ or positive $q_i$ for every $i$: otherwise set both variables in that pair true and independently falsify all Boolean literals of $C$, contradicting the entailment. Since $C$ is false at ${\alpha }_r$, it must contain the false member $r_i$, never its true partner. Consequently the same $C$ cannot be false at any different ${\alpha }_s$. The $2^n$ different assignments therefore require at least $2^n$ different Boolean clauses.

Writing the answer already takes $\boxed{\Omega (2^n)\text{ time in the worst case}}$. This obstruction applies to first-order logic as well, since the example can be expressed using ground unary atomic formulas. It concerns exact equivalence without auxiliary symbols. A Tseytin transformation can produce a polynomial-size equisatisfiable conjunctive normal form with auxiliary variables, so the statement must not be extended to that different task.

The algorithm is $\boxed{\text{incorrect: it can return true for a non-entailed ground atom}}$. Its recursive calls return only Booleans. They do not return and propagate the first-order substitutions obtained while satisfying earlier rule premises.

Take distinct constants $a,b,c$, factsand the single Datalog ruleAsk for $H(c)$. The head matches the goal without binding $x$. In line 15, the recursive call for $P(x)$ succeeds by first-order unification with $P(a)$, but returns only true. The next recursive call still receives $Q(x)$ with $x$ unbound, and succeeds by first-order unification with $Q(b)$. Neither subgoal is the visited head $H(c)$, so the visited test does not stop these calls. Both recursive results are true, and the algorithm returns true for $H(c)$.

However, the least Herbrand model is just $\{P(a),Q(b)\}$. No single constant makes both $P(x)$ and $Q(x)$ true, so the rule cannot derive $H(c)$. The two individually successful premises need one consistent first-order substitution. A correct backward chaining procedure must thread answer first-order substitutions through the remaining premises and backtrack when they cannot be extended; forward chaining on ground Datalog instances is another way to avoid this error.

A fragment has the finite model property if $\boxed{\text{every satisfiable sentence in the fragment has a finite model}}$. This does not mean that every model is finite, nor that there is one uniform bound on model size for the entire fragment.

ALC has the finite model property, including satisfiability with respect to finite TBoxes. A tableau algorithm for ALC uses finitely many possible labels and direct blocking in description logic to obtain a finite representation of a model. The resulting finite-model claim is a property of the logic; termination alone, for an arbitrary procedure, would not establish it.

Full first-order logic does not have the finite model property. For example, the first-order sentencerequires an irreflexive transitive relation with a successor for every element. It is satisfied by the usual strict order on the natural numbers. In a nonempty finite domain, repeatedly taking successors eventually repeats an element; transitivity would then force $R(x,x)$, contradicting irreflexivity. Hence this satisfiable first-order sentence has no finite model.

An initial split into an acyclic definition and the remaining general concept inclusions isThe definition of $C$ is suitable for TBox unfolding: its right-hand side does not depend on $C$, and $C$ has only this defining left-hand side. The other displayed general concept inclusions do not initially have an atomic defined left-hand side. In particular, $A\sqcap B⊑\perp$ can be rewritten for TBox absorption, but is not already an atomic definition.

Absorb (4) using the equivalenceThus we can takeHere $A⊑\neg B$ is a primitive inclusion, handled by adding $\neg B$ whenever $A$ labels a node. For literal substitution-based TBox unfolding, introduce a fresh description logic concept $A_0$ and replace the primitive inclusion byThis preserves the original models after forgetting $A_0$: any model of the primitive inclusion extends by taking $A_0=A$, and any model of the new definition satisfies the primitive inclusion. The fresh name is important. Replacing $A$ by $\neg B$ alone would incorrectly assert that every non-$B$ element is an $A$ element.

Use the substitution version of TBox unfolding from part (a), and abbreviateThe notation $\overline{L}$ is the negation normal form of $\neg L$. The unfolded input description logic concept isFor the remaining TBox, turn each general concept inclusion $X⊑Y$ into $\neg X\bigsqcup Y$, and unfold all defined names. The global description logic concept to add at every generated node isIn the last line, negating $\exists R.(\exists R.A\bigsqcup \exists R.B)$ gives $\forall R.(\forall R.\neg A\sqcap \forall R.\neg B)$. Both levels of universal restriction are needed.

Start the tableau algorithm for ALC with a root $x$ labelled $D^{\prime }$ and $\Gamma$. Expand the logical conjunctions. For the disjunction from (2), choose $\forall R.\overline{L}$. For the disjunction from (3), choose $\forall R.L$. Apart from the compound formulas already processed, the root label isThere is no existential restriction at $x$, so no successor needs to be generated. In particular, $\forall R.\exists P.\top$ creates a $P$-successor only at an existing $R$-successor; it creates no $R$-successor itself. The branch is complete and has no tableau clash. There is $\boxed{\text{no directly blocked node}}$: the open completion graph has only its root. The universal restrictions can have incompatible fillers without creating a tableau clash when there are no successors.

For comparison, choosing the other alternative $\exists R.\exists R.L$ from (2) creates an $R$-successor $y$. The root restriction $\forall R.(L\sqcap B)$ puts $A_0,\neg B,B$ in $\mathcal{L}(y)$, giving a tableau clash immediately. That branch closes before direct blocking in description logic is needed. The figure records the processed formulas through the label $\Gamma$ and displays the decisive labels explicitly.

A concrete model confirms the open branch:All three remaining general concept inclusions hold because their relevant $R$-successor requirements are vacuous. The definition of $C$ and the disjointness condition hold as well. Thus $\boxed{D\text{ is satisfiable with respect to }\mathcal{T}}$.

Using the absorbed TBox with its primitive inclusion, translate description logic concepts as unary predicates and description logic roles as binary predicates. Concept satisfiability means that some element belongs to $A\sqcap C$, while every element satisfies the TBox axioms. The required first-order sentence isOnly ${\mathcal{T}}_u$ is included here, as requested. There is no requirement to satisfy (1), (2) or (3). For instance, one element with $A=C=\{d\}$, $B=\varnothing$ and $P=\{(d,d)\}$ satisfies this first-order sentence.

Alternatively, unfolding the absorbed TBox first gives the existential first-order sentence $\exists x\exists y(A_0(x)\wedge \neg B(x)\wedge P(x,y))$. The interpretation of the eliminated names is then recovered by $A=A_0\setminus B$ and $C=\{x:\exists yP(x,y)\}$.

For EL with bottom, the eligible axioms are $\boxed{(2),(4),(5)}$. Axioms (1) and (3) contain universal restrictions, and (3) also contains a disjunction, so they are outside its syntax. For plain EL, whose constructors are $\top$, atomic names, conjunction and existential restriction, the eligible axioms are $\boxed{(2),(5)}$; (4) is excluded because it uses $\perp$. These conventions should not be conflated.

Here is a normalized TBox for the bottom-inclusive version. Introduce one fresh description logic concept $X$ for $\exists R.A$, and useThese are the usual normalized forms: an existential restriction on the left with an atomic right-hand side, an atomic left-hand side with an existential restriction on the right, or a conjunction of atomic names implying $\perp$. Here $\top$ is permitted as a filler.

The first two general concept inclusions force $X\equiv \exists R.A$. The third then says $\exists R.A⊑\exists R.\exists R.A$, exactly (2). Conversely, any model of (2) extends by $X=(\exists R.A{)}^{\mathcal{I}}$ to satisfy all three normalized general concept inclusions. The last two are the two directions of (5). For plain EL, delete just $A\sqcap B⊑\perp$ from this normalized TBox.

The standard semantics of ALC and EL do not impose the unique name assumption. Therefore the two individual names may denote the same element. A minimum-size model of either normalized TBox from part (d), together with the ABox, isThe $R$ self-loop supplies the ABox fact and makes both $\exists R.A$ and $\exists R.X$ true at $d$. The $P$ self-loop supplies exactly the existential restriction defining $C$. Disjointness holds because $B$ is empty. Hence every normalized general concept inclusion is satisfied. A domain must be nonempty, so $\boxed{|{\Delta }^{\mathcal{I}}|=1}$ is minimal.

If a separate unique name assumption were imposed, the minimum would instead be two. One can take $a\ne b$, $A=\{a\}$, $C=\{b\}$, $R=\{(a,b)\}$, $P=\{(b,b)\}$ and $B=X=\varnothing$. There is then no $R$-edge ending at an $A$ element, so the normalized requirements involving $X$ hold vacuously. That additional convention is not part of standard description logic semantics.

For plain EL, $\boxed{\text{every concept is satisfiable with respect to every EL TBox}}$. On a one-element domain, interpret every atomic description logic concept as the whole domain and every description logic role as the full binary relation. A structural induction makes every EL description logic concept denote that element. Every general concept inclusion is consequently true, including cyclic ones. The decision procedure can therefore always answer yes on well-formed inputs.

For EL with bottom, concept satisfiability with respect to general TBoxes is $\boxed{\text{P-complete}}$ under the usual logarithmic-space reductions. Polynomial-time completion propagates atomic inclusions, conjunction consequences and existential requirements; deriving $\perp$ for the queried description logic concept detects unsatisfiability. There are polynomially many such labels and normalized relationships to propagate.

For the lower bound, encode a monotone Boolean circuit with a starting description logic concept $S$. Give each input gate labelled one an inclusion $S⊑G_i$. Encode an AND gate by $G_i\sqcap G_j⊑G_k$, and an OR gate by $G_i⊑G_k$ and $G_j⊑G_k$. Finally add $G_{\mathrm{out}}⊑\perp$. Then $S$ is unsatisfiable exactly when the circuit output is one. The complement version is also P-complete, since P is closed under complement. Thus allowing $\perp$ changes a trivial satisfiability problem into a nontrivial polynomial-time one. The bottom-inclusive convention is also reflected in the ^[ref].

The complete numbered axioms in the rule fragment RL description logic are $\boxed{(1),(3),(4)}$. Their translations to Datalog with constraints areThe first rule is (1). For (3), its existential antecedent needs a two-edge $R$ path ending at an $A$ or $B$ element. Split that disjunction into two Datalog rules, and use a separate variable $w$ for an arbitrary immediate $R$-successor of $x$. The conclusion applies to every such successor, not merely the path witness $y$.

The last rule is a constraint: a ground instance with both premises true makes the knowledge base inconsistent. If an implementation permits only positive Datalog heads, replace $\perp$ by a fresh nullary predicate $Bad$ and separately check that it is never derived. Merely deriving $Bad$ without that check would not express disjointness.

Axiom (2) requires an existential witness in its head and is outside RL description logic. Axiom (5), considered as the whole equivalence, is outside for the same reason in the direction $C⊑\exists P.\top$. If definitions are split before selecting eligible general concept inclusions, its reverse direction is eligible and adds $\boxed{P(x,y)\to C(x)}$. Keep the difference between selecting the complete equivalence and retaining its rule-expressible half explicit. The permitted positions of existential and universal restrictions are specified in the ^[ref].

Fix a signature, adding a fresh constant if it otherwise has no ground terms. Its Herbrand universe $U$ is the set of all ground terms, and its Herbrand base $B$ is the set of all ground atoms over $U$. A Herbrand interpretation is identified with a subset $I\subseteq B$: precisely its members are true. Function symbols and constants have their term interpretations.

A least Herbrand model of a knowledge base $\mathcal{K}$ is a Herbrand model $M$ satisfyingIf it exists, it is unique. This is stronger than being minimal: a minimal model merely has no strictly smaller model contained in it.

For a positive definite Datalog program with facts, let $T$ add every fact and the head of every ground rule whose body is already true. Starting from the empty set and repeatedly adding consequences yieldswhere $T$ is taken inflationary, so it also retains its input. Every added ground atom belongs to every model, and the union is closed under every finite rule body. These two facts establish that it is the least Herbrand model. The intersection assertion is guaranteed here by the definite Horn form, not for arbitrary knowledge bases.

$\boxed{\text{No.}}$ A disjunctive Datalog knowledge base can have several incomparable minimal Herbrand models without a least Herbrand model. Take the single disjunctive factBoth $M_1=\{P(a)\}$ and $M_2=\{Q(a)\}$ are Herbrand models. Any least Herbrand model would have to be contained in both, hence contained in $M_1\cap M_2=\varnothing$. But the empty Herbrand interpretation falsifies the disjunctive fact. This is a contradiction. Taking the intersection of all models therefore fails because that intersection need not itself be a model.

Use not for negation as failure, rather than classical logical negation. The disjunctive condition is expressed by two separate Datalog with negation rules:The positive $Year(x)$ premise restricts the rule to years and makes the variable explicitly safe. The divisibility relation is input data; the integer-looking constants do not make arbitrary arithmetic facts true automatically.

The remaining classification rule isThe positive premise restricts the rule to years. Its negation as failure premise is evaluated by stable model semantics; it does not assert a separately stored negative fact. This gives a stratified Datalog program: divisibility and year facts are inputs, leap status is computed next, and common status last.

Add the ground atomTogether with the three rules above, this is the Datalog with negation knowledge base $\mathcal{K}$. There are no supplied divisibility facts and no other year facts. In particular, nothing in this knowledge base asserts $DivisibleBy(N,4)$ or $DivisibleBy(N,100)$.

A Herbrand interpretation $I$ is a stable model when it is the least Herbrand model of its stable model reduct ${\mathcal{K}}^I$. To form the reduct, ground the rules, delete each rule with a premise $\mathrm{not}A$ for which $A\in I$, and remove the remaining occurrences of not and their atoms.

For ${\mathcal{I}}_1$, the rules concerning $N$ in the reduct aretogether with $Year(N)$. No rule has a divisibility atom in its head, so forward chaining produces no divisibility facts and no leap fact. Ground rules for the other constants cannot fire because their year premises are absent. ThusTherefore $\boxed{{\mathcal{I}}_1\text{ is stable}}$.

For ${\mathcal{I}}_2$, the rule using $\mathrm{not}DivisibleBy(N,100)$ is deleted. The common-year rule is retained without its negative premise, since $Leap(N)$ is absent. Crucially, the reduct does not convert atoms already in ${\mathcal{I}}_2$ into facts. Its least Herbrand model is again $\{Year(N),Common(N)\}$. The two divisibility atoms in ${\mathcal{I}}_2$ have no support. Hence

Inspecting these two interpretations alone is not sufficient for skeptical entailment. That requires every stable model to contain $Common(N)$. Here we can finish the argument: every reduct has no rule deriving divisibility atoms, so every stable model has empty divisibility relation. Its leap relation must then be empty as well. The common-year rule consequently derives $Common(N)$, and the only year fact is $Year(N)$. Thus ${\mathcal{I}}_1$ is the unique stable model, andThis final uniqueness argument, rather than the examination of just two candidate interpretations, establishes the required universal claim.

A safe one-rule Datalog with negation example with no stable model isThere are no variables, so no safety condition is violated. If $P(a)$ is absent from a proposed stable model, its reduct contains the fact $P(a)$, whose least Herbrand model contains $P(a)$. If $P(a)$ is present, the rule is deleted, and the reduct has empty least Herbrand model. Either choice disagrees with its reduct's least Herbrand model. Additional unsupported atoms cannot repair the disagreement. Hence there is no stable model.

For polynomial-time many-one reductions, an unconditional example is the empty language:A procedure that rejects every input decides it in constant time, so it belongs to P and hence NP. It is not NP-hard: the nonempty formal language $\{0\}$ belongs to NP, but no many-one reduction $f$ can satisfyThe right-hand side is always false. Thus the hardness condition fails without assuming $\mathsf{P}\ne \mathsf{NP}$. Giving an ordinary nontrivial problem in P would not establish the requested separation unconditionally, because that would require excluding the possibility $\mathsf{P}=\mathsf{NP}$.

The halting problem is an unconditional example:Reduce SAT to it as follows. Given a Boolean formula $\phi$, construct a Turing machine $M_{\phi }$ that ignores its input, enumerates all Boolean valuations of $\phi$, and halts if it finds a satisfying one. If none satisfies $\phi$, it enters an infinite loop after the enumeration. ThenThe construction of the machine description takes polynomial time; the potentially exponential running time of the constructed machine is irrelevant to the time needed to compute the polynomial-time reduction. Since SAT is NP-complete, this proves NP-hardness of the halting problem.

Every problem in NP is decidable, by enumerating the finitely many polynomial-length certificates and running the verifier. The halting problem is undecidable, so it is outside NP and therefore cannot be NP-complete.

The satisfiability problem is $\boxed{\text{decidable}}$. Partition the positive facts according to their predicate symbols. Let ${\mathcal{A}}_{\mathcal{T}}$ contain those using description logic concepts or description logic roles from $\mathcal{T}$. Run an ordinary ALC knowledge base consistency procedure on $(\mathcal{T},{\mathcal{A}}_{\mathcal{T}})$. Return no if it is inconsistent, and yes otherwise.

The no answer is sound because any model of the whole knowledge base would restrict to a model of $(\mathcal{T},{\mathcal{A}}_{\mathcal{T}})$. For the converse, take a model $\mathcal{I}$ of that ALC part. Keep its domain, individual interpretations and TBox predicates. Interpret every predicate used by the positive Datalog rules as the full relation of its arity on this same domain. This is possible because those predicates are disjoint from the TBox predicates. Every Datalog rule head is then true under every variable assignment, so every positive rule and every remaining positive fact is satisfied. Predicates occurring only in facts can likewise be interpreted as full relations. Any individual name not already interpreted can denote an arbitrary domain element.

Consequently,The argument depends on both restrictions in the question: disjoint predicate vocabularies and positive rule heads. A rule concluding $\perp$ would not be made true by filling all relations. Sharing constants alone causes no problem, since the expansion uses the same domain and the same interpretations of those constants.