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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.