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...
Autores principales: | , |
---|---|
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 |