Topic

On Machine Learning Powered Theorem Prover for Propositional Fragment of Minimal Logic

September 11, 2020

Ashot Baghdasaryan

 

Ashot Baghdasaryan1 and Hovhannes Bolibekyan2

1Russian – Armenian University
2Yerevan 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

 

[email protected]