Internal Guidance for Satallax

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F16%3A00311246" target="_blank" >RIV/68407700:21730/16:00311246 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-40229-1_24" target="_blank" >http://dx.doi.org/10.1007/978-3-319-40229-1_24</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-40229-1_24" target="_blank" >10.1007/978-3-319-40229-1_24</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Internal Guidance for Satallax

Popis výsledku v původním jazyce

We propose a new internal guidance method for automated theorem provers based on the given-clause algorithm. Our method influences the choice of unprocessed clauses using positive and negative examples from previous proofs. To this end, we present an efficient scheme for Naive Bayesian classification by generalising label occurrences to types with monoid structure. This makes it possible to extend existing fast classifiers, which consider only positive examples, with negative ones. We implement the method in the higher-order logic prover Satallax, where we modify the delay with which propositions are processed. We evaluated our method on a simply-typed higher-order logic version of the Flyspeck project, where it solves 26 % more problems than Satallax without internal guidance.

Název v anglickém jazyce

Internal Guidance for Satallax

Popis výsledku anglicky

We propose a new internal guidance method for automated theorem provers based on the given-clause algorithm. Our method influences the choice of unprocessed clauses using positive and negative examples from previous proofs. To this end, we present an efficient scheme for Naive Bayesian classification by generalising label occurrences to types with monoid structure. This makes it possible to extend existing fast classifiers, which consider only positive examples, with negative ones. We implement the method in the higher-order logic prover Satallax, where we modify the delay with which propositions are processed. We evaluated our method on a simply-typed higher-order logic version of the Flyspeck project, where it solves 26 % more problems than Satallax without internal guidance.

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

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2016

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

Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings

ISBN

978-3-319-40228-4

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

13

Strana od-do

349-361

Název nakladatele

Axel Springer Praha, a.s.

Místo vydání

Praha

Místo konání akce

Coimbra

Datum konání akce

27. 6. 2016

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

WRD - Celosvětová akce

Kód UT WoS článku

000491484800024