If we convert ∃u ∀v ∀x ∃y (P(f(u), v, x, y) → Q(u, v, y)) to ∀v ∀x (P(f(a), v, x, g(v, x)) → Q(a, v,…
Existentialu precedes universals, so introduce freshconstanta. Existentialy occurs afterforallv, x, so replace it consistently by freshfunctiong(v, x). Existential…
Choose your answer
If we convert
∃u ∀v ∀x ∃y (P(f(u), v, x, y) → Q(u, v, y)) to
∀v ∀x (P(f(a), v, x, g(v, x)) → Q(a, v, g(v, x)))
This process is known as
Answer and explanation
Correct answer C
Existentialu precedes universals, so introduce freshconstanta. Existentialy occurs afterforallv, x, so replace it consistently by freshfunctiong(v, x). Existential elimination with those dependency arguments is Skolemization. It preserves satisfiability in an expanded vocabulary, not logical equivalence with the unexpanded formula; unification and resolution do different transformations.
Practice for these exams
-
UGC NET Computer Science and Applications