JUCS - Journal of Universal Computer Science 27(11): 1193-1202, doi: 10.3897/jucs.76563

On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic

‡ Russian-Armenian University, Yerevan, Armenia§ Yerevan State University, Yerevan, Armenia

Corresponding author: Ashot Baghdasaryan ( baghdasaryana95@gmail.com ) © Ashot Baghdasaryan, Hovhannes Bolibekyan. This is an open access article distributed under the terms of the Creative Commons Attribution License (CC BY-ND 4.0). This license allows reusers to copy and distribute the material in any medium or format in unadapted form only, and only so long as attribution is given to the creator. The license allows for commercial use. Citation:
Baghdasaryan A, Bolibekyan H (2021) On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic. JUCS - Journal of Universal Computer Science 27(11): 1193-1202. https://doi.org/10.3897/jucs.76563 |

Abstract

There are three main problems for theorem proving with a standard cut-free system for the first order 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. New systems with history mechanisms were introduced for solving the looping problems of automated theorem provers in the first order minimal logic. 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.

Keywords

Automated theorem prover, Minimal logic, Loop detection, Recurrent neural network