Have Geek Brain

How does EXISTS single condition skimming work?

If I have a formula:

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = for all / E = exists)

The skolemisation rules say that:

  • if E outside FA is replaced by a constant, or
  • if E inside FA is replaced with a new function, contain all vars outside FA as arguments.

So what should I do in this case? Can I just remove the Exists quantifier or replace it with a constant?

Thanks!

+1


a source to share


1 answer


First, write this using standard notation:

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

Now, applying your second scolemization rule:



∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

So, I replaced ∃z with a function containing all the vars from the outside.

Now it is still not in Skolem normal form because it is not in coevolutionary normal form: the formulas still use a set of clauses (∨). The deletion of this data remains for you.

+3


a source






More articles:


All Articles