The HELM Team and contributors<BR>
University of Bologna, Department of Computer Science<BR>
The HELM Team and contributors<BR>
University of Bologna, Department of Computer Science<BR>
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
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.