## Ashot Baghdasaryan

*Ashot Baghdasaryan*^{1} and Hovhannes Bolibekyan^{2}

^{1}and Hovhannes Bolibekyan

^{2}

^{1}Russian – Armenian University

^{2}Yerevan State University

**Abstract:**

There are three main problems for theorem proving with a standard cut-free system for the propositional fragment of minimal logic. The first problem is the possibility of looping. Secondly, it might generate proofs which are permutations of each other. Finally, during the proof some choice should be made to decide which rules to apply and where to use them. In order to solve the rule selection problem, recurrent neural networks are deployed and they are used to determine which formula from the context should be used on further steps. As a result, it yields to the reduction of time during theorem proving. |

**Discussion Room: On Machine Learning Powered Theorem Prover for Propositional Fragment of Minimal Logic**