Hi all, I have two questions about resolution principle in math logic theory.
I know, how to arrange formulas for the resolution method (CNF, Skolem...) but I don't know two things during resolution process.
1) Can I repeatedly use the same clause? For example: I will make resolution with clauses 1 and 2. I write the resolvent to the end of the list. Can I use the same variables or predicates of the 1st clause again for another resolution?
2) Is there any rule that I have to use all basic clauses for resolution or I can stop just in the moment I find the empty resolvent? For explanation - theoretically - If I have 5 initial clauses in the list and I find empty resolvent during first resolution. Is it OK or I have to continue and try all remaining clauses?
Thank you in advance for the answer. Sorry for my English...