The abduction problem considered here is to find for a given formula \(\varphi\) some formula \(\alpha\) (a solution) of the form \(\kappa(L_ 1 \& \dots \& L_ n)\) such that \(\alpha \vdash \varphi\), \(\kappa\) is a quantifier prefix and \(L_ 1, \dots, L_ n\) are literals. The authors consider modifications of a well-known algorithm for the propositional case: put \(\varphi\) into a conjunctive normal form \(\&_{i \leq n} {\mathcal D}_ i\), and take \(\alpha = L_ 1 \& \dots \& L_ n\) where \(L_ i \in {\mathcal D}_ i\).
In the case of predicate logic they consider a proof-search tree for a goal formula \(\varphi\) using dummy variables to instantiate existential quantifiers \([\Gamma, \delta(d) / \Gamma, \exists x \delta (x)]\) and dynamic Skolemization to instantiate universal quantifiers \([\Gamma, \delta(h (d_ 1, \dots, d_ k)) / \Gamma\), \(\forall x \delta(x)\), where \(d_ 1, \dots, d_ k\) are all dummy variables of the conclusion]. For each non-closed leaf \(\ell_ i\) of \(\Pi\) let \({\mathcal D}_ i\) be the corresponding disjunction of literals. The authors point out that deriving \(\alpha\) as in the propositional case and then de-Skolemizing (quantifying dummy variables by \(\exists\) and Skolem terms \(h(d_ 1, \dots,d_ k)\) by \(\forall\) in a proper order) is sound and complete: \(\pi \alpha\) is a solution and for each solution \(\gamma\) there is an \(\alpha\) such that \(\gamma \vdash \pi \alpha\).