I understand how to produce an interpolant for propositional logic, but i have trouble to understand how to produce an interpolant for a first order sentence. I'm using the textbook First-Order logic and automated theorem proving by Melvin Fitting, 2nd edition.
I want to produce an interpolant for the following first-order sentence: $[(\forall x) (P(x) \implies \lnot Q(x)) \land P(c)] \implies \lnot Q(c)$
As for the propositional case i would produce a closed tableau, my tableau looks like this
Using the rules for propositional logic my interpolant would by $(\forall x) [x/c] \lor (\forall x) [x/c]$ but i don't think that this is right. Can someone explain me how to produce an interpolant for this sentence? Thank you.