In this paper we present new and original formal proofs that definite clause grammars (DCG's) are equivalent in their generative power to Turing machines and type 0 phrase-structure grammars. Both proofs are constructive unlike the previously known ones on the same theme. As such they actually describe two algorithms for transferring from a language description by a Turing machine or a type 0 grammar to a DCG characterization. Along the way, the paper also presents a strict and rigorous formalization of logic grammars and other related notions.