Cargando…

Prolog Technology Reinforcement Learning Prover: (System Description)

We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learni...

Descripción completa

Detalles Bibliográficos
Autores principales: Zombori, Zsolt, Urban, Josef, Brown, Chad E.
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324016/
http://dx.doi.org/10.1007/978-3-030-51054-1_33
_version_ 1783551865670074368
author Zombori, Zsolt
Urban, Josef
Brown, Chad E.
author_facet Zombori, Zsolt
Urban, Josef
Brown, Chad E.
author_sort Zombori, Zsolt
collection PubMed
description We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.
format Online
Article
Text
id pubmed-7324016
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240162020-06-30 Prolog Technology Reinforcement Learning Prover: (System Description) Zombori, Zsolt Urban, Josef Brown, Chad E. Automated Reasoning Article We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released. 2020-06-06 /pmc/articles/PMC7324016/ http://dx.doi.org/10.1007/978-3-030-51054-1_33 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Zombori, Zsolt
Urban, Josef
Brown, Chad E.
Prolog Technology Reinforcement Learning Prover: (System Description)
title Prolog Technology Reinforcement Learning Prover: (System Description)
title_full Prolog Technology Reinforcement Learning Prover: (System Description)
title_fullStr Prolog Technology Reinforcement Learning Prover: (System Description)
title_full_unstemmed Prolog Technology Reinforcement Learning Prover: (System Description)
title_short Prolog Technology Reinforcement Learning Prover: (System Description)
title_sort prolog technology reinforcement learning prover: (system description)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324016/
http://dx.doi.org/10.1007/978-3-030-51054-1_33
work_keys_str_mv AT zomborizsolt prologtechnologyreinforcementlearningproversystemdescription
AT urbanjosef prologtechnologyreinforcementlearningproversystemdescription
AT brownchade prologtechnologyreinforcementlearningproversystemdescription