A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
Logic in Computer Science
2017-03-03 v9
Abstract
We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL's monadic interpreter to show that the underlying idea of PSL is transferable to other ITPs.
Keywords
Cite
@article{arxiv.1606.02941,
title = {A Proof Strategy Language and Proof Script Generation for Isabelle/HOL},
author = {Yutaka Nagashima and Ramana Kumar},
journal= {arXiv preprint arXiv:1606.02941},
year = {2017}
}
Comments
This paper has been submitted to CADE26