Email Gateway (Aug 22 2022 at 14:41): Email Gateway (Aug 22 2022 at 14:41):From: Tobias Nipkow <nipkow@in.tum.de>
Proof Strategy Language
Yutaka Nagashima
Isabelle includes various automatic tools for finding proofs under certain
conditions. However, for each conjecture, knowing which automation to use, and
how to tweak its parameters, is currently labour intensive. We have developed a
language, PSL, designed to capture high level proof strategies. PSL offloads the
construction of human-readable fast-to-replay proof scripts to automatic search,
making use of search-time information about each conjecture. Our preliminary
evaluations show that PSL reduces the labour cost of interactive theorem
proving. This submission contains the implementation of PSL and an example
theory file, Example.thy, showing how to write poof strategies in PSL.
https://www.isa-afp.org/entries/Proof_Strategy_Language.shtml
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 08:19 UTC