# What happens to uninterpreted predicates in Ackermann's reduction?

I know the procedure to apply the Ackermann's reduction to a formula that doesn't involve uninterpreted predicates. But, how do we treat the uninterpreted boolean predicates? Nearly all the examples I have seen, usually just assume there are no uninterpreted predicates, and give examples of simpler reductions, but if we have something like this:

$$p(z, F(x_1)) \wedge F(F(x_1)) = G(x_2,G(x_1,x_3,x_4),F(x_2)) \rightarrow p(x_1,y)$$

How will I get rid of the uninterpreted predicate, so that I can apply the usual reduction?

• When I googled Ackermann's reduction, the first hit was this slide set which seems to answer your question starting from slide 36. Does it? – Derek Elkins Jan 26 '16 at 4:14
• @DerekElkins I saw that too, but it wasn't very helpful. I don't see where it mentions specifically uninterpreted predicates. – Yunyao Jan 26 '16 at 8:48
• Ah, okay. I missed that distinction. – Derek Elkins Jan 26 '16 at 10:16

Getting rid of $F$ and $G$ first:
\begin{align*} p(z,f_1)&\wedge f_2=g_1\to p(x_1,y)\wedge x_1=f_1\to f_1=f_2\\ &\wedge x_1=x_2\to f_1=f_3\wedge f_1=x_2\to f_2=f_3\\ &\wedge (x_1=x_2\wedge g_2=x_3\wedge f_3=x_4)\to g_1=g_2 \end{align*}
Introduce boolean variables $b_1,b_2$ for $p(z,f_1)$ and $p(x_1,y)$, respectively, and add a condition that they are equivalent when the arguments agree:
\begin{align*} b_1 &\wedge f_2=g_1\to b_2\wedge x_1=f_1\to f_1=f_2\\ &\wedge x_1=x_2\to f_1=f_3\wedge f_1=x_2\to f_2=f_3\\ &\wedge (x_1=x_2\wedge g_2=x_3\wedge f_3=x_4)\to g_1=g_2\wedge (z=x_1\wedge f_1=y)\to(b_1\leftrightarrow b_2) \end{align*}