On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
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 decid...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | article |
| Lenguaje: | EN |
| Publicado: |
Graz University of Technology
2021
|
| Materias: | |
| Acceso en línea: | https://doaj.org/article/f2205cc247654498bf82c2913f53472a |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| Sumario: | 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. |
|---|