Convert Sentences to Conjunctive Normal Form

After a raw input string has been converted to , it needs to be converted into a normal form, which is also of the type . However, it is much easier to make inferences using resolution in normal form (conjunctive or implicative). The following functions were impleneted to convert an arbitrary sentence into one in CNF:

• [1)]

This function gets rid of the connective by replacing with

• [2)]

Use de Morgan's law to move the symbol onto atoms (not sentences), replace:

$$\begin{eqnarray*} \neg (p\vee q) & becomes & \neg p\wedge \neg q\\ \neg (p\wedg... ...p & becomes & \forall \, x\, \neg p\\ \neg \neg p & becomes & p \end{eqnarray*}$$

• [3)]

Rename variables that are quantified more than once in a sentence, eg: rename to in the original sentence . This is used to avoid confusions when dropping quantifiers. (NOT implemented).

• [4)]

At this stage, we can safely collect all the quantifiers and move them to the left hand side of a sentence.

• [5)]

Eliminate quantifiers by replacing the quantified variables with skolem constants or skolem functions. In addition, any quantifiers on the left hand side of the sentence may be dropped because any variable left in the sentence must be universally quantified.

• [6)]

Perform the following convertion:

$$\begin{eqnarray*} (a\wedge b)\vee c & becomes & (a\vee c)\wedge (b\vee c)\\ a\vee (b\wedge c) & becomes & (a\vee c)\wedge (b\vee c) \end{eqnarray*}$$

as well as flatenning nested conjunctions and disjunctions.

• [7)]

This is basically the top level function that use the listed helper function as pipeline for transforming a raw sentence into one in conjunctive normal form