Database programming requires having the knowledge of database semantics both to maintain database integrity and to explore more optimization opportunities. Automated programming of database transactions is desirable and feasible. In general, transactions use simple constructs and algorithms; specifications of database semantics are available; and transactions perform small incremental updates to database contents. Automated programming in such a restricted but wellunderstood and important domain is promising. We approach the synthesis of database transactions that preserve the validity of integrity constraints using deductive tachniques. A transaction logic is developed as the formalism with which the synthesis is conducted. Transactions are generated as the by-product of proving specifications in the logic. The Manna-Waldinger deductive-tableau system is extended with inference rules for the extraction of transactions from proofs, which require the cooperation of multiple tableaux.