Let $\FF$ be a formal language with alphabet $\AA$.
Let $S$ be a collation in $\AA$.
A parsing sequence for $S$ in $\FF$ is a sequence of collations in $\FF$ formed by application of rules of formation of $\FF$ from previous collations in this sequence, and ending in the collation $S$.
If $S$ has no parsing sequence in $\FF$, then it is not a well-formed formula in $\FF$.
A parsing sequence for a given well-formed formula in any formal language is usually not unique.
Thus, we can determine whether $S$ is a well-formed formula in any formal language by using a sequence of rules of formation of that language.
To parse a collation in a formal language is to find a parsing sequence for that collation, and thereby to determine whether or not it is a well-formed formula.
Also known as
Some sources call a parsing sequence a derivation.
Other sources use the term derivation tree or formation tree.
The latter names arise from the presentation of the parsing sequence as a labeled tree.
- 1993: M. Ben-Ari: Mathematical Logic for Computer Science ... (previous) ... (next): Chapter $2$: Propositional Calculus: $\S 2.2$: Propositional formulas
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.2$: Syntax of Propositional Logic
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.3$: Propositional logic as a formal language
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.1.6$