Many algorithms treat the first-order statements as a simple macro language, and generate ground propositions from them.  In 1965, Robinson was the first to propose the idea of performing inference at the level of abstract rather than concrete entities.