News

1. Introduction

MathNat (Mathematical texts in Controlled Natural language) is a project for developing tools to enable automatic formalisation of mathematical text. We proceed in three steps as followed:

  1. Syntax: we develop a controlled language for mathematical text, mainly proofs by using a type theoretic approach. This is a subset of natural language.
  2. Semantics: we translate this controlled language to an abstract mathematical language (MathAbs). MathAbs is a system independent formal language for writing mathematics. we also solve some basic anaphora in this step.
  3. Proof checking: Translation of MathAbs into a prover specific formalism. It is a future work. We plan to do it by providing a good API to interface with proof assistants and automated theorem provers.

Here is a small introductory presentation.

2. Thesis homepage

3. Publications

4. Talks, Posters, Demos

5. Download and Install

The source package of MathNat: mathnat version 1.0 (release date: 12 October 2011).

To setup MathNat, you need following softwares:

  1. Haskell Platform 2010.2.0.1 or newer (homepage)
  2. The BNF Converter (homepage)
  3. The Grammatical Framework (GF-3.3) (homepage)

5.1. Haskell Platform

Haskell Platform is required to compile GF as well as MathNat. Instructions for installing Haskell Platform are given on its homepage. I give below tailored instructions partially taken from GF install page. On Linux distribution, it can be installed as: 

   sudo apt-get install haskell-platform (Debian/Ubuntu)
   sudo yum install haskell-platform (Fedora)

For GF, you need some C libraries: 

   sudo apt-get install libghc6-terminfo-dev (Debian/Ubuntu)
   sudo yum install ghc-terminfo-devel (Fedora)

cabal program should be installed with the Haskell Platform. You need to update it with command: 

   sudo cabal update

If the program cabal asks for an upgrade, then follow its instructions. Most probably, it will ask you to run the following command: 

   sudo cabal install --global cabal-install

Other ways of installing the Haskell platform can be found on Haskell homepage.

5.2. The BNF Converter

The BNF Converter (bnfc) is available on hackage. Therefore, it could be installed with cabal. 

   sudo cabal install --global bnfc

Alternatively, install it directly from the distribution: 

   sudo apt-get install bnfc (Debian/Ubuntu)
   sudo yum install bnfc (Fedora)

5.3. The Grammatical Framework

The Grammatical Framework is also available on hackage. Therefore, it could be installed with cabal: 

   sudo cabal install --global gf

If you get errors regarding the conflicts in dependencies, you probably need to update some of the libraries of Haskell compiler (GHC). These libraries are usually available as "libghc6-library_name-dev" in your Linux distribution. For instance, if you get the error something like that: 

base-3.0.3.2 requires syb==0.1.0.2
.... requires json-05...

You need to update libraries: json, base, and syb. You may do it as shown below. To get the hints about the exact names of these libraries, press tab while typing the following command: 

   sudo apt-get install libghc6-base-dev libghc6-json-dev libghc6-syb-dev

Other ways can be found on GF homepage.

5.4. The System MathNat

Download the source package of MathNat: mathnat version 1.0 and uncompress it. Go to the directory mathnat and type make.

You can do these steps with the following commands: 

    wget http://www.lama.univ-savoie.fr/~humayoun/repos/mathnat-1.0.tar.gz (downloading mathnat)
    tar -zxvf mathnat-1.0.tar.gz                                           (uncompressing)
    cd mathnat
    make

5.5. Running an example in MathNat

Go to the directory mathnat and execute the following command: 

    ./mathnat examples/ex.nat

The output will be displayed on the console. You can save this output with the Unix command: 

    ./mathnat examples/ex.nat >examples/ex.nat.output

For stable examples, see mathnat/examples. For each example ex.nat, you'll find its output already stored in ex.nat.out.

For questions and queries, contact me by email: humayoun AT gmail DOT com.

Last update: Thu Jan 19 18:43:47 2012