Layered Clause Selection for Saturation-Based Theorem Proving

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F20%3A00344481" target="_blank" >RIV/68407700:21730/20:00344481 - isvavai.cz</a>

Výsledek na webu

<a href="http://ceur-ws.org/Vol-2752/paper3.pdf" target="_blank" >http://ceur-ws.org/Vol-2752/paper3.pdf</a>

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Layered Clause Selection for Saturation-Based Theorem Proving

Popis výsledku v původním jazyce

Clause selection is one of the main heuristic decision points in navigating proof search of saturationbased theorem provers. A recently developed layered clause selection framework allows one to boost a basic clause selection heuristic by organising clauses into groups of more or less promising ones according to a specified numerical feature. In this work, we investigate this framework in depth and introduce, in addition to a previously presented feature (based on the amount of theory reasoning in the derivation of a clause), three new features for clause selection (tracking relatedness to the goal, the number of split dependencies in the Avatar architecture, and closeness to the Horn fragment, respectively). We implemented the resulting clause selection heuristics in the state-of-the-art saturation-based theorem prover Vampire and present an evaluation of these new clause-selection strategies and their combinations over the TPTP and SMTLIB libraries.

Název v anglickém jazyce

Layered Clause Selection for Saturation-Based Theorem Proving

Popis výsledku anglicky

Clause selection is one of the main heuristic decision points in navigating proof search of saturationbased theorem provers. A recently developed layered clause selection framework allows one to boost a basic clause selection heuristic by organising clauses into groups of more or less promising ones according to a specified numerical feature. In this work, we investigate this framework in depth and introduce, in addition to a previously presented feature (based on the amount of theory reasoning in the derivation of a clause), three new features for clause selection (tracking relatedness to the goal, the number of split dependencies in the Avatar architecture, and closeness to the Horn fragment, respectively). We implemented the resulting clause selection heuristics in the state-of-the-art saturation-based theorem prover Vampire and present an evaluation of these new clause-selection strategies and their combinations over the TPTP and SMTLIB libraries.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GJ20-06390Y" target="_blank" >GJ20-06390Y: Zlepšování automatických dokazovačů vět pomocí strojového učení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020

ISBN

—

ISSN

1613-0073

e-ISSN

1613-0073

Počet stran výsledku

19

Strana od-do

34-52

Název nakladatele

CEUR Workshop Proceedings

Místo vydání

Tilburg

Místo konání akce

Paris

Datum konání akce

29. 6. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—