Math Gate

Contact Person

Automated Reasoning in Higher Order Logic

Matracas Mathematics Related Software

Welcome to Math Gate

The purpose of the Math Gate site is to provide a link between formal (computer checkable) and informal (human readable) mathematics. Currently the main content of the site is an online book (DeTSeT) in which the foundations of mathematics are developed starting from some axioms of set theory. In the future I would like the site to evolve into a formal blog.

Updates

May 17, 2008 There is a Javascript translator from Jitpro syntax to LEO-II (thf) syntax that can also call the higher-order theorem prover LEO-II remotely. A collection of example problems is here.

May 12, 2008 Some exercises using Basil Smith's Elementary Theory of Relations in Jitpro and LEO-II.

April 19, 2008 I formulated conditions related to consistency of Quine's NF in Simptcheck notation. You can use Simptcheck to verify a solution (which would prove Quine's NF consistent) or to verify a proof that my approach to constructing a model of NF cannot work.

March 30, 2008 Added the proof checker simptcheck and checkable formal versions of the DeTSeT items.

Links

Scunak is an interactive theorem prover for set theory in a dependent type theory. It is written in Common Lisp.
Simptcheck is a simple checker for proof terms written in OCaml.