Towards evolutionary theorem proving for Isabelle/HOL

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F19%3A00339873" target="_blank" >RIV/68407700:21230/19:00339873 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/19:00339873

Výsledek na webu

<a href="https://doi.org/10.1145/3319619.3321921" target="_blank" >https://doi.org/10.1145/3319619.3321921</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3319619.3321921" target="_blank" >10.1145/3319619.3321921</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards evolutionary theorem proving for Isabelle/HOL

Popis výsledku v původním jazyce

Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation.

Název v anglickém jazyce

Towards evolutionary theorem proving for Isabelle/HOL

Popis výsledku anglicky

Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation.

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í

2019

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

GECCO 2019 Companion - Proceedings of the 2019 Genetic and Evolutionary Computation Conference Companion

ISBN

978-1-4503-6748-6

ISSN

—

e-ISSN

—

Počet stran výsledku

2

Strana od-do

419-420

Název nakladatele

Association for Computing Machinery

Místo vydání

New York

Místo konání akce

Praha

Datum konání akce

13. 7. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000538328100209