11.6 check: a general proof checker

Prev Up Next Page 383 of 800 Search internet

The check page defines a proof checker which can verify proofs relative to arbitrary theories. The check page also defines a tactic engine which allows the user to define proof tactics. The tactic engine ultimately translates all proofs to the Logiweb sequent calculus. A numbered version of the check.lgs source text is here.

Also see the original, unnumbered lgs file, the main pdf, and the document root.

Prev Up Next Page 383 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05