A complete, nonredundant algorithm for reversed Skolemization

AbstractAn algorithm is presented which, for an arbitrary literal d containing Skolem functions, outputs a set Q of closed quantified literals with the following properties:]lt|O 1.(i) Soundness: if s ∈ Q, then s ⊃ d.2.(ii) Completeness: if a ⊃ d, then there exists an s ∈ Q such that a ⊃ s.3.(iii) Nonredundancy: if s, t ∈ Q, then neither s ⊃ t nor t ⊃ s.The relation ⊃ is a natural generalization of the implication of predicate logic, and is defined as follows: a ⊃ b iff {sk(a), dsk(b)} is unifiable, where sk denotes Skolemization and dsk denotes the dual operation where the roles of ∀ and ∃ are reversed