= Subformula
A <subformula> is a constituent <propositional formula> in a formula's recursive construction, including the whole formula itself. For an atomic variable the only <subformula> is itself; for $\neg A$, add $\neg A$ to the <subformulas> of $A$; for a binary connective, add the combined formula to the union of the two operands' <subformulas>. The set of distinct <subformulas> can have smaller cardinality than the number of occurrences in the <abstract syntax tree> when the same expression appears more than once.
Back to article page
