A Formal Expression Language for Mathematics
Edmund Furse
The language FEL is presented as a language suitable for representing pure mathematics texts in a way that is both formal and expressive. FEL is formal in that it has a precise syntax and semantics. It is expressive in that it is straightforward to express existing mathematical texts in the language without needing large amounts of expansion. FEL is useful as a means of checking that proofs are correct, either by hand or by computer. It is claimed that FEL is sufficiently rich to encode most of pure mathematics, and examples are given of well known proofs in FEL.

Furse E., (1990), A formal expression language for mathematics, Technical Report no. CS-90-2, Department of Computer Studies, University of Glamorgan.

List of Papers