Matita HomeMatita HomeThe system shares a common look&feel with the Coq proof assistant and its graphical user interface. The two systems have variants of the same logic, close proof languages and similar sets of tactics. From the user point of view the main lacking features with respect to Coq are:
proof extraction;
an extensible language of tactics;
automatic implicit arguments;
several ad-hoc decision procedures;
several rarely used variants for most of the tactics;
sections and local variables.
Still from the user point of view, the main differences with respect to Coq are:
the language of tacticals that allows execution of partial tactical application;
the unification of the concept of metavariable and existential variable;
terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;
ambiguous terms are disambiguated by direct interaction with the user;
theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.