From: denes Date: Tue, 30 Jun 2009 12:07:20 +0000 (+0000) Subject: Corrected a few typos X-Git-Tag: make_still_working~3767 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e4dbb2c911e538fcb8c8260c7d3e2be1bcc5b1e;p=helm.git Corrected a few typos --- diff --git a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html index fbbf4c4bc..4ac62f499 100644 --- a/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html +++ b/helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html @@ -22,14 +22,14 @@ clauses.

Implementation

Matita is written in Objective Caml, a functional language similar to ML -developed at INRIA. The automatic prover partecipating to the CASC is +developed at INRIA. The automatic prover participating to the CASC is a module of 4000 lines, designed with simplicity and ease of integration in mind. -It uses the fuctor abstraction mechanism of the OCaml language to achieve +It uses the functor abstraction mechanism of the OCaml language to achieve a good degree of reusability (i.e. comparison over terms is an abstract notion, that can be instantiated with a reduction aware relation for higher order logics like the Calculus of Inductive Constructions on which Matita is based, or a simpler -alpha equivalence relation for the TPTP first order lnaguage). Matita is based -on the Curry-Howard Isomorphims, i.e. proofs are lambda-terms of the CIC calculus. +alpha equivalence relation for the TPTP first order language). Matita is based +on the Curry-Howard Isomorphism, i.e. proofs are lambda-terms of the CIC calculus. The automatic prover is thus able to produce a trace suitable for proof term reconstruction [HOPR].