Goal-Oriented Conjecturing for Isabelle/HOL

Autor:	Julian Parsert, Yutaka Nagashima
Rok vydání:	2018
Předmět:	TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Goal orientation Exploit Computer science Programming language business.industry TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science HOL computer.software_genre business computer Automation
Zdroj:	Lecture Notes in Computer Science ISBN: 9783319968117 CICM
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::0513119d8e613436e34e9f51b0cfe285 https://doi.org/10.1007/978-3-319-96812-4_19 Zobrazit plný text záznamu