Redlog Documentation Center

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


rlatl – list of atomic formulas

Calling Sequence

rlatl \((\,\varphi\,)\)


\(\varphi\) first-order formula


\(L\) list of atomic formulas


Return the set of atomic formulas occurring in \(\varphi\) as a list. Atomic formulas with multiple occurrences in \(\varphi\) are listed only once.

For additional information on multiplicities of occurrences use rlatml.

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


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

See Also