HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

What happens to uninterpreted predicates in Ackermann's reduction?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
predicateswhatreductionuninterpretedhappensackermann

Problem

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?

Solution

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

Context

StackExchange Computer Science Q#52292, answer score: 4

Revisions (0)

No revisions yet.