**forall**(

`:Cond, :Action`)

`Cond`,

`Action`can be proven. The example verifies that all arithmetic statements in the given list are correct. It does not say which is wrong if one proves wrong.

?- forall(member(Result = Formula, [2 = 1 + 1, 4 = 2 * 2]), Result =:= Formula).

The predicate forall/2
is implemented as `\+ ( Cond, \+ Action)`

, i.e., *There is
no instantiation of Cond for which Action is
false.*. The use of double negation implies that
forall/2

*does not change any variable bindings*. It proves a relation. The forall/2 control structure can be used for its side-effects. E.g., the following asserts relations in a list into the dynamic database:

?- forall(member(Child-Parent, ChildPairs), assertz(child_of(Child, Parent))).

Using forall/2
as `forall(Generator, SideEffect)`

is preferred over the
classical *failure driven loop* as shown below because it makes
it explicit which part of the construct is the generator and which part
creates the side effects. Also, unexpected failure of the side effect
causes the construct to fail. Failure makes it evident that there is an
issue with the code, while a failure driven loop would succeed with an
erroneous result.

..., ( Generator, SideEffect, fail ; true )

If your intent is to create variable bindings, the forall/2 control structure is inadequate. Possibly you are looking for maplist/2, findall/3 or foreach/2.