World's most popular travel blog for travel bloggers.

# [Solved]: What happens to uninterpreted predicates in Ackermann's reduction?

, ,
Problem Detail:

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?

#### Answered By : Klaus Draeger

Essentially, you can treat uninterpreted predicates as boolean-valued functions (adding a new boolean sort if necessary) and replace them with boolean variables as you would other functions. For the given example:

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*}