Conjunctive Normal Forms:
However there for the resolution rule to resolve two sentences so they must both be in a normalised format called as conjunctive normal form, that is usually abbreviated to CNF.
Just because this is an unfortunate name thus the sentences themselves are made up of sets of disjunctions. Rather than it is implicitly assumed that the complete knowledge base is a big conjunction of the sentences, that is when conjunctive normal form gets its name. But, CNF is usually a conjunction of disjunctions. Most of the disjunctions are madeup of literals that can either be a predicate or the negation of a predicate like for the negation of a proposition or propositional read a proposition:
Thus CNF sentences are of the form as:
(p1 ? p2 ? ... ? pm) ^ (q1? q2 ? ... ? qn) ^ etc.
whether each pi and qj is a literal means that we call the disjunction of that literals a clause. So as a concrete example like,
likes(george, X) ? likes(tony, george) ? ¬ is_mad(maggie)
that is in conjunctive normal form, so:
likes(george, X) ? likes(tony, george) → ¬ is_mad(maggie) ^ is_mad(tony)
this is not in CNF.