Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

A Learning-Based Fact Selector for Isabelle/HOL

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

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

  • Výsledek na webu

    <a href="https://doi.org/10.1007/s10817-016-9362-8" target="_blank" >https://doi.org/10.1007/s10817-016-9362-8</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/s10817-016-9362-8" target="_blank" >10.1007/s10817-016-9362-8</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    A Learning-Based Fact Selector for Isabelle/HOL

  • Popis výsledku v původním jazyce

    Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our "zero click" vision: MaSh integrates seamlessly with the users' workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.

  • Název v anglickém jazyce

    A Learning-Based Fact Selector for Isabelle/HOL

  • Popis výsledku anglicky

    Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our "zero click" vision: MaSh integrates seamlessly with the users' workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.

Klasifikace

  • Druh

    J<sub>imp</sub> - Článek v periodiku v databázi Web of Science

  • CEP obor

  • OECD FORD obor

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

Návaznosti výsledku

  • Projekt

  • Návaznosti

    R - Projekt Ramcoveho programu EK

Ostatní

  • 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ů

Údaje specifické pro druh výsledku

  • Název periodika

    Journal of Automated Reasoning

  • ISSN

    0168-7433

  • e-ISSN

    1573-0670

  • Svazek periodika

    57

  • Číslo periodika v rámci svazku

    3

  • Stát vydavatele periodika

    CZ - Česká republika

  • Počet stran výsledku

    26

  • Strana od-do

    219-244

  • Kód UT WoS článku

    000382693500002

  • EID výsledku v databázi Scopus

    2-s2.0-84957604800