Cargando…

Layered Clause Selection for Theory Reasoning: (Short Paper)

Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of th...

Descripción completa

Detalles Bibliográficos
Autores principales: Gleiss, Bernhard, Suda, Martin
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324215/
http://dx.doi.org/10.1007/978-3-030-51074-9_23
_version_ 1783551894216507392
author Gleiss, Bernhard
Suda, Martin
author_facet Gleiss, Bernhard
Suda, Martin
author_sort Gleiss, Bernhard
collection PubMed
description Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of the search space where the chance to find a proof is low. In this paper, we describe a new strategy for controlling the amount of reasoning with explicit theory axioms. The strategy refines a recently proposed two-layer-queue clause selection and combines it with a heuristic measure of the amount of theory reasoning in the derivation of a clause. We implemented the new strategy in the automatic theorem prover Vampire and present an evaluation showing that our work dramatically improves the state-of-the-art clause-selection strategy in the presence of theory axioms.
format Online
Article
Text
id pubmed-7324215
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73242152020-06-30 Layered Clause Selection for Theory Reasoning: (Short Paper) Gleiss, Bernhard Suda, Martin Automated Reasoning Article Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of the search space where the chance to find a proof is low. In this paper, we describe a new strategy for controlling the amount of reasoning with explicit theory axioms. The strategy refines a recently proposed two-layer-queue clause selection and combines it with a heuristic measure of the amount of theory reasoning in the derivation of a clause. We implemented the new strategy in the automatic theorem prover Vampire and present an evaluation showing that our work dramatically improves the state-of-the-art clause-selection strategy in the presence of theory axioms. 2020-05-30 /pmc/articles/PMC7324215/ http://dx.doi.org/10.1007/978-3-030-51074-9_23 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
Gleiss, Bernhard
Suda, Martin
Layered Clause Selection for Theory Reasoning: (Short Paper)
title Layered Clause Selection for Theory Reasoning: (Short Paper)
title_full Layered Clause Selection for Theory Reasoning: (Short Paper)
title_fullStr Layered Clause Selection for Theory Reasoning: (Short Paper)
title_full_unstemmed Layered Clause Selection for Theory Reasoning: (Short Paper)
title_short Layered Clause Selection for Theory Reasoning: (Short Paper)
title_sort layered clause selection for theory reasoning: (short paper)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324215/
http://dx.doi.org/10.1007/978-3-030-51074-9_23
work_keys_str_mv AT gleissbernhard layeredclauseselectionfortheoryreasoningshortpaper
AT sudamartin layeredclauseselectionfortheoryreasoningshortpaper