Skip to main content
This is a pre-production deployment of Warehouse. Changes made here affect the production instance of PyPI (pypi.python.org).
Help us improve Python packaging - Donate today!

Checks mathematical proofs written in TeX

Project Description

Mathematical proofs are sequences of steps which take expressions in a formal language which state something already known to another formal expression which becomes known as a result. Each step must be justified by a rule of inference. The notion of proof is sharpened when the set of inference rules is reduced to a small number. But the effect of such reduction on proofs is to make them cumbersome, like the computations of a Turing Machine. ProofCheck uses a really large rule set to make possible proofs which are not cumbersome. The default inference rule set currently contains over 1500 rules and is still growing.

Either TeX or LaTeX may be used. What is required in the way of document structure is that:

1. Each theorem must be labeled and numbered in number-dot-number style,

2. Each theorem and proof must be expressed in a language that ProofCheck can learn to parse, and

3. Proof steps must be numbered and annotated following ProofCheck syntax.

The work cycle is as follows:

  1. Edit the document using your preferred text editor:

    emacs article.tex

  2. TeX the document:

    tex article

  3. Parse the document:

    parse.py article

  4. Check a proof of, say theorem 1.23:

    check.py article 1.23

Errors at any stage of course send you back to the text editor.

Release History

Release History

This version
History Node

1.0

Download Files

Download Files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

File Name & Checksum SHA256 Checksum Help Version File Type Upload Date
proofcheck-1.0.tar.gz (149.5 kB) Copy SHA256 Checksum SHA256 Source Mar 7, 2012

Supported By

WebFaction WebFaction Technical Writing Elastic Elastic Search Pingdom Pingdom Monitoring Dyn Dyn DNS Sentry Sentry Error Logging CloudAMQP CloudAMQP RabbitMQ Heroku Heroku PaaS Kabu Creative Kabu Creative UX & Design Fastly Fastly CDN DigiCert DigiCert EV Certificate Rackspace Rackspace Cloud Servers DreamHost DreamHost Log Hosting