Section "syntactic"
Uninterpreted function symbols and constants lead to the Herbrand
domain, which can be equipped with equality and comparison. We
provide the usual ISO core standard predicates with a few
restrictions. The Dogelog player does currently not yet support
variable ordering or reference ordering, so that comparison throws
an exception in these cases.
The following syntactic predicates are provided:
- X == Y: [ISO 8.4.1]
- The built-in succeeds when X and Y are syntactically
equivalent, otherwise fails.
- X \== Y: [ISO 8.4.1]
- The built-in succeeds when X and Y are not syntactically
equivalent, otherwise fails.
- X @< Y: [ISO 8.4.1]
- The predicate succeeds when X is syntactically less than Y,
otherwise fails.
- X @>= Y: [ISO 8.4.1]
- The predicate succeeds when X is syntactically greater or
equal to Y, otherwise fails.
- X @> Y: [ISO 8.7.1]
- The predicate succeeds when X is syntactically greater than Y,
otherwise fails.
- X @=< Y: [ISO 8.7.1]
- The predicate succeeds when X is syntactically less or equal
to Y, otherwise fails.
- compare(C, X, Y): [TC2 8.4.2]
- The built-in succeeds in C with the syntactic comparison of X
and Y.
Kommentare