From 0692f9fb99211c02a93c72d58c9177f9f994e4d9 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 3 Apr 2012 08:35:11 +0000 Subject: [PATCH] prova --- helm/www/matita/matita.shtml | 79 ------------------------------------ 1 file changed, 79 deletions(-) diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 4c9e166c5..a68b48830 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -11,13 +11,6 @@
-
- Matita - - italian flag - -
-

Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the @@ -27,79 +20,7 @@ -

- - - Matita screenshot: authoring interface - - - - Matita is based on the - Calculus of (Co)Inductive Constructions, and is compatible, at some - extent, with Coq. - It is a reasonably small and simple application, whose - architectural and software complexity is meant to be mastered by - students, providing a tool particularly suited for testing innovative - ideas and solutions. - Matita adopts a tactic based editing mode; (XML-encoded) proof objects - are produced for storage and exchange. -

- -

- - - Matita screenshot: hyperlinks - - - Matita screenshot: direct manipulation - - - 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

- -

- - - Matita screenshot: library browsing - - - Matita screenshot: Whelp query - - - - - The knowledge base can be - browsed as an hypertext - (locally or on the World Wide Web) and - searched by means of - content-based queries;

- -

- - - Matita screenshot: tinycals - - - The tactical language, part of the proof language, has - step-by-step semantics, enabling inspection and replaying of deeply - structured proof scripts.

- -

Matita is partially supported by the following Projects:

- -
-- 2.39.2