A new version of transition logic is presented. It integrates (dynamic) transitions, which change world states, and classical (static) reasoning, restricted in the paper to Horn logic. This is achieved by dening a deductive relationship `(T ; ) among formulas for a partially ordered set (T; ) of transitions. This novel integration might form the core for a unied framework for practical reasoning with the potential of a full exploitation of the maturing techniques from classical planning and deduction. For the chosen formula type the logic at the same time oers one possible clarication of the deductive formalism envisioned for original STRIPS but never made precise before.