[  lenny  ] [  squeeze  ] [  sid  ]
[ Source: matita  ]

Package: matita (0.5.8-2)

interactive theorem prover

Matita is a graphical interactive theorem prover based on the Calculus of (Co)Inductive Constructions.

Matita adopts XML-encoded proof objects are produced for storage and exchange. This makes it compatible, at some extent, with Coq.

The graphical interface has been inspired by CtCoq and Proof General. It supports high quality bidimensional rendering of proofs and formulae transformed on-the-fly to MathML markup

Tags: Field: Mathematics, Implemented in: OCaml, User Interface: Command Line, X Window System, Role: Program, Interface Toolkit: GTK, Purpose: Checking, X Window System: Application

Other Packages Related to matita

  • depends
  • recommends
  • suggests
  • dep: libatk1.0-0 (>= 1.20.0) [amd64, i386, powerpc, sparc]
    The ATK accessibility toolkit
  • dep: libc6 (>= 2.7) [amd64, i386, powerpc, sparc]
    GNU C Library: Shared libraries
    also a virtual package provided by libc6-udeb
  • dep: libcairo2 (>= 1.2.4) [amd64, i386, powerpc, sparc]
    The Cairo 2D vector graphics library
  • dep: libexpat1 (>= 1.95.8) [amd64, i386, powerpc, sparc]
    XML parsing C library - runtime library
  • dep: libfontconfig1 (>= 2.4.0) [amd64, i386, powerpc, sparc]
    generic font configuration library - runtime
  • dep: libfreetype6 (>= 2.2.1) [amd64, i386, powerpc, sparc]
    FreeType 2 font engine, shared library files
  • dep: libgdome2-0 [amd64, i386, powerpc, sparc]
    DOM level2 library for accessing XML files
  • dep: libgdome2-cpp-smart0c2a [amd64, i386, powerpc, sparc]
    C++ bindings for GDome2 DOM implementation
  • dep: libglade2-0 (>= 1:2.6.1) [amd64, i386, powerpc, sparc]
    library to load .glade files at runtime
  • dep: libglib2.0-0 (>= 2.16.0) [amd64, i386, powerpc, sparc]
    The GLib library of C routines
  • dep: libgtk2.0-0 (>= 2.12.0) [amd64, i386, powerpc, sparc]
    The GTK+ graphical user interface library
  • dep: libgtkmathview0c2a [amd64, i386, powerpc, sparc]
    rendering engine for MathML documents
  • dep: libgtksourceview2.0-0 (>= 2.7.2) [amd64, i386, powerpc, sparc]
    shared libraries for the GTK+ syntax highlighting widget
  • dep: libmysqlclient16 (>= 5.1.21-1) [i386, powerpc, sparc]
    MySQL database client library
    dep: libmysqlclient16 (>= 5.1.36) [amd64]
  • dep: libpango1.0-0 (>= 1.14.0) [amd64, i386, powerpc, sparc]
    Layout and rendering of internationalized text
  • dep: libpcre3 (>= 7.7) [amd64, i386, powerpc, sparc]
    Perl 5 Compatible Regular Expression Library - runtime files
  • dep: libsqlite3-0 (>= 3.6.20) [amd64, i386, powerpc, sparc]
    SQLite 3 shared library
  • dep: libt1-5 (>= 5.1.0) [amd64, i386, powerpc, sparc]
    Type 1 font rasterizer library - runtime
  • dep: libxml2 (>= 2.6.27) [amd64, i386, powerpc, sparc]
    GNOME XML library
  • dep: ocaml-base-nox-3.11.1 [not amd64, i386, powerpc, sparc]
    virtual package provided by ocaml-base-nox
  • dep: zlib1g (>= 1:1.1.4) [amd64, i386, powerpc, sparc]
    compression library - runtime
  • rec: graphviz
    rich set of graph drawing tools
  • rec: yelp
    Help browser for GNOME
  • sug: matita-doc
    user manual of the Matita interactive theorem prover

Download matita

Download for all available architectures
Architecture Package Size Installed Size Files
amd64 7,108.2 kB21236 kB [list of files]
armel 15,213.2 kB38232 kB [list of files]
hppa 15,213.1 kB38232 kB [list of files]
i386 4,934.8 kB14448 kB [list of files]
ia64 15,213.3 kB38232 kB [list of files]
mips 15,215.0 kB38232 kB [list of files]
mipsel 15,213.3 kB38232 kB [list of files]
powerpc 5,735.8 kB15508 kB [list of files]
s390 15,213.3 kB38232 kB [list of files]
sparc 5,807.4 kB15816 kB [list of files]