0
$\begingroup$

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.

$\endgroup$

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.