This is the home page of Marcel, a system for computer-assisted reasoning in a sequent calculus equivalent to Jensen's set theory NFU (the version of Quine's New Foundations which allows urelements).
Don't be scared by the mention of set theory: the current applications of Marcel are mostly educational in the areas of propositional and first-order logic: some work has been done at the level of elementary real analysis which involves algebraic calculations and a little bit of set theory (at a level where which set theory is in use is not an issue).
We are grateful to Marcel Crabbé, who has graciously agreed to serve as godfather to the prover "as long as he doesn't have to give it any presents" (so I don't have to come up with a new name!). The details of the sequent calculus used here come from his paper on a semantic proof of cut-elimination for New Foundations without any axiom of extensionality.
The source file for Marcel is here. This has been updated Dec 15 2010 to the version of Jan 30 2010. The logic of this version is different from that which was used to run the Guild files, source for which is preserved in the Guild directory.
Marcel is written in Moscow ML, an implementation of Standard ML which is free to download through the link given.
Here is the manual, which does include a command reference. This is the version of December 15, 2010.
Here is the final draft of Joanna Guild’s thesis (included by permission, to be replaced by the final version when this comes out of the Graduate Office).
Here is my own current implementation project, a development of Edmund Landau's classic Foundations of Analysis (in progress). This has been updated June 22 (and needs June 22 prover version to run correctly). The Automath group also implemented this book.
Here are some theorems of set theory (details of New Foundations might be or become relevant in this file). This file was extensively affected by the June 22 prover update: this is a new version which works with that update.
Here is the file with the axioms for Joanna Guild's development of elementary real analysis (this is not her file, but an adaptation of that file to the current prover version; also, this file has errors in it, but if you page through it you will get the axioms). See the following link for the full development.
Here is the directory with the files for Joanna Guild's Master's thesis project. This contains a proof of the theorem that every positive real number has a square root from the axioms of an ordered field. Unfortunately, the initial portions of this work were done under an old version of the prover and the resulting proofs have to be ported forward to the new version in the complicated way described in the "read me" file in the directory.
Here find a directory with files under construction by Nathan Bailey, a student who did a presentation on Marcel for the Undergraduate Research Conference at BSU in spring 2007. He is currently proving theorems from Ross's real analysis book (the Math 314 text).