X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Fsec_intro.html;fp=matita%2Fmatita%2Fhelp%2FC%2Fhtml%2Fsec_intro.html;h=a967fff1ae0addc2485ca95a8d14d9cc4aca816a;hb=9d5a0d55e331b348d44b6d50d3d67e62b60a0e18;hp=0000000000000000000000000000000000000000;hpb=7b6ca76a0ed511b288b654729c9758277dbcd352;p=helm.git diff --git a/matita/matita/help/C/html/sec_intro.html b/matita/matita/help/C/html/sec_intro.html new file mode 100644 index 000000000..a967fff1a --- /dev/null +++ b/matita/matita/help/C/html/sec_intro.html @@ -0,0 +1,7 @@ + +Chapter 1. Introduction
Chapter 1. Introduction
Prev   Next

Chapter 1. Introduction

Table of Contents

Features
Matita vs Coq

Features

Matita is an interactive theorem prover + (or proof assistant) with the following characteristics:

  • It is based on a variant of the Calculus of (Co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.

  • It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.

  • It has a stand-alone graphical user interface (GUI) inspired by +CtCoq/Proof General. The GUI is implemented according to the state +of the art. In particular:

    • It is based and fully integrated with Gtk/Gnome.

    • An on-line help can be browsed via the Gnome documentation browser.

    • Mathematical formulae are rendered via Unicode.

  • It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.

Prev   Next
Matita V0.99.5 + User Manual (rev. 0.99.5 +) Home Matita vs Coq
\ No newline at end of file