Package: matita (0.5.8-2 and others)

[ Source: matita  ]

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

• dep: libatk1.0-0 (>= 1.20.0) [not armel, ia64, mips, mipsel, s390]

  The ATK accessibility toolkit

• dep: libc0.1 (>= 2.7) [kfreebsd-amd64, kfreebsd-i386]

  Embedded GNU C Library: Shared libraries
  also a virtual package provided by libc0.1-udeb

• dep: libc6 (>= 2.7) [amd64, i386, powerpc, sparc]

  Embedded GNU C Library: Shared libraries
  also a virtual package provided by libc6-udeb

• dep: libcairo2 (>= 1.2.4) [not armel, ia64, mips, mipsel, s390]

  The Cairo 2D vector graphics library

• dep: libexpat1 (>= 1.95.8) [not armel, ia64, mips, mipsel, s390]

  XML parsing C library - runtime library

• dep: libfontconfig1 (>= 2.8.0) [not armel, ia64, mips, mipsel, s390]

  generic font configuration library - runtime

• dep: libfreetype6 (>= 2.2.1) [not armel, ia64, mips, mipsel, s390]

  FreeType 2 font engine, shared library files

• dep: libgdome2-0 [not armel, ia64, mips, mipsel, s390]

  DOM level2 library for accessing XML files

• dep: libgdome2-cpp-smart0c2a [not armel, ia64, mips, mipsel, s390]

  C++ bindings for GDome2 DOM implementation

• dep: libglade2-0 (>= 1:2.6.1) [not armel, ia64, mips, mipsel, s390]

  library to load .glade files at runtime

• dep: libglib2.0-0 (>= 2.16.0) [not armel, ia64, mips, mipsel, s390]

  The GLib library of C routines

• dep: libgtk2.0-0 (>= 2.12.0) [not armel, ia64, mips, mipsel, s390]

  The GTK+ graphical user interface library

• dep: libgtkmathview0c2a [not armel, ia64, mips, mipsel, s390]

  rendering engine for MathML documents

• dep: libgtksourceview2.0-0 (>= 2.7.2) [not armel, ia64, mips, mipsel, s390]

  shared libraries for the GTK+ syntax highlighting widget

• dep: libmysqlclient16 (>= 5.1.21-1) [not armel, ia64, mips, mipsel, s390]

  MySQL database client library

• dep: libpango1.0-0 (>= 1.14.0) [not armel, ia64, mips, mipsel, s390]

  Layout and rendering of internationalized text

• dep: libpcre3 (>= 7.7) [not armel, ia64, mips, mipsel, s390]

  Perl 5 Compatible Regular Expression Library - runtime files

• dep: libsqlite3-0 (>= 3.6.22) [not armel, ia64, mips, mipsel, s390]

  SQLite 3 shared library

• dep: libt1-5 (>= 5.1.0) [not armel, ia64, mips, mipsel, s390]

  Type 1 font rasterizer library - runtime

• dep: libxml2 (>= 2.6.27) [not armel, ia64, mips, mipsel, s390]

  GNOME XML library

• dep: ocaml-base-nox-3.11.2 [armel, ia64, mips, mipsel, s390]

  virtual package provided by ocaml-base-nox

• dep: zlib1g (>= 1:1.1.4) [not armel, ia64, mips, mipsel, s390]

  压缩库 - 运行时

• 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	Version	Package Size	Installed Size	Files
amd64	0.5.8-2+b1	5,950.1 kB	18,996.0 kB	[list of files]
armel	0.5.8-2+b2	15,217.0 kB	38,240.0 kB	[list of files]
i386	0.5.8-2+b1	4,938.4 kB	14,448.0 kB	[list of files]
ia64	0.5.8-2+b2	15,218.0 kB	40,352.0 kB	[list of files]
kfreebsd-amd64	0.5.8-2+b1	5,948.4 kB	18,828.0 kB	[list of files]
kfreebsd-i386	0.5.8-2+b1	4,937.9 kB	14,092.0 kB	[list of files]
mips	0.5.8-2+b2	15,218.1 kB	38,240.0 kB	[list of files]
mipsel	0.5.8-2+b2	15,217.0 kB	38,240.0 kB	[list of files]
powerpc	0.5.8-2+b1	5,732.0 kB	15,496.0 kB	[list of files]
s390	0.5.8-2+b2	15,217.0 kB	38,240.0 kB	[list of files]
sparc	0.5.8-2+b1	5,815.8 kB	15,828.0 kB	[list of files]