Logiweb(TM)

6.7.1 Compile a mathematical proof

Prev Up Next Page 87 of 800 Search internet


Earlier, you populated the foo directory with several .lgs files. Now compile check.lgs:

   > lgc check.lgs

You now have the Logiweb proof checker, i.e. the proof checker which comes with Logiweb. That proof checker is a general purpose proof checker. It allows you to define any axiomatic theory you like, and then it can verify your proofs against your theory.

If you reference the check page as first reference, then all proofs on your page will be checked by the Logiweb proof checker. To use it, you have to express you theories, lemmas, and proofs in the language of the Logiweb sequent calculus. That imposes no restrictions on your theories, lemmas, and proofs.

If you like the Logiweb proof checker, use it. If you don't, make your own. If you want to share your work, publish it on Logiweb.

Now compile Peano.lgs:

   > lgc Peano.lgs

You now have the theories of propositional calculus, first order predicate calculus, and Peano arithmetic expressed using the Logiweb sequent calculus. They can be used together with the Logiweb proof checker. The Peano page also proves a number of theorems and defines a couple of tactics. A tactic is a computer program which can generate proofs for you.

If you like the theories of propositional calculus, first order predicate calculus, and Peano arithmetic as defined on the Peano page, use them. If you don't, make your own. If you want to share your work, publish it on Logiweb.

The theories on the Peano page are classical in the sense that they can prove the law of excluded middle. You can make your own intuitionistic versions if you like.

Now compile multzero.lgs:

   > lgc multzero.lgs

Then view it:

   > firefox multzero/index.html &
   Click 'Main page'

Prev Up Next Page 87 of 800 Search logiweb.eu

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