Page 383 of 800
| 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 |