Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Resolution - Converting to Clause Normal Form

  • Step 5: Skolemization
    • Skolem constant
      • (∃X)(dog(X)) may be replaced by dog(fido) where the name fido is picked from the domain of definition of X to represent that individual X.
    • Skolem function
      • If the predicate has more than one argument and the existentially quantified variable is within the scope of universally quantified variables, the existential variable must be a function of those other variables.
        (∀X)(∃Y)(mother(X,Y)) ⇒ (∀X)mother(X,m(X))
        (∀X)(∀Y)(∃Z)(∀W)(foo (X,Y,Z,W))
        ⇒ (∀X)(∀Y)(∀W)(foo(X,Y,f(X,Y),w))

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.