Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.


rlatnum – number of atomic formulas

Calling Sequence

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


\(\varphi\) first-order formula


\(n\) integer


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.


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

See Also