helm/software/components/binaries/matitaprover/SystemDescriptionMatita.html

   1 <HR><!------------------------------------------------------------------------>
   2 <H2>Matita (prover) 1.0.0</H2>
   3 The HELM Team and contributors<BR>
   4 University of Bologna, Department of Computer Science<BR>
   5
   6 <H3>Architecture</H3>
   7
   8 Matita (v. 0.5.7) is an Interactive Theorem Prover comprising
   9 a fully automatic module (prover) for problems falling in
  10 the first order unit equality case.
  11
  12 <P>
  13 An overall description of the system and its architecture can be found
  14 in [UIMPA], but there is no paper devoted to the automatic prover built
  15 in the system.
  16
  17 <H3>Strategies</H3>
  18
  19 The prover is based on standard superposition calculus for unit equality
  20 clauses.
  21
  22 <H3>Implementation</H3>
  23
  24 Matita is written in Objective Caml, a functional language similar to ML
  25 developed at INRIA. The automatic prover participating to the CASC is
  26 a module of 4000 lines, designed with simplicity and ease of integration in mind.
  27 It uses the functor abstraction mechanism of the OCaml language to achieve
  28 a good degree of reusability (i.e. comparison over terms is an abstract notion,
  29 that can be instantiated with a reduction aware relation for higher order logics
  30 like the Calculus of Inductive Constructions on which Matita is based, or a simpler
  31 alpha equivalence relation for the TPTP first order language). Matita is based
  32 on the Curry-Howard Isomorphism, i.e. proofs are lambda-terms of the CIC calculus.
  33 The automatic prover is thus able to produce a trace suitable for proof term
  34 reconstruction [HOPR].
  35
  36 The ATP system registered to the CASC competition will be part
  37 of the upcoming 1.0 release of the Matita interactive theorem prover, and
  38 is thus not part of any officially released versions, but can be downloaded
  39 using the SVN repository.
  40 <PRE>
  41     <A HREF="http://matita.cs.unibo.it">http://matita.cs.unibo.it</A></PRE>
  42
  43 <H3>Expected Competition Performance</H3>
  44
  45 Since the system never participated to the CASC, there is no
  46 real expectation, but we hope not to finish last ;-)
  47
  48 <H3>References</H3>
  49 <DL>
  50
  51 <DT> UIMPA
  52 <DD> Asperti, Sacerdoti Coen, Tassi, Zacchiroli. 2007
  53      <STRONG>User Interaction with the Matita Proof Assistant</STRONG>,
  54      <EM>Journal of Automated Reasoning</EM>
  55      Special Issue  on User Interfaces for Theorem Proving
  56      pp. 109-139
  57      Springer Netherlands
  58 <DT> HOPR
  59 <DD> Asperti, Tassi. 2007
  60      <STRONG> Higher order proof reconstruction from paramodulation-based refutations:
  61               the unit equality case</STRONG>,
  62      <EM> MKM 2007: The 6th International Conference on Mathematical Knowledge Management</EM>,
  63      LNAI, Springer
  64 </DL>
  65 <P>
  66
  67 <HR><!------------------------------------------------------------------------>