What happens to uninterpreted predicates in Ackermann's reduction?
-
03-11-2019 - |
Question
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?
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange