Ghilbert and Shullivan

Ghilbert is a project by Raph Levien with the ambitious goal of creating a proof system suitable for publishing mathematical proofs on the Web. Ghilbert defines a proof language supporting imported/exported proof interfaces and definitions, and provides a proof verifier implemented in Python.

Shullivan is a project by Dan Krejsa to implement the Ghilbert proof verifier in C and add some interactive and experimental features. A preliminary release (0.05) of Shullivan is available here. Shullivan was developed under linux, comes with a simple Makefile and should be an easy port to other *nix variants. It depends on the readline library.

A Ghilbert language specification is being actively developed. Further changes to Shullivan to make it consistent with the upcoming specification should appear "shortly".

Changes in Shullivan 0.05 Release:

Fixed some cases in which shul would die with an assertion failure (rather than print a nice error message and stay alive) when a statement or variable was introduced with the same name as an earlier introduced statement.
Terminology change: What I previously called 'mandatory variables', i.e. variables occurring in the conclusion of an assertion but not in its hypotheses, I now call 'wild variables', since my earlier usage of 'mandatory' did not agree with that in metamath.
Make a few messages more accurate and useful.

Changes in Shullivan 0.04 Release:

Added support for pretty-printing expressions and printing detailed results obtained during a proof
isave writes terms for defs in the history

Example: Sequent Calculus

Version 0.01 of an example implementation of the propositional part of Sequent Calculus in Ghilbert is available here. This includes an exported version of pax/prop.ghi proven from the sequent calculus.

Last modified: Fri Jan 19 18:57:41 PST 2007