4
$\begingroup$

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?

$\endgroup$
3
  • $\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$ Jan 26, 2016 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$
    – user9201
    Jan 26, 2016 at 8:48
  • $\begingroup$ Ah, okay. I missed that distinction. $\endgroup$ Jan 26, 2016 at 10:16

1 Answer 1

4
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.