The Formal Theory System
The Formal Theory System (FTS, for short) is a proof development software consisting of a simple and elegant
language, namely FTL (Formal Theory Language), for writing strictly formalized theories based on axioms,
inference rules, definitions, and theorems, and a generic automatic (mechanical) proof verifier, namely FTV
(Formal Theory Verifier), which is a computer program able to check the correctness of proofs written in this
language.
One of the major design goal of this theory system is to be user friendly and, at the same time, to make as
easy as possible the formalization of mathematical proofs.
It is to this aim that the Formal Theory Language is close enough to the easier and classical human
mathematical syntax and style, so that people can read and understand proof almost immediately, and it is
formal enough, so that proofs can automatically be checked by the Formal Theory Verifier using only a simple
algorithm based on matching and substitution.
Theories, written in an ordinary ASCII coding, are developed in a very natural way through an extended
Hilbert-style deduction system.
FTV will be implemented in the
Haskell programming language and distributed under the terms of the
University of Illinois / NCSA Open Source License.
The first version of this software is still under design.