FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F15%3A00311239" target="_blank" >RIV/68407700:21730/15:00311239 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-662-48899-7_7" target="_blank" >http://dx.doi.org/10.1007/978-3-662-48899-7_7</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-48899-7_7" target="_blank" >10.1007/978-3-662-48899-7_7</a>

Jazyk výsledku

angličtina

Název v původním jazyce

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

Popis výsledku v původním jazyce

FEMaLeCoP is a connection tableau theorem prover based on leanCoP which uses efficient implementation of internal learning-based guidance for extension steps. Despite the fact that exhaustive use of such internal guidance can incur a significant slowdown of the raw inferencing process, FEMaLeCoP trained on related proofs can prove many problems that cannot be solved by leanCoP. In particular on the MPTP2078 benchmark, FEMaLeCoP adds 90 (15.7%) more problems to the 574 problems that are provable by leanCoP. FEMaLeCoP is thus the first AI/ATP system convincingly demonstrating that guiding the internal inference algorithms of theorem provers by knowledge learned from previous proofs can significantly improve the performance of the provers. This paper describes the system, discusses the technology developed, and evaluates the system.

Název v anglickém jazyce

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover

Popis výsledku anglicky

FEMaLeCoP is a connection tableau theorem prover based on leanCoP which uses efficient implementation of internal learning-based guidance for extension steps. Despite the fact that exhaustive use of such internal guidance can incur a significant slowdown of the raw inferencing process, FEMaLeCoP trained on related proofs can prove many problems that cannot be solved by leanCoP. In particular on the MPTP2078 benchmark, FEMaLeCoP adds 90 (15.7%) more problems to the 574 problems that are provable by leanCoP. FEMaLeCoP is thus the first AI/ATP system convincingly demonstrating that guiding the internal inference algorithms of theorem provers by knowledge learned from previous proofs can significantly improve the performance of the provers. This paper describes the system, discusses the technology developed, and evaluates the system.

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í

2015

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

Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings

ISBN

978-3-662-48898-0

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

9

Strana od-do

88-96

Název nakladatele

Bertelsmann Springer CZ

Místo vydání

Praha

Místo konání akce

Suva

Datum konání akce

24. 11. 2015

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

WRD - Celosvětová akce

Kód UT WoS článku

000375574900007