atoms : term -> term list

SYNOPSIS

Returns a list of the atomic propositions in a Boolean term

DESCRIPTION

When applied to a term of Boolean type, atoms returns a list of the atomic fomulas, considering the term as a propositional formula built up recursively with negation, conjunction, disjunction, implication and logical equivalence, treating all other subterms (e.g. quantified ones) as atomic.

FAILURE CONDITIONS

Fails if the term does not have type :bool.

EXAMPLE

Here the atomic formulas are simply variables:

  # atoms `p \/ q ==> r`;;
  val it : term list = [`r`; `p`; `q`]

while here the atomic formulas are composite:

  # atoms `x < 1 \/ x > 1 ==> ~(x = 1)`;;
  val it : term list = [`x < 1`; `x > 1`; `x = 1`]