Mizarインスパイア系
- the system Declare by D. Syme
?? 不明 - the Mizar mode for HOL by J.Harrison
http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html - the Isar language for Isabelle by M. Wenzel
http://isabelle.in.tum.de/Isar/ - Mizar-light for HOLlight by F. Wiedijk
ダウンロード注意! https://www.cs.ru.nl/~freek/mizar/miz.ps.gz
http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf
- the declarative proof language (DPL) for Coq by P. Corbineau
http://www-verimag.imag.fr/~corbinea/ftp/publis/types08.pdf - the notion of 'formal proof sketches' developed by F. Wiedijk
https://www.cs.ru.nl/~freek/pubs/sketches2.pdf