First, all this "worlds" stuff is unnecessary. It's a notion used in some semantics of modal logic. You don't need it to understand modal logic, let alone non-modal logics. This isn't to say it can't be useful, it's just that "worlds" is not some fundamental constituent of logic or their semantics, and, regardless, is not typically used outside of modal logics. As common logic programming languages (i.e. Prolog) are not based on modal logic, there's not much reason to bring it up nor concepts sometimes used in its semantics. You can have modalities in a logic programming language, e.g. LolliMon does. The notion of worlds doesn't really map well onto variable assignments. The problem, among other things, is that you can want multiple different assignments to the same variable at the same time.
Sticking to (pure1) Prolog, due to the restrictions on where you can place connectives, it turns out that it can be understood as operating in a logic with no connectives. Let's consider a fairly general example of a Prolog rule:
p(X,Y) :- q(X,Z), r(W); t(Y).
This corresponds to the logical formula: $$\forall X,Y.(t(Y)\lor(\exists Z.q(X,Z)\land r(W)))\to p(X,Y)$$
First, we can eliminate the universal quantifiers and simplify things by considering entailments between open terms where the free variables will behave like constants. This more or less corresponds to $\forall$ introduction. So $\vdash \forall x.\varphi(x)$ becomes just $\vdash\varphi(x)$. Our example becomes:
$$\vdash (t(Y)\lor(\exists Z.q(X,Z)\land r(W)))\to p(X,Y)$$
We can use the $\to$ introduction (aka the deduction theorem) to eliminate the sole occurrence of $\to$ in any particular rule producing for our example:
$$(t(Y)\lor(\exists Z.q(X,Z)\land r(W)))\vdash p(X,Y)$$
We can use the $\lor$ left rule of the sequent calculus LK/LJ to handle the disjunction. Alternatively we could have used the equivalence $(P\lor Q)\to R\equiv (P\to R)\land(Q\to R)$ before eliminating $\to$ and then used $\land$ introduction, then eliminate $\to$ to produce the same result. We could also eliminate disjunctions (';') via a standard source-to-source transformation of the Prolog that is based on these rules. Our example becomes a pair of entailments:
$$t(Y)\vdash p(X,Y)\qquad \exists Z.q(X,Z)\land r(W)\vdash p(X,Y)$$
We can eliminate the existential with a $\exists$ left rule a la LK/LJ which is basically the dual of $\forall$ introduction and works the same way. That is, we just drop the existentials and the bound variables become free and are treated as constants. Alternatively, this could be understood in terms of the equivalence $(\exists x.\varphi(x))\to\psi\equiv\forall x.\varphi(x)\to\psi$. The relevant entailment of our example becomes:
$$q(X,Z)\land r(W)\vdash p(X,Y)$$
Finally, we can use the $\land$ left rule to eliminate conjunctions, producing:
$$q(X,Z),r(W)\vdash p(X,Y)$$
For an arbitrary (pure) Prolog program, the end result is that we have a collection of rules with a list of premises which consist of atomic formulas entailing a single atomic formula. All connectives can be eliminated. If you don't like this, you can easily go from here to the program corresponding to a series of axioms of the form $\forall\vec{X}.(p_1(\vec{X})\land\cdots\land p_n(\vec{X}))\to q(\vec{X})$, which are Horn clauses, or curry this to get rid of $\land$ producing $\forall\vec{X}.p_1(\vec{X})\to(\cdots(p_n(\vec{X})\to q(\vec{X})\cdots)$. This would mean you only need to understand universal quantification and implication, but even then neither ever occurs in a negative position, so you don't need their full generality which is part of why they can be eliminated. If you want to inject classical logic unnecessarily, you can use material implication and write $\forall\vec{X}.\neg p_1(\vec{X})\lor\cdots\lor\neg p_n(\vec X)\lor q(\vec X)$, and, instead of Cut below, we'd talk about Resolution.
Sticking to the connective-free version, how do we actually prove things? Well, we still have the structural rules. In particular, we have Cut which states (for our purposes):
$$\dfrac{\Gamma\vdash P\qquad\Delta,P\vdash Q}{\Gamma,\Delta\vdash Q}$$
where $P$ and $Q$ are atomic formulas and $\Gamma$ and $\Delta$ are lists of atomic formulas. Cut corresponds to calling a subgoal.
For the top-level call that kicks off the execution of a Prolog program, we aren't trying to show whether the universal closure of the top-level goal is true, but rather listing all the bindings to free variables that makes the goal derivable. This can be seen as enumerating the derivations of $\vdash\exists\vec X.q(\vec X)$ if $q(\vec X)$ is the top-level goal.
For the connection to execution, I recommend getting familiar with the concept of an abstract logic programming language as defined in Uniform Proofs as a Foundation for Logic Programming. This shows how we can interpret connectives as instructions to proof search. By constraining the logic, we can make it so this operational interpretation of the connectives (and atomic formulas), can give a complete proof search procedure (for our highly restricted logic). The elimination of connectives that I've done shows that for Prolog (but not $\lambda$Prolog), the only operational interpretation we need is that of atomic formulas. Non-determinism arises from choosing which rule to use to derive the atomic formula and how to instantiate its free variables. Implementation-wise, the former is usually handled by backtracking and the latter by unification.
If you recorded the steps of the execution of a (pure) Prolog program, the result would be a derivation, i.e. a formal proof. There is no "satisfaction" involved. A Prolog program like p :- q, r does not try assigning different truth values to q and r. There's no way to express a contradiction in (pure) Prolog, so every (pure) Prolog program corresponds to a satisfiable formula.
Datalog is usually analyzed with a more semantic approach, but it has additional restrictions over (pure) Prolog to make this well behaved. Datalog is often implemented in a bottom-up manner where we generate a series of single-step deductions and grow the set of derived facts until we reach a fixed point. Prolog, however, is almost always implemented in a top-down manner where we backchain so that we only derive the facts that are relevant for our goal.
1 This excludes this like assert/retract, cut (!), and the negation-as-failure thing.
