I know the theorem of "Completeness for Resolution principle", but i have a question :
if the resolution principle is complete, this means that via only the binary resolution we are able to find EVERY logical consequence of the initial set of clauses .
However the resolution principle uses the modus ponens and we know that there exist other inference rules beyond it, like generalization. Why the modus ponens is able to generate by itself every possible logical consequence?
When applied to FOL, the Resolution technique presupposes:
first, that the formulas must be "skolemized", with all quantification becomes implicit: universal quantifiers are simply omitted as understood, while existentially-quantified variables are replaced by Skolem functions
second: clauses must be converted to conjunctive normal form.
After the above transformations, the problem is reduced to as "propostional problems" (the caluses contain only atoms), where modus ponens suffices.
The inference rule used in the various algorithmic implementations of Resoution is refutation-complete, meaning that a set of clauses is unsatisfiable if and only if there exists a derivation of the empty clause using resolution alone.
See: Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), Chapter 10: First-Order Logic: Resolution, for a complete treatment, and see page 200:
Also very useful: Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press (1973).