|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|