Could someone clarify the definitions of "statement" and "expression" in the manual entry for FindEquationalProof?
The best I can make of it is that an expression $E$ is either a constant, variable, or term created from heads consisting of lower-case letters which aren't already defined in Mathematica. So for example, $p[x]$ is acceptable since $p$ is not already defined in Mathematica, while
PrimeQ$[x]$ is not, since
PrimeQ is already defined in Mathematica.
Similarly, a statement $S$ seems to be either an equation $E_1== E_2$, a term created from a new head $p$ of the form $p[E]$, quantified statements like
Exists[$vars,S$], or logical combinations of expressions like $E_1 \&\& E_2$, $E_1 \| E_2$, where the logical operators come from the Mathematica language. But $S_1 \| S_2$ is presumably disallowed.
Please point out my mistakes. The more formal the answer the better. Many thanks