He might be thinking about the SLDNF resolution happening. But yes, you can implement any prover in prolog. This distinction is discussed a bit here: https://www.metalevel.at/prolog/theoremproving