I have been searching for an automatic method (a computer program) to evaluate any first-order logic (FOL) formula given some knowledge base. The most common approach to do this is to use PROLOG. The issue with PROLOG is that it employs a subset of FOL which, for example, restricts the use of quantifiers.
When searching about this, I have learned that PROLOG uses the resolution algorithm, which requires formulae to be in Conjunctive Normal Form (CNF). I have also learned that there is a process called Skolemnization that can be used to remove the quantifiers from a formula and help convert it into CNF.
Therefore, my question is the following: Can the resolution algorithm be applied to any FOL formula? By this, I mean if there exists some algorithm that takes as input any FOL formula and normalizes it (using skolemnization and other methods) into CNF so that resolution can be applied to it?