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