How to express a predicate

Question

The given signaure list $(=, +, y = x^2)$ is defined on the domain of all real numbers.

How can I express a predicate $xy = z$ and what is generic algorithm for solving that kind of problems?

Answer 1

Using the fact that $\,4xy=(x+y)^2-(x-y)^2,\,$ you can see that for all $x, y, z\in \mathbb{R},$

$$xy=z \;\text{ iff }\;(\exists a)(\exists b)\left(a+y=x \;\wedge\; b=a^2 \;\wedge\;((z+z)+(z+z))+b=(x+y)^2\right).$$

However, there is no algorithm that can solve this sort of problem in general for all models with any signature, and for all predicates.