Consider one gives you $n$ digits of a (possibly irrational) number and a finite set of math operators and constants, like $\{\sin(x), \ln(x),+,\times, \pi,e,7\}$. Then he asks you to build a mathematical expression just using these operators and constants which its $n$ first digits are exactly what is given to you. For example:
For the number $6.5892187094970913045\,$with $20$ digits, the expression $7+\sin(e+\pi)$ is a solution because the first $20$ digits of its value are exactly what is given but there might be other solutions too.
Is there any effective algorithm or software to solve this type of problems at least in very simple cases? If yes, please introduce your references. When is there a unique expression for a given number up to a fixed set of operators and constants? What sort of necessary and sufficient conditions are necessary for proving such a uniqueness?
Well, for very simple cases brute force might work, since "simple" implies a complexity bound. Convert your set of constants and operators to a context-free grammar, generate terms, and evaluate the terms to see if they satisfy your equality condition; quit when you hit the complexity bound. A reference:
Generating all words in a language from CFG
Showing uniqueness is going to be tougher. Here's a somewhat artificial example for you. Imagine a theory which contains no axioms asserting the equality of any two terms. Now think of the Herbrand Universe: no two terms can be equal, so once the algorithm finds a solution, it's guaranteed to be unique. I can't think of a proof right now, but I suspect the uniqueness condition is going to be closely tied to the particulars of the theory under consideration.