Control

P,Q

prove P and Q

P;Q

prove P or Q

M:P

call P in module M

P->Q;R

if P succeeds, prove Q; if not, prove R

P->Q

if P succeeds, prove Q; if not, fail

!

cut any choices taken in the current procedure

\+ P

goal P is not provable

X ^ P

there exists an X such that P is provable (used in setof and bagof)

bagof(X,P,B)

B is the bag of instances of X such that P is provable

call(P)

prove (execute) P

fail

fail (start backtracking)

false

same as fail

findall(T,G,L)

L is the list of all solutions T for the goal G

otherwise

same as true

repeat

succeed repeatedly on backtracking

setof(X,P,S)

S is the set of instances of X such that P is provable

true

succeed