Predicates

Gappa works on sets of facts about real-valued expressions. The following predicates are handled internally:

BND(x,I)

The value of expression x is included in interval I.

ABS(x,I)

The absolute value of expression x is included in interval I.

REL(x,y,I)

The values of expressions x and y satisfy [math] with [math].

FIX(x,k)

The value of expression x is such that [math].

FLT(x,k)

The value of expression x is such that [math].

NZR(x)

The value of expression x is not zero.

EQL(x,y)

Expressions x and y have equal values.

In the definitions above, I denotes an interval whose bounds have known numerical values, while k is a known integer. In the description of the theorems, these parameters will usually be ignored. For instance, BND(x) just means that an enclosure of x is known. In addition, EQL properties are also used to express rewriting hints provided by the user.