## 11.6 check: a general proof checker

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.

Page 383 of 800 |
| Search logiweb.eu |

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