Transformers have been shown to emulate logical deduction over natural\nlanguage theories (logical rules expressed in natural language), reliably\nassigning true/false labels to candidate implications. However, their ability\nto generate implications of a theory has not yet been demonstrated, and methods\nfor reconstructing proofs of answers are imperfect. In this work we show that a\ngenerative model, called ProofWriter, can reliably generate both implications\nof a theory and the natural language proof(s) that support them. In particular,\niterating a 1-step implication generator results in proofs that are highly\nreliable, and represent actual model decisions (rather than post-hoc\nrationalizations). On the RuleTaker dataset, the accuracy of ProofWriter's\nproofs exceed previous methods by +9% absolute, and in a way that generalizes\nto proof depths unseen in training and on out-of-domain problems. We also show\nthat generative techniques can perform a type of abduction with high precision:\nGiven a theory and an unprovable conclusion, identify a missing fact that\nallows the conclusion to be proved, along with a proof. These results\nsignificantly improve the viability of neural methods for systematically\nreasoning over natural language.\n