Automated Invention of Strategies and Term Orderings for Vampire

Result code in 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>

Result on the web

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

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Automated Invention of Strategies and Term Orderings for Vampire

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>

Continuities

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

Publication year

2017

Confidentiality

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

Article name in the collection

GCAI 2017, 3rd Global Conference on Artificial Intelligence

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Number of pages

13

Pages from-to

121-133

Publisher name

EasyChair Publications

Place of publication

Manchester

Event location

Miami

Event date

Oct 18, 2017

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—