We said in this chapter that resolution cannot be used to generate all logical consequences of a set of sentences. Can any algorithm do this?