Program
Verification
Book

PV6 ⊧ Tinkerinteractive theorem prover with various backends

Application domain/field

Interactive theorem proving
Proof strategy language
Proof strategies

Type of tool

Meta-tool

Internals

Tinker implements PSGraph, a graphical proof strategy language. It supports the theorem provers Isabelle-HOL, ProofPower and Rodin.

Links

Project page: https://ggrov.github.io/tinker/
Repository: https://github.com/ggrov/tinker
- Last commit date: 05 Apr 2017 (default branch)
- Last commit date: 13 Sep 2017 (last activity)

Related papers

Developing and Debugging Proof Strategies by Tinkering (TACAS '16, presents Tinker2)
Tinker, tailor, solver, proof (EPTCS vol. 167, '14, presents Tinker)

Last publication date

9 April 2016

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.