### Abstract

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.

### License

BSD License

### Topics

- Tools

### Session Proof_Strategy_Language

- Try_Hard
- PSL
- Example

## Cite

×

Proof_Strategy_Language-AFP

    @article{Proof_Strategy_Language-AFP,
      author  = {Yutaka Nagashima},
      title   = {Proof Strategy Language},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Proof_Strategy_Language.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 21, 2016 : Isabelle2016-1