`P``,`

`Q`- prove
`P`and`Q` `P``;`

`Q`- prove
`P`or`Q` `!`

- cut any choices taken in the current procedure
`call(P)`

- prove (execute)
`P` `\+`

`P`- goal
`P`is not provable `P``->`

`Q``;`

`R`- if
`P`succeeds, prove`Q`; if not, prove`R` `P``->`

`Q`- if
`P`succeeds, prove`Q`; if not, fail `true`

- succeed
`otherwise`

- same as
`true`

`fail`

- fail (start backtracking)
`false`

- same as
`fail`

`repeat`

- succeed repeatedly on backtracking