The disjunction operator allows alternative execution of two goals. If the left operand fails the right operand is only then considered and an attempt to prove the right operand is started. It is a predefined right associative (xfy) operator with a precedence of 1100.
| Examples | |
| true; toprove(a). | the goal 'true' succeeds and the goal 'toprove(a)' is never proven |
| fail; toprove(a). | the goal 'fail' succeeds and proving of the goal 'toprove(a)' is started |