Clausal normal form for resolution, which approach?

Hello, I've got a small newbie doubt.

I have a knowledge base in propositional logic, composed of a bunch of
well formed formulas. I want to convert them to clausal normal form so
I can perform level-saturation resolution on them. Should I make a big
conjunction (wff1 ^ wff2 ^ wff3...) of all the formulas and then
process them (negation normal form -> prenex normal form -> skolem
normal form -> clausal normal form), or should I process each formula
individually, and then join all the clauses from all the formulas as
the new KB?

Thanks!
.

Quantcast