PaMpeR: Proof Method Recommendation System for Isabelle/HOL

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F18%3A00329580" target="_blank" >RIV/68407700:21230/18:00329580 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/18:00329580

Výsledek na webu

<a href="https://dl.acm.org/citation.cfm?id=3238210&dl=ACM&coll=DL" target="_blank" >https://dl.acm.org/citation.cfm?id=3238210&dl=ACM&coll=DL</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

PaMpeR: Proof Method Recommendation System for Isabelle/HOL

Popis výsledku v původním jazyce

Deciding which sub-tool to use for a given proof state requires expertise specific to each interactive theorem prover (ITP). To mitigate this problem, we present PaMpeR, a proof method recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users’ expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users’ proof methods invocation especially when it comes to special purpose proof methods.

Název v anglickém jazyce

PaMpeR: Proof Method Recommendation System for Isabelle/HOL

Popis výsledku anglicky

Deciding which sub-tool to use for a given proof state requires expertise specific to each interactive theorem prover (ITP). To mitigate this problem, we present PaMpeR, a proof method recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users’ expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users’ proof methods invocation especially when it comes to special purpose proof methods.

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í

2018

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

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

ISBN

978-1-4503-5937-5

ISSN

—

e-ISSN

—

Počet stran výsledku

11

Strana od-do

362-372

Název nakladatele

ACM

Místo vydání

New York

Místo konání akce

Montpellier

Datum konání akce

3. 9. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

000553784500036