Sequent rules allow to create proof obligations from the main formula, that involves some connective, e.g. implication. This is backward chaining strategy for theorem proving. But can I use sequent calculus for the forward chaining: i.e. using sequent rule to eliminate implication and the resulting 2 sequents consider as the new (derived) knowledge (that certainly holds, are asserted) and not as the proof obligations (that should be proved, e.g. by the further expansion using other sequent rules), of course, assuming, that the initial sequent (with implication) has been already shown to be valid (by some other proof or by being axiom - e.g. observed empirically to be universally valid or at least satisfiable for the current assignment function).
This my question the continuation of my efforts started with Can sequent calculus start with facts and assert facts? I.e. can sequent calculus be used as extended rule engines?