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?

  • $\begingroup$ 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? $\endgroup$ – Derek Elkins Jan 26 '16 at 4:14
  • $\begingroup$ @DerekElkins I saw that too, but it wasn't very helpful. I don't see where it mentions specifically uninterpreted predicates. $\endgroup$ – Yunyao Jan 26 '16 at 8:48
  • $\begingroup$ Ah, okay. I missed that distinction. $\endgroup$ – Derek Elkins Jan 26 '16 at 10:16

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


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.