* {{mvar|S}} and <math>S'</math> are equivalent according to the specific constraint semantics
A sequence of transitions is a derivation. A goal {{mvar|G}} can be proved if there exists a derivation from <math>\langle G, \emptyset \rangle</math> to <math>\langle \emptyset, S \rangle</math> for some satisfiable constraint store {{mvar|S}}. This semantics formalizes the possible evolutions of an interpreter that arbitrarily chooses the literal of the goal to process and the clause to replace literals. In other words, a goal is proved under this semantics if there exists a sequence of choices of literals and clauses, among the possibly many ones, that lead to an empty goal and satisfiable store.
Actual interpreters process the goal elements in a [[LIFO (computing)|LIFO]] order: elements are added in the front and processed from the front. They also choose the clause of the second rule according to the order in which they are written, and rewrite the constraint store when it is modified.
