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...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Ashot Baghdasaryan, Hovhannes Bolibekyan
Formato:	article
Lenguaje:	EN
Publicado:	Graz University of Technology 2021
Materias:	Automated theorem prover Minimal logic Loop dete Electronic computers. Computer science QA75.5-76.95
Acceso en línea:	https://doaj.org/article/f2205cc247654498bf82c2913f53472a
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

id	oai:doaj.org-article:f2205cc247654498bf82c2913f53472a
record_format	dspace
spelling	oai:doaj.org-article:f2205cc247654498bf82c2913f53472a2021-11-30T04:30:13ZOn Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic10.3897/jucs.765630948-6968https://doaj.org/article/f2205cc247654498bf82c2913f53472a2021-11-01T00:00:00Zhttps://lib.jucs.org/article/76563/download/pdf/https://lib.jucs.org/article/76563/download/xml/https://lib.jucs.org/article/76563/https://doaj.org/toc/0948-6968There 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.Ashot BaghdasaryanHovhannes BolibekyanGraz University of TechnologyarticleAutomated theorem proverMinimal logicLoop deteElectronic computers. Computer scienceQA75.5-76.95ENJournal of Universal Computer Science, Vol 27, Iss 11, Pp 1193-1202 (2021)
institution	DOAJ
collection	DOAJ
language	EN
topic	Automated theorem prover Minimal logic Loop dete Electronic computers. Computer science QA75.5-76.95
spellingShingle	Automated theorem prover Minimal logic Loop dete Electronic computers. Computer science QA75.5-76.95 Ashot Baghdasaryan Hovhannes Bolibekyan On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
description	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.
format	article
author	Ashot Baghdasaryan Hovhannes Bolibekyan
author_facet	Ashot Baghdasaryan Hovhannes Bolibekyan
author_sort	Ashot Baghdasaryan
title	On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
title_short	On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
title_full	On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
title_fullStr	On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
title_full_unstemmed	On Recurrent Neural Network Based Theorem Prover For First Order Minimal Logic
title_sort	on recurrent neural network based theorem prover for first order minimal logic
publisher	Graz University of Technology
publishDate	2021
url	https://doaj.org/article/f2205cc247654498bf82c2913f53472a
work_keys_str_mv	AT ashotbaghdasaryan onrecurrentneuralnetworkbasedtheoremproverforfirstorderminimallogic AT hovhannesbolibekyan onrecurrentneuralnetworkbasedtheoremproverforfirstorderminimallogic
_version_	1718406779848622080

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

Ejemplares similares