Are there efforts to consider forward or backward (theorem proving) logical inference process as Markov decision process in which the the action space is: 1) selection of the inference rule (e.g. from the sequent calculus) (or more generally - selection of Coq or Isabelle/HOL tactic); 2) selection of the premises for which the inference rule is applied). If such redefinition is possible then reinforcement learning can be applied for the logical inference. I am aware of the use of reinforcement learning in the theorem proving (e.g. by Prague AI4Reason group), but 2 things are lacking in their efforts: 1) they use subsymbolic representation for the premises; 2) they consider backward reasoning (theorem proving) only. Forward reasoning (with extra large search space and changes of creative discoveries) is more interesting case.