Redlog Documentation

rlatnum – number of atomic formulas

Calling Sequence

rlatnum $$(\,\varphi\,)$$

Arguments

 $$\varphi$$ — first-order formula

Returns

 $$n$$ — integer

Description

Count the number of atomic formulas occurring in $$\varphi$$ including multiplicities. This is often used as an indicator for the size of a formula. For determining, in contrast, the number of different atomic formulas use rlatl in combination with length.

Occurrences of the truth values true and false are not counted, because Redlog considers those to be not atomic formulas but logical constants.

Examples

 rlatnum(a = 0 or (b = 0 and b = 0)); rlatnum(a = 0 and true);