From 0e4dbb2c911e538fcb8c8260c7d3e2be1bcc5b1e Mon Sep 17 00:00:00 2001 From: denes Date: Tue, 30 Jun 2009 12:07:20 +0000 Subject: [PATCH] Corrected a few typos --- .../binaries/matitaprover/SystemDescriptionMatita.html | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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]. -- 2.39.2