10.4 check.lgs: a general proof checker

Prev Up Next Page 371 of 800 Search internet

The check page defines a proof checker which can verify proofs relative to arbitrary, user define 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.

Prev Up Next Page 371 of 800 Search logiweb.eu

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