Machine Learning Guidance for Connection Tableaux

Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: first, we show optimised functional implementations of connection tableaux proof search, including a consistent Skolemisation procedure for...

Descripción completa

Detalles Bibliográficos
Autores principales: Färber, Michael, Kaliszyk, Cezary, Urban, Josef
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer Netherlands 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7900060/
https://www.ncbi.nlm.nih.gov/pubmed/33678931
http://dx.doi.org/10.1007/s10817-020-09576-7
_version_ 1783654142660575232
author Färber, Michael
Kaliszyk, Cezary
Urban, Josef
author_facet Färber, Michael
Kaliszyk, Cezary
Urban, Josef
author_sort Färber, Michael
collection PubMed
description Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: first, we show optimised functional implementations of connection tableaux proof search, including a consistent Skolemisation procedure for machine learning. Then, we show two guidance methods based on machine learning, namely reordering of proof steps with Naive Bayesian probabilities, and expansion of a proof search tree with Monte Carlo Tree Search.
format Online
Article
Text
id pubmed-7900060
institution National Center for Biotechnology Information
language English
publishDate 2020
publisher Springer Netherlands
record_format MEDLINE/PubMed
spelling pubmed-79000602021-03-05 Machine Learning Guidance for Connection Tableaux Färber, Michael Kaliszyk, Cezary Urban, Josef J Autom Reason Article Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: first, we show optimised functional implementations of connection tableaux proof search, including a consistent Skolemisation procedure for machine learning. Then, we show two guidance methods based on machine learning, namely reordering of proof steps with Naive Bayesian probabilities, and expansion of a proof search tree with Monte Carlo Tree Search. Springer Netherlands 2020-09-05 2021 /pmc/articles/PMC7900060/ /pubmed/33678931 http://dx.doi.org/10.1007/s10817-020-09576-7 Text en © The Author(s) 2020 Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
spellingShingle Article
Färber, Michael
Kaliszyk, Cezary
Urban, Josef
Machine Learning Guidance for Connection Tableaux
title Machine Learning Guidance for Connection Tableaux
title_full Machine Learning Guidance for Connection Tableaux
title_fullStr Machine Learning Guidance for Connection Tableaux
title_full_unstemmed Machine Learning Guidance for Connection Tableaux
title_short Machine Learning Guidance for Connection Tableaux
title_sort machine learning guidance for connection tableaux
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7900060/
https://www.ncbi.nlm.nih.gov/pubmed/33678931
http://dx.doi.org/10.1007/s10817-020-09576-7
work_keys_str_mv AT farbermichael machinelearningguidanceforconnectiontableaux
AT kaliszykcezary machinelearningguidanceforconnectiontableaux
AT urbanjosef machinelearningguidanceforconnectiontableaux

Ejemplares similares