Automated Invention of Strategies and Term Orderings for Vampire

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F17%3A00318955" target="_blank" >RIV/68407700:21730/17:00318955 - isvavai.cz</a>

Výsledek na webu

<a href="http://www.easychair.org/publications/paper/rsMF" target="_blank" >http://www.easychair.org/publications/paper/rsMF</a>

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Automated Invention of Strategies and Term Orderings for Vampire

Popis výsledku v původním jazyce

State-of-the-art first-order automated theorem provers (ATPs) such as E and Vampire allow a large number of user-specified proof search strategies described by large number of proof-search options. Inventing targeted proof search strategies for a specific prover and specific problem sets is a difficult task. Several machine learning methods that invent strategies automatically for ATPs were proposed previously. One of them is BliStrTune which allows invention of targeted E Prover strategies. In this paper we introduce EmpireTune, an extension of BliStrTune, which additionally supports Vampire prover and we experiment with an innovative method for invention of beneficial term orderings. Furthermore, from an experimental evaluation of the impact of various EmpireTune parameters we derive rules for parameter setting. We provide an experimental evaluation at AIM benchmarks and show a significantly increased performance.

Název v anglickém jazyce

Automated Invention of Strategies and Term Orderings for Vampire

Popis výsledku anglicky

State-of-the-art first-order automated theorem provers (ATPs) such as E and Vampire allow a large number of user-specified proof search strategies described by large number of proof-search options. Inventing targeted proof search strategies for a specific prover and specific problem sets is a difficult task. Several machine learning methods that invent strategies automatically for ATPs were proposed previously. One of them is BliStrTune which allows invention of targeted E Prover strategies. In this paper we introduce EmpireTune, an extension of BliStrTune, which additionally supports Vampire prover and we experiment with an innovative method for invention of beneficial term orderings. Furthermore, from an experimental evaluation of the impact of various EmpireTune parameters we derive rules for parameter setting. We provide an experimental evaluation at AIM benchmarks and show a significantly increased performance.

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/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

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

Rok uplatnění

2017

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

GCAI 2017, 3rd Global Conference on Artificial Intelligence

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Počet stran výsledku

13

Strana od-do

121-133

Název nakladatele

EasyChair Publications

Místo vydání

Manchester

Místo konání akce

Miami

Datum konání akce

18. 10. 2017

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

WRD - Celosvětová akce

Kód UT WoS článku

—