# Clarifying the syntax of FindEquationalProof

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 ForAll[$$vars,S$$] or 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

• For Expression e.g. look up in the help: tutorial/Expressions#4715 or tutorial/Expressions#20284 . For Statement from the help of FindEquationProof : "The statements stmt can consist of arbitrary logical combinations of predicates." And a predicate, I think, can be defined as a function that returns True of False. – Daniel Huber Feb 15 at 10:31