Goal-Oriented Conjecturing for Isabelle/HOL

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F18%3A00328681" target="_blank" >RIV/68407700:21730/18:00328681 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007%2F978-3-319-96812-4_19" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-319-96812-4_19</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-96812-4_19" target="_blank" >10.1007/978-3-319-96812-4_19</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Goal-Oriented Conjecturing for Isabelle/HOL

Popis výsledku v původním jazyce

We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to identify and prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle’s strong automation to identify and prove such conjectures.

Název v anglickém jazyce

Goal-Oriented Conjecturing for Isabelle/HOL

Popis výsledku anglicky

We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to identify and prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle’s strong automation to identify and prove such conjectures.

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

Intelligent Computer Mathematics

ISBN

978-3-319-96811-7

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

7

Strana od-do

225-231

Název nakladatele

Springer Nature

Místo vydání

—

Místo konání akce

Hagenberg

Datum konání akce

13. 8. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

—