Negation and Control

'!'/0

Cut (discard) all choice points made since the parent goal started execution. Cuts across tabled predicates are not valid. The compiler checks for such cuts, although whether the scope of a cut includes a tabled predicate is undecidable in the presence of meta-predicates like call/1. Further discussion of conditions allowing cuts and of their actions can be found in Section 5.1.

fail_if(+P)

If the goal P has a solution, fails, otherwise it succeeds. Equivalently, it is true iff call(P) (see Section 6.8) is false. Argument P must be ground for sound negation as failure, although no runtime checks are made by the system.

The standard predicate fail_if/1 is compiled by the XSB compiler.

Exceptions:

instantiation_error

P is not instantiated.

type_error

P is not a callable term.

Exactly the same as fail_if/1. Its existence is only for compatibility with other Prolog systems.

not +P

If the goal P has a solution, fails, otherwise it succeeds. It is defined by:

	not(P) :- call(P), !, fail.
	not(_).

Argument P must be ground for sound negation, although no runtime checks are made by the system.

Note that in contrast to the other two kinds of negation as failure ( $\tt '\backslash+'\!/1$ and fail_if/1), predicate not/1 is not compiled by the compiler but the above definition is used.

Exceptions: The same as call/1 (see Section 6.8).

tnot(+P)

Tabling
The semantics of tnot/1 allows for correct execution of programs with according to the well-founded semantics. P must be a tabled predicate, For a detailed description of the actions of tabled negation for in XSB Version 2.5 see [40,42]. Chapter 5 contains further discussion of the functionality of tnot/1.

Exceptions:

instantiation_error

P is not ground (floundering occurs).

type_error

P is not a callable term.

table_error

P is not a call to a tabled predicate.

sk_not(+P)

Tabling
If +P is a tabled predicate, sk_not/1 acts as tnot/1 but permits variables in its subgoal argument. This replaces the 't not'/1 predicate of earlier XSB versions whose implementation and semantics were dubious. The semantics in the case of unbound variables is as follows:

... :- ..., sk_not(p(X)), ...

is equivalent to

... :- ..., tnot(pp), ...
pp :- p(X).

where pp is a new proposition. Thus, the unbound variable X is treated as $\tt tnot(\exists X (p(X)))$.

If +P is a non-tabled predicate ensures that +P is ground and called via a tabled predicate so that sk_not/1 can be used with non-tabled predicates as well, regardless of whether +P is ground or not.

P -> Q ; R

Analogous to if P then Q else R, i.e. defined as if by

	(P -> Q ; R) :- P, !, Q.
	(P -> Q ; R) :- R.

P -> Q

When occurring other than as one of the alternatives of a disjunction, is equivalent to:

P -> Q ; fail.

repeat

Generates an infinite sequence of choice points (in other words it provides a very convenient way of executing a loop). It is defined by the clauses:

	repeat.
	repeat :- repeat.