  Reasoning semantically in first-order logic is notoriously a challenge. This
paper surveys a selection of semantically-guided or model-based methods that
aim at meeting aspects of this challenge. For first-order logic we touch upon
resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we
give a preview of a new method called SGGS, for Semantically-Guided
Goal-Sensitive reasoning. For first-order theories we highlight hierarchical
and locality-based methods, concluding with the recent Model-Constructing
satisfiability calculus.
