Goal-Oriented Conjecturing for Isabelle/HOL
Logic in Computer Science
2018-07-26 v2
Abstract
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 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.
Cite
@article{arxiv.1806.04774,
title = {Goal-Oriented Conjecturing for Isabelle/HOL},
author = {Yutaka Nagashima and Julian Parsert},
journal= {arXiv preprint arXiv:1806.04774},
year = {2018}
}
Comments
This paper has been accepted at 11th Conference on Intelligent Computer Mathematics. An error in Abstract has been fixed