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

  • $\begingroup$ 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. $\endgroup$ – Daniel Huber Feb 15 at 10:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.