This page is designed to be (eventually) a full reference manual for the ghilbert proof verifier.

Ghilbert distinguishes between interfaces and modules and different commands are valid in interfaces or modules. Interfaces live in a .ghi file and proof module live in a .gh file. Interfaces contain axioms and statements to be proved; modules prove those statements. A lemma which is proven in a module but which is not likely to be useful in contexts other than the given proof should not be listed in any interface.

Anything from # to the end of the line is a comment (that is, it is ignored by Ghilbert).


Interfaces contain:



Some of the error messages you may encounter are:

Term freemap mismatch with verify context

This means that you are trying to export to a term, but the thing you are exporting does not agree with the term's freemap. See the discussion of freemaps under term above.

Definition dummy 'x' is not a proof dummy

The variable x appears in the term being defined and also in the conclusion or hypotheses. See the discussion under defthm above.

term xxx not known

This means that xxx is the first item in an expression, but it was not defined by term or defthm. One common cause of this error is writing, for example (p → q) instead of (→ p q).

term must be id, found (x y)

Similar to the previous error, but the first item in the expression is not even an identifier. For example, in ((→ p q)) (with too many parentheses), the term is (→ p q), not as intended.

External links

Other related systems, which may help you understand ghilbert (especially until this manual is a bit more complete) are:

Login to edit