--- /dev/null
+<Files ~ "Makefile|matita\.xcf|CVS.*">
+ Deny from all
+</Files>
--- /dev/null
+all:
+ dpkg-scanpackages -m . /dev/null | gzip > Packages.gz
+ dpkg-scansources . /dev/null | gzip > Sources.gz
--- /dev/null
+all:
+ dpkg-scanpackages -m . /dev/null | gzip > Packages.gz
+ dpkg-scansources . /dev/null | gzip > Sources.gz
--- /dev/null
+
+# should be a checked out version of sofware/matita/help/C/ (or a symlink to it)
+DOCS_SRC_DIR = docs-src
+DOCS_DEST_DIR = $(CURDIR)/docs/manual
+# should be a checked out and compiled with -execcomments of
+# sofware/matita/nlibrary/topology/igft.ma
+TUTORIAL_SRC_DIR = tutorial-src
+TUTORIAL_DEST_DIR = $(CURDIR)/docs/tutorial
+
+MARGIN_X=30
+MARGIN_Y=206
+SIZE_X=426
+SIZE_Y=70
+
+SEQ=3
+
+all:
+ @echo
+ @echo "Nothing to do per default, interesting targets:"
+ @echo
+ @echo " manual # import the (xhtml version of the) user manual"
+ @echo " tutorial # import the html version of the topology tutorial"
+ @echo " library # import the scripts building the library"
+ @echo " images # build images for the splash screen"
+ @echo " papers # build the papers page from xml/papers.xml"
+ @echo
+
+clean:
+
+manual: manual-stamp
+manual-stamp: $(DOCS_SRC_DIR)/*.xml $(DOCS_SRC_DIR)/xsl/*
+ $(MAKE) -C $(DOCS_SRC_DIR)/ html
+ rm -rf $(DOCS_DEST_DIR)/*
+ test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_DEST_DIR)/
+ $(MAKE) -C $(DOCS_SRC_DIR) install-html DESTDIR=$(DOCS_DEST_DIR)/
+ touch $@
+
+tutorial: tutorial-stamp
+tutorial-stamp: $(TUTORIAL_SRC_DIR)/igft.html
+ rm -rf $(TUTORIAL_DEST_DIR)/*
+ test -d $(TUTORIAL_DEST_DIR)/ || mkdir -p $(TUTORIAL_DEST_DIR)/
+ cp $(TUTORIAL_SRC_DIR)/igft.html $(TUTORIAL_DEST_DIR)/
+ cp $(TUTORIAL_SRC_DIR)/igft.pdf $(TUTORIAL_DEST_DIR)/
+ cp $(TUTORIAL_SRC_DIR)/*.png $(TUTORIAL_DEST_DIR)/
+ cp $(TUTORIAL_SRC_DIR)/*.svg $(TUTORIAL_DEST_DIR)/
+ cp $(TUTORIAL_SRC_DIR)/*.css $(TUTORIAL_DEST_DIR)/
+ cp $(TUTORIAL_SRC_DIR)/*.js $(TUTORIAL_DEST_DIR)/
+ touch $@
+
+.PHONY: library
+library:
+ if [ -d library/ ] ; then \
+ svn update library/ ; \
+ else \
+ echo "Can't find the scripts, check them out in library/" ; \
+ exit 1 ; \
+ fi
+
+papers: papers.shtml
+papers.shtml: xsl/papers2xhtml.xsl xml/papers.xml
+ xsltproc $^ > $@
+
+.PHONY: images
+images: images/matita.xcf
+ for Y in `seq 0 $(SEQ)`; do \
+ convert images/matita.png -crop \
+ $(SIZE_X)x$(SIZE_Y)+$(MARGIN_X)+`expr $(MARGIN_Y) + $$Y '*' '(' $(SIZE_Y) + 1 ')'` tmp.png; \
+ composite -compose src-over images/bg.png tmp.png images/bg$$Y.png;\
+ done;\
+ rm tmp.png
+
+clean:
+ rm -f manual-stamp
+dist-clean: clean
+ for X in `seq 0 $(SEQ)`; do\
+ rm images/bg$$X.png;\
+ done
+
--- /dev/null
+all:
+ dpkg-scanpackages -m . /dev/null | gzip > Packages.gz
+ dpkg-scansources . /dev/null | gzip > Sources.gz
--- /dev/null
+all:
+ dpkg-scanpackages -m . /dev/null | gzip > Packages.gz
+ dpkg-scansources . /dev/null | gzip > Sources.gz
--- /dev/null
+<!-- $Id$ -->
+<div class="bottombar">
+ <samp class="tiny">Last-modified: <!--#flastmod file="$DOCUMENT_NAME"--></samp>
+ <div class="uplined">
+ <a class="quiet" href="http://validator.w3.org/check/referer">
+ <img alt="Valid XHTML 1.0!" src="images/valid-xhtml10.png" width="88" height="31" /></a>
+ <a class="quiet" href="http://jigsaw.w3.org/css-validator/">
+ <img alt="Valid CSS" src="images/valid-css.png" width="88" height="31" />
+ </a>
+ </div>
+</div>
--- /dev/null
+div#page-index .intro
+{
+ width: 225px;
+ height: 225px;
+
+ margin-top: 2.3em;
+ margin-right: 2.3em;
+ float: right;
+
+ background: transparent no-repeat url(http://matita.cs.unibo.it/images/matita-medium.png);
+}
--- /dev/null
+#!/usr/bin/perl -w
+use strict;
+
+# Copyright (C) 2006, HELM Team.
+#
+# This file is part of HELM, an Hypertextual, Electronic
+# Library of Mathematics, developed at the Computer Science
+# Department, University of Bologna, Italy.
+#
+# HELM is free software; you can redistribute it and/or
+# modify it under the terms of the GNU General Public License
+# as published by the Free Software Foundation; either version 2
+# of the License, or (at your option) any later version.
+#
+# HELM is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with HELM; if not, write to the Free Software
+# Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+# MA 02111-1307, USA.
+#
+# For details, see the HELM World-Wide-Web page,
+# http://helm.cs.unibo.it/
+
+use CGI;
+use Syntax::Highlight::Universal;
+
+# Configuration
+
+my $documentroot = '/projects/matita/public_html/';
+my $protohrc = $documentroot . 'helm-proto.hrc';
+my $scriptsdir = $documentroot . 'library/';
+
+my %formatmap = (
+ '.ma' => 'grafite',
+ '.c' => 'c', # debug
+);
+
+# Code
+
+my $query = CGI->new; # used globally by some 'sub' below
+print $query->header(-type=>'text/html', -charset=>'utf-8');
+
+sub die_invalid_file() {
+ print $query->start_html;
+ print 'Invalid script.';
+ print $query->end_html;
+ exit 0;
+}
+
+sub lookup_script($) {
+ my ($f) = @_;
+ die_invalid_file() unless $f =~ /^(.*)(\.[^.]+)$/;
+ my $base = $1;
+ my $extension = $2;
+ die_invalid_file() unless $base =~ /[-a-zA-Z_]+(\/[-a-zA-Z_])*/;
+ die_invalid_file() unless exists $formatmap{$extension};
+ my $path = $scriptsdir . $f;
+ die_invalid_file() unless -f $path;
+ return ($path, $formatmap{$extension});
+}
+
+my $fname = $query->param('f');
+
+my $highlighter = Syntax::Highlight::Universal->new;
+$highlighter->addConfig($protohrc);
+
+my ($script, $format) = lookup_script($fname);
+open SCRIPT, "< $script" or die "Can't open Matita script \"$script\"\n";
+my @lines = <SCRIPT>;
+my $text = join '', @lines;
+close SCRIPT;
+
+print $query->start_html(-style=>{'src'=>"/$format-format.css"},
+ -encoding=>'utf-8');
+my $result = $highlighter->highlight($format, $text);
+print "<pre>\n";
+print $result;
+print "</pre>\n";
+print $query->end_html;
+
--- /dev/null
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>Matita - Community</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <div class="main">
+ <h1>Matita Community</h1>
+
+ <h2>Mailing lists</h2>
+ <p>
+ Discussions about Matita are held in the following mailing list
+ </p>
+ <a href="http://cs.unibo.it/cgi-bin/mailman/listinfo/matita">Matita mailing list</a>
+ <p>
+ The list is open to subscriptions for everyone, subscription is
+ required in order to post. <a href="http://www.cs.unibo.it/pipermail/matita/">Archives</a> of old posts are available.
+ </p>
+ <p>Here a link to the <a href="http://www.cs.unibo.it/cgi-bin/mailman/admin/matita/">administrative</a> interface</p>
+
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>Matita Developers</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <div class="main">
+
+ <h1>Matita Developers</h1>
+ <p>
+ The origins of Matita go back to 1999 and are intertwined with the
+ <a href="http://helm.cs.unibo.it">HELM Project</a>. Since then, a
+ lot of people contributed both ideas and source code that have made
+ Matita what it looks today. In this page we tried to summarize all
+ of them, we apologize for whom we forgot to mention.
+ </p>
+
+ <h2>People<a name="people"></a></h2>
+ <h3>Current team members</h3>
+ <ul class="wide">
+ <li><a href="http://www.cs.unibo.it/~asperti/">Andrea Asperti</a> - Full Professor</li>
+ <li><a href="http://www.cs.unibo.it/~fguidi/">Ferruccio Guidi</a> - PhD</li>
+ <li><a href="http://ricciott.web.cs.unibo.it/">Wilmer Ricciotti</a> - PhD Student </li>
+ <li><a href="http://www.cs.unibo.it/~sacerdot/">Claudio Sacerdoti Coen</a> - Lecturer </li>
+ <li><a href="http://www.cs.unibo.it/~tassi/">Enrico Tassi</a> - PhD </li>
+ </ul>
+
+ <h3>Former members</h3>
+ <ul class="wide">
+ <li><a href="http://www.cs.unibo.it/~zacchiro/">Stefano Zacchiroli</a> - PhD </li>
+ <li><a href="http://www.sti.uniurb.it/padovani/">Luca Padovani</a> - Lecturer</li>
+ <li><a href="http://www.cs.unibo.it/~schena/">Irene Schena</a> - PhD</li>
+ <li>Pietro Di Lena - Master Student</li>
+ <li>Michele Galatá - Master Student</li>
+ <li>Alberto Griggio - Master Student</li>
+ <li>Matteo Selmi - Master Student</li>
+ <li>Vincenzo Tamburrelli - Master Student</li>
+ </ul>
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>Matita - Documentation</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+<script type="text/javascript">
+ function toggleAbstracts() {
+ abstracts = document.getElementsByTagName("span");
+ len = abstracts.length;
+ for (i=0; i != len-1; i++) {
+ elt = abstracts.item(i);
+ if (elt.hasAttribute("class")) {
+ if (elt.getAttribute("class") == "paper_abstract") {
+ if (elt.style.display != "none") {
+ elt.style.display = "none";
+ } else {
+ elt.style.display = "inline";
+ }
+ }
+ }
+ }
+ }
+</script>
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <div class="main">
+ <h1>Matita Documentation</h1>
+
+ <h2>User Manual<a name="manual"></a></h2>
+
+ <p> The Matita User Manual is accessible from Matita itself via the
+ <a href="http://developer.gnome.org/arch/doc/help.html">GNOME Help
+ System</a>, just hit <kbd><F1></kbd> while running Matita and it
+ will be shown to you. </p>
+
+ <p> Alternatively you can browse it in
+ <!--<a href="http://www.w3.org/TR/xhtml1/">-->XHTML<!--</a>--> format:
+ </p>
+ <ul>
+ <li> <a href="docs/manual/html">Matita User Manual (XHTML format, multiple pages)</a>
+ </li>
+ </ul>
+
+ <p> The source code of the user manual (in <a
+ href="http://www.oasis-open.org/docbook/">DocBook</a> format) is
+ available from our repository, in the
+ <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fhelp%2FC%2F&rev=0&sc=0">matita/help/C/</a> folder. </p>
+
+ <h2>Tutorials<a name="tutorial"></a></h2>
+
+ <p>A not so short <a href="FILES/matita-tut.pdf">tutorial</a> by
+ A.Asperti, discussing some basic notions of number theory, for
+ the stable version of Matita.</p>
+
+ <p>A <a href="docs/tutorial/igft.html">tutorial</a> by E.Tassi based on
+ the formalization of the paper "Between formal topology and game theory:
+ an explicit solution for the conditions for an inductive generation of
+ formal topologies" by S.Berardi and S.Valentini. The tutorial describes
+ the ng version of Matita (not officially released yet, cohexisting with
+ the stable system in version 0.5.8). If some characters are not displayed
+ correctly (i.e. you are not using firefox) you may try the
+ <a href="docs/tutorial/igft.pdf">pdf version</a>.
+ </p>
+
+
+ <h2>Exercises<a name="exercises"></a></h2>
+
+ <p>Some commented <a href="FILES/matita-ex.pdf">exercises</a> given at the
+ <a href="http://typessummerschool07.cs.unibo.it">types summer school 2007</a>
+ by C.Sacerdoti and E.Tassi.
+ </p>
+
+ <h2>Publications</h2>
+ <!--#include virtual="papers.shtml" -->
+
+ <h2>Large Developments</h2>
+ <!--#include virtual="theses.shtml" -->
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>Matita - Download</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <div class="main">
+ <h1>Download Matita!</h1>
+
+ <h2>Releases<a name="releases"></a></h2>
+ <p>
+ The current version is 0.5.8, released on January 8, 2010. Here the
+ <a href="http://helm.cs.unibo.it/websvn/filedetails.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fdist%2FChangeLog&rev=0&sc=0">ChangeLog</a>.
+ </p>
+ <dl>
+ <dt>Live CD</dt>
+
+ <!--
+ <dd>Coming soon</dd>
+ -->
+ <dd>The <a href="FILES/matita-0.5.8.iso">live CD</a> (around 530
+ MB, md5sum:
+9a6912765eacaaa7f96d7d6d6b34add5
+ )
+ is the easiest way to try Matita. You can burn the CD image
+ and boot you computer from the CD, or install a free emulator like <a
+ href="http://virtualbox.org">virtualbox</a> and boot a virtual
+ machine from the CD image. Virtualbox is available for Mac OS X,
+ Windows and Linux. A short guide to VirtualBox is part of the
+ <a href="docs/manual/html">Matita manual</a><br/>
+ </dd>
+
+ <dt>.deb package</dt>
+
+ <dd>Matita is part of the <a
+ href="http://packages.debian.org/source/matita"> Debian archive</a>, you can
+ install it with the following command:<pre>aptitude install matita</pre>
+ </dd>
+
+ <dt>Sources</dt>
+
+ <dd>You can download the <a
+ href="FILES/matita-0.5.8.orig.tar.gz">sources</a> of Matita (around 6 MB, md5sum:
+125223d3dc522c4ac063a66f5d46df69
+ )
+ and
+ build it by yourself, following the <a
+ href="docs/manual/html/sec_install.html">installation instructions</a>.
+ The build process, due to the high number of external dependency is not
+ trivial, we thus suggest you to try the live CD or the .deb package
+ first.</dd>
+ </dl>
+
+ <h2>License<a name="license"></a></h2>
+ <p>
+ All our source code is released under the terms of the <a
+ href="http://www.gnu.org/licenses/gpl.html">GNU General Public
+ Licence</a> and is publically accessible on our <a
+ href="http://subversion.tigris.org">Subversion</a> repository.
+ </p>
+
+ <h2>Subversion repository<a name="repo"></a></h2>
+ <p>
+ You can <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2F&sc=0">browse our svn repository</a> directly on the web.
+ </p>
+
+ <h2>Nightly builds<a name="nightly"></a></h2>
+ <p>
+ A build of the Debian package is performed every night, and a live CD containing that version is also built.
+ You can <a href="FILES/matita-svnhead.iso">download this experimental live CD</a>, or add the Debian repository
+ to your apt configuration file:
+ </p>
+ <pre>
+ deb http://matita.cs.unibo.it/DEBIAN ./
+ deb-src http://matita.cs.unibo.it/DEBIAN ./
+ </pre>
+
+ <h2>Cluster .cs.unibo.it.<a name="clustercs"></a></h2>
+ <p>
+ The following repository contains the version of Matita installed
+ in the Ercolani laboratory, currently running Ubuntu Jaunty.
+ </p>
+ <pre>
+ deb http://matita.cs.unibo.it/CLUSTERCS ./
+ deb-src http://matita.cs.unibo.it/CLUSTERCS ./
+ </pre>
+ <p>
+ The same version is also available for Ubuntu Hardy (LTS)
+ </p>
+ <pre>
+ deb http://matita.cs.unibo.it/UBUNTU_HARDY ./
+ deb-src http://matita.cs.unibo.it/UBUNTU_HARDY ./
+ </pre>
+
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+/* color scheme similar to the colors we use in gtksourceview */
+
+.grafite_TheoremKinds {
+ color: #a52a2a;
+ font-weight: bold;
+}
+
+.grafite_Commands {
+ color: #a52a2a;
+ font-weight: bold;
+}
+
+.grafite_Tactics {
+ color: #008b8b;
+ /*font-style: italic;*/
+}
+
+.grafite_Macros {
+ color: #a020f0;
+}
+
+.grafite_Sorts {
+ color: #2e8b57;
+}
+
+.grafite_Operators {
+ color: #a020f0;
+}
+
+.grafite_String {
+ color: #ff00ff;
+}
+
+.grafite_Comment {
+ color: #0000ff;
+}
+
+.grafite_Symbols {
+ color: #a52a2a;
+ font-weight: bold;
+}
+
+/* color scheme from colorer's navy.css stylesheet */
+
+/*
+.grafite_TheoremKinds {
+ color: #7779bb;
+ font-weight: bold;
+}
+
+.grafite_Commands {
+ color: #200080;
+ font-weight: bold;
+}
+
+.grafite_Tactics {
+ color: #930000;
+ font-style: italic;
+}
+
+.grafite_Macros {
+ color: #004a43;
+}
+
+.grafite_Sorts {
+ color: #7779bb;
+}
+
+.grafite_Operators {
+ color: #44aadd;
+}
+
+.grafite_String {
+ color: #1060b6;
+}
+
+.grafite_Comment {
+ color: #595979;
+}
+
+.grafite_Symbols {
+ color: #406080;
+ font-weight: bold;
+}
+*/
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE hrc PUBLIC "-//Cail Lomecb//DTD Colorer HRC take5//EN"
+ "http://colorer.sf.net/2003/hrc.dtd">
+<hrc version="take5" xmlns="http://colorer.sf.net/2003/hrc"
+ xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+ xsi:schemaLocation="http://colorer.sf.net/2003/hrc http://colorer.sf.net/2003/hrc.xsd">
+
+ <type name="grafite">
+
+ <annotation>
+ <documentation>
+ Grafite: Matita scripts language
+ </documentation>
+ </annotation>
+
+ <region name="TheoremKinds" />
+ <region name="Commands" />
+ <region name="Tactics" />
+ <region name="Macros" />
+ <region name="Sorts" />
+ <region name="Operators" />
+ <region name="Symbols" />
+ <region name="Comment" />
+ <region name="String" />
+
+ <scheme name="grafite">
+
+ <keywords region="TheoremKinds" ignorecase="no">
+ <word name="theorem" />
+ <word name="definition" />
+ <word name="lemma" />
+ <word name="fact" />
+ <word name="remark" />
+ <word name="variant" />
+ </keywords>
+
+ <keywords region="Commands" ignorecase="no">
+ <word name="axiom" />
+ <word name="alias" />
+ <word name="and" />
+ <word name="as" />
+ <word name="coercion" />
+ <word name="coinductive" />
+ <word name="corec" />
+ <word name="default" />
+ <word name="for" />
+ <word name="include" />
+ <word name="include" />
+ <word name="inductive" />
+ <word name="in" />
+ <word name="interpretation" />
+ <word name="let" />
+ <word name="match" />
+ <word name="names" />
+ <word name="notation" />
+ <word name="on" />
+ <word name="qed" />
+ <word name="rec" />
+ <word name="record" />
+ <word name="return" />
+ <word name="to" />
+ <word name="using" />
+ <word name="with" />
+ </keywords>
+
+ <keywords region="Tactics" ignorecase="no">
+ <word name="absurd" />
+ <word name="apply" />
+ <word name="assumption" />
+ <word name="auto" />
+ <word name="paramodulation" />
+ <word name="clear" />
+ <word name="clearbody" />
+ <word name="change" />
+ <word name="constructor" />
+ <word name="contradiction" />
+ <word name="cut" />
+ <word name="decompose" />
+ <word name="discriminate" />
+ <word name="elim" />
+ <word name="elimType" />
+ <word name="exact" />
+ <word name="exists" />
+ <word name="fail" />
+ <word name="fold" />
+ <word name="fourier" />
+ <word name="fwd" />
+ <word name="generalize" />
+ <word name="goal" />
+ <word name="id" />
+ <word name="injection" />
+ <word name="intro" />
+ <word name="intros" />
+ <word name="inversion" />
+ <word name="lapply" />
+ <word name="linear" />
+ <word name="left" />
+ <word name="letin" />
+ <word name="normalize" />
+ <word name="reduce" />
+ <word name="reflexivity" />
+ <word name="replace" />
+ <word name="rewrite" />
+ <word name="ring" />
+ <word name="right" />
+ <word name="symmetry" />
+ <word name="simplify" />
+ <word name="split" />
+ <word name="to" />
+ <word name="transitivity" />
+ <word name="unfold" />
+ <word name="whd" />
+ </keywords>
+
+ <keywords region="Tactics" ignorecase="no">
+ <!-- tacticals -->
+ <word name="try" />
+ <word name="solve" />
+ <word name="do" />
+ <word name="repeat" />
+ <word name="first" />
+ <word name="focus" />
+ <word name="unfocus" />
+ </keywords>
+
+ <keywords region="Macros" ignorecase="no">
+ <word name="check" />
+ <word name="hint" />
+ <word name="set" />
+ </keywords>
+
+ <regexp match="/whelp\s+(elim|hint|instance|locate|match)/" region="Macros"/>
+
+ <keywords region="Sorts" ignorecase="no">
+ <word name="Set" />
+ <word name="Prop" />
+ <word name="Type" />
+ </keywords>
+
+ <keywords region="Operators" ignorecase="no">
+ <symb name="\def" />
+ <symb name="\forall" />
+ <symb name="\lambda" />
+ <symb name="\to" />
+ <symb name="\exists" />
+ <symb name="\Rightarrow" />
+ <symb name="\Assign" />
+ <symb name="\land" />
+ <symb name="\lor" />
+ <symb name="\lnot" />
+ <symb name="\liff" />
+ <symb name="\subst" />
+ <symb name="\vdash" />
+ <symb name="\iforall" />
+ <symb name="\iexists" />
+ </keywords>
+
+ <keywords region="Symbols" ignorecase="no">
+ <symb name="[" />
+ <symb name="]" />
+ <symb name="|" />
+ <symb name="{" />
+ <symb name="}" />
+ <symb name="@" />
+ <symb name="$" />
+ </keywords>
+
+ <regexp match="/".*?"/" region="String"/>
+
+ <block start="/\(\*/" end="/\*\)/" scheme="grafite-comment" region="Comment" />
+
+ </scheme>
+
+ <scheme name="grafite-comment">
+ <regexp match=".*" region="Comment" />
+ </scheme>
+
+ </type>
+</hrc>
--- /dev/null
+<?xml version="1.0" encoding='Windows-1251'?>
+<!DOCTYPE hrc PUBLIC "-//Cail Lomecb//DTD Colorer HRC take5//EN"
+ "http://colorer.sf.net/2003/hrc.dtd">
+<hrc version="take5" xmlns="http://colorer.sf.net/2003/hrc"
+ xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+ xsi:schemaLocation="http://colorer.sf.net/2003/hrc http://colorer.sf.net/2003/hrc.xsd">
+
+ <annotation>
+ <documentation>
+ This is a base HRC file with prototype defines and types linking information.
+ </documentation>
+ </annotation>
+
+ <!-- main languages -->
+ <prototype name="grafite" group="helm" description="Matita script language">
+ <location link="grafite.hrc" />
+ <filename>/\.ma$/i</filename>
+ </prototype>
+
+ <type name="default">
+ <scheme name="grafite" />
+ </type>
+
+</hrc>
--- /dev/null
+To generate miniatures:
+
+ for f in screenshot-* ; do convert -resize 100 $f MINI_$f ; done
+
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://web.resource.org/cc/"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ width="744.09448819"
+ height="1052.3622047"
+ id="svg1879"
+ sodipodi:version="0.32"
+ inkscape:version="0.44"
+ sodipodi:docbase="/home/zack"
+ sodipodi:docname="matitina-apache.svg">
+ <defs
+ id="defs1881" />
+ <sodipodi:namedview
+ id="base"
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1.0"
+ gridtolerance="10000"
+ guidetolerance="10"
+ objecttolerance="10"
+ inkscape:pageopacity="0.0"
+ inkscape:pageshadow="2"
+ inkscape:zoom="14.738889"
+ inkscape:cx="385.71429"
+ inkscape:cy="652.82322"
+ inkscape:document-units="px"
+ inkscape:current-layer="layer1"
+ inkscape:window-width="902"
+ inkscape:window-height="579"
+ inkscape:window-x="10"
+ inkscape:window-y="71" />
+ <metadata
+ id="metadata1884">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <g
+ inkscape:label="Layer 1"
+ inkscape:groupmode="layer"
+ id="layer1">
+ <g
+ transform="matrix(0.957434,0.288652,-0.288652,0.957434,376.8964,394.9313)"
+ style="fill:black;fill-rule:evenodd;stroke:none;stroke-width:0pt;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none"
+ id="g4"
+ inkscape:export-xdpi="260.08759"
+ inkscape:export-ydpi="260.08759">
+ <path
+ d="M 1.586,0.867 C 1.265,0.867 0.867,1.375 0.867,1.793 C 0.867,1.985 1.007,2.153 1.175,2.153 C 1.484,2.153 1.863,1.645 1.863,1.227 C 1.863,1.028 1.746,0.867 1.586,0.867 z M 2.293,0 C 2.293,0 0.808,0.25 0.808,0.25 C 0.808,0.25 0,1.606 0,1.606 C 0,1.606 0.41,3.141 0.41,3.141 C 0.41,3.141 4.734,5.739 4.734,5.739 C 4.871,5.821 5.082,5.879 5.261,5.879 C 5.261,5.879 8.019,5.879 8.019,5.879 C 8.261,5.879 8.379,5.801 8.379,5.641 C 8.379,5.578 8.371,5.551 8.308,5.442 C 8.308,5.442 6.886,2.942 6.886,2.942 C 6.777,2.742 6.726,2.692 6.566,2.602 C 6.566,2.602 6.464,2.543 6.464,2.543 C 6.464,2.543 2.293,0 2.293,0 z M 2.211,0.239 C 2.211,0.239 2.55,1.426 2.55,1.426 C 2.55,1.426 1.824,2.66 1.824,2.66 C 1.824,2.66 0.617,2.918 0.617,2.918 C 0.617,2.918 0.289,1.625 0.289,1.625 C 0.289,1.625 0.976,0.469 0.976,0.469 C 0.976,0.469 2.211,0.239 2.211,0.239 z M 7.562,4.614 C 7.781,4.942 7.781,4.953 7.781,5.043 C 7.781,5.16 7.632,5.41 7.504,5.532 C 7.433,5.602 7.293,5.641 7.144,5.641 C 7.144,5.641 5.34,5.641 5.34,5.641 C 6.277,5.012 6.675,4.325 6.754,3.239 C 6.754,3.239 7.562,4.614 7.562,4.614 z M 2.543,0.418 C 2.543,0.418 6.464,2.809 6.464,2.809 C 6.496,2.989 6.507,3.078 6.507,3.207 C 6.507,3.348 6.496,3.449 6.464,3.649 C 6.464,3.649 2.82,1.465 2.82,1.465 C 2.82,1.465 2.543,0.418 2.543,0.418 z M 2.699,1.664 C 2.699,1.664 6.379,3.887 6.379,3.887 C 6.336,4.157 5.98,4.754 5.75,4.934 C 5.75,4.934 2.074,2.699 2.074,2.699 C 2.074,2.699 2.699,1.664 2.699,1.664 z M 1.953,2.91 C 1.953,2.91 5.59,5.102 5.59,5.102 C 5.429,5.289 5.101,5.578 4.972,5.641 C 4.972,5.641 0.847,3.117 0.847,3.117 C 0.847,3.117 1.953,2.91 1.953,2.91 z "
+ id="path6" />
+ </g>
+ </g>
+</svg>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://web.resource.org/cc/"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ width="744.09448819"
+ height="1052.3622047"
+ id="svg1879"
+ sodipodi:version="0.32"
+ inkscape:version="0.44"
+ sodipodi:docbase="/home/zack"
+ sodipodi:docname="matitina.svg">
+ <defs
+ id="defs1881" />
+ <sodipodi:namedview
+ id="base"
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1.0"
+ gridtolerance="10000"
+ guidetolerance="10"
+ objecttolerance="10"
+ inkscape:pageopacity="0.0"
+ inkscape:pageshadow="2"
+ inkscape:zoom="14.738889"
+ inkscape:cx="385.71429"
+ inkscape:cy="652.85714"
+ inkscape:document-units="px"
+ inkscape:current-layer="layer1"
+ inkscape:window-width="902"
+ inkscape:window-height="579"
+ inkscape:window-x="10"
+ inkscape:window-y="71" />
+ <metadata
+ id="metadata1884">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <g
+ inkscape:label="Layer 1"
+ inkscape:groupmode="layer"
+ id="layer1">
+ <g
+ transform="translate(378.6676,403.7084)"
+ style="fill:black;fill-rule:evenodd;stroke:none;stroke-width:0pt;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none"
+ id="g4">
+ <path
+ d="M 1.586,0.867 C 1.265,0.867 0.867,1.375 0.867,1.793 C 0.867,1.985 1.007,2.153 1.175,2.153 C 1.484,2.153 1.863,1.645 1.863,1.227 C 1.863,1.028 1.746,0.867 1.586,0.867 z M 2.293,0 C 2.293,0 0.808,0.25 0.808,0.25 C 0.808,0.25 0,1.606 0,1.606 C 0,1.606 0.41,3.141 0.41,3.141 C 0.41,3.141 4.734,5.739 4.734,5.739 C 4.871,5.821 5.082,5.879 5.261,5.879 C 5.261,5.879 8.019,5.879 8.019,5.879 C 8.261,5.879 8.379,5.801 8.379,5.641 C 8.379,5.578 8.371,5.551 8.308,5.442 C 8.308,5.442 6.886,2.942 6.886,2.942 C 6.777,2.742 6.726,2.692 6.566,2.602 C 6.566,2.602 6.464,2.543 6.464,2.543 C 6.464,2.543 2.293,0 2.293,0 z M 2.211,0.239 C 2.211,0.239 2.55,1.426 2.55,1.426 C 2.55,1.426 1.824,2.66 1.824,2.66 C 1.824,2.66 0.617,2.918 0.617,2.918 C 0.617,2.918 0.289,1.625 0.289,1.625 C 0.289,1.625 0.976,0.469 0.976,0.469 C 0.976,0.469 2.211,0.239 2.211,0.239 z M 7.562,4.614 C 7.781,4.942 7.781,4.953 7.781,5.043 C 7.781,5.16 7.632,5.41 7.504,5.532 C 7.433,5.602 7.293,5.641 7.144,5.641 C 7.144,5.641 5.34,5.641 5.34,5.641 C 6.277,5.012 6.675,4.325 6.754,3.239 C 6.754,3.239 7.562,4.614 7.562,4.614 z M 2.543,0.418 C 2.543,0.418 6.464,2.809 6.464,2.809 C 6.496,2.989 6.507,3.078 6.507,3.207 C 6.507,3.348 6.496,3.449 6.464,3.649 C 6.464,3.649 2.82,1.465 2.82,1.465 C 2.82,1.465 2.543,0.418 2.543,0.418 z M 2.699,1.664 C 2.699,1.664 6.379,3.887 6.379,3.887 C 6.336,4.157 5.98,4.754 5.75,4.934 C 5.75,4.934 2.074,2.699 2.074,2.699 C 2.074,2.699 2.699,1.664 2.699,1.664 z M 1.953,2.91 C 1.953,2.91 5.59,5.102 5.59,5.102 C 5.429,5.289 5.101,5.578 4.972,5.641 C 4.972,5.641 0.847,3.117 0.847,3.117 C 0.847,3.117 1.953,2.91 1.953,2.91 z "
+ id="path6" />
+ </g>
+ </g>
+</svg>
--- /dev/null
+matita.shtml
\ No newline at end of file
--- /dev/null
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <title>Matita - Library</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <div class="main">
+ <h1>Matita Library</h1>
+
+ <h2>Scripts<a name="scripts"></a></h2>
+ <p>
+ The <a href="library/">scripts</a> used to generate the knowledge base of
+ Matita can be <a href="library/">browsed on line</a>.
+ </p>
+ <p>
+ The experimental <a href="nlibrary/">scripts</a> for the next major version of Matita can also be <a href="nlibrary/">browsed on line</a>.
+ </p>
+
+ <br/>
+
+ <h1>Large Developments</h1>
+
+ <h2>Certified Complexity (CerCo)<a name="cerco"></a></h2>
+ <p>Matita is being used to certify a cost preserving compiler from a
+ large subset of C into the 8051 machine code. The compiler does not
+ only produce the target code, but it also instruments the source code
+ with precise cost declarations for the execution of O(1) code
+ fragments. This induced cost model for the source language is
+ inherently non compositional since it is affected by the compilation
+ strategy: the same instructions are compiled in different ways in
+ different contexts, yielding different costs.
+ </p>
+ <p>The final aim of the CerCo project is to formally reason on
+ intensional properties on the C code -- e.g. to show that some hard
+ deadline is always met
+ -- and to be sure that the property holds also for the target code.
+ </p>
+ <p>The CerCo project is a FET Open IST project funded by the EU
+ community in the 7th Framework Programme. More informations on the
+ project and the code of the Matita formalization can be found
+ on the <a href="cerco.cs.unibo.it">CerCo Web site</a>
+ </p>
+
+ <h2>The Basic Picture<a name="sambin"></a></h2>
+ <p>
+ The <a href="library/formal_topology">scripts</a> present a formalization
+ of some results from the forthcoming book <a href="http://www.oup.com/us/catalog/general/subject/Mathematics/Logic/?view=usa&ci=9780199232888">The Basic Picture - Structures for Constructive Topology</a> by Giovanni Sambin.
+ </p>
+ <p>The formalization has been the result of a three years long
+ collaboration between mathematicians from the University of Padova
+ and computer scientists from the University of
+ Bologna, funded by the University of Padova. In particular,
+ the groups that collaborated are headed respectively by Prof. Sambin
+ in Padua (formal topology and constructive type theory)
+ and by Prof. Asperti in Bologna (constructive type theory and interactive
+ theorem proving).
+ </p>
+ <p>
+ In particular the <a href="library/formal_topology">scripts</a> present:
+ </p>
+ <ul>
+ <li>the category of Basic Pairs, that are generalizations of
+ topological spaces</li>
+ <li>the category of Basic Topologies, that are generalizations of
+ formal topologies</li>
+ <li>the existence of a categorical embedding of the former category
+ into the latter. The embedding is an improvement on the usual
+ adjunction between topological spaces and locales</li>
+ </ul>
+ <p>
+ All the results are presented constructively and in the predicative
+ fragment of Matita based on the minimalist type theory
+ by Maietti and Sambin, where choice axioms are not valid.
+ </p>
+ In order to reason comfortably on the previous concrete categories and
+ functors, we also present algebraic versions of all the introduced
+ notions, as well as categorical embedding of the concrete categories in
+ the algebrized ones. In particular we formalized:
+ </p>
+ <ul>
+ <li>the large category of Overlap Algebras, that extends locales with an
+ axiomatized (= algebraized) overlap binary predicate. The
+ concrete overlap predicate states positively
+ (i.e. without using negation) the existence (in the intuitionistic
+ sense) of a point in the intersection of two sets.
+ Morphisms of Overlap Algebras algebrize concrete relations between
+ sets by means of four functions that capture the
+ existential and universal pre and post images of a relation.
+ </li>
+ <li>the large category of O-Basic Pairs, that algebraize Basic
+ Pairs by means of Overlap Algebras</li>
+ <li>the large category of O-Basic Topologies, that algebraize Basic
+ Topologies by means of Overlap Algebras</li>
+ <li>the categorical embedding of Basic Pairs into O-Basic Pairs and
+ of Basic Topologies into O-Basic Topologies</li>
+ <li>the existence of a categorical embedding of the category
+ of O-Basic Pairs into the category of O-Basic Topologies</li>
+ </ul>
+ <p>
+ More information will be available in a forthcoming paper by
+ Claudio Sacerdoti Coen and Enrico Tassi to be
+ published in the Mathematical Structures in Computer Science journal.
+ </p>
+
+ <h2>Freescale<a name="freescale"></a></h2>
+ <p>
+ The <a href="freescale/">scripts</a> present:
+ </p>
+
+ <ul>
+ <li>an executable formalization of the operational semantics of
+ any <a href="http://www.freescale.com">Freescale</a>
+ micro-controller of the <a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?nodeId=0162468449&tid=FSH">HC05/HC08/RS08/HCS08 families</a>
+ </li>
+ <li>a compiler from assembly language (pseudocodes + operands) to
+ machine code</li>
+ <li>several automatic checks for unhandled opcodes, memory accesses,
+ correctness of ALU logic, etc.</li>
+ <li>three examples of assembly programs (string reverse, counting sort
+ and perfect numbers sieve) with sets of data to run them</li>
+ </ul>
+
+ <p>The execution in the executable formalization has been compared
+ to real world execution using the <a href="http://www.freescale.com/webapp/sps/site/overview.jsp?code=784_LPBBNEWTOOL&fsrch=1">USB SPYDER08</a>
+ in-circuit debugger.
+ </p>
+
+ <p>
+ The code (in <a href="http://caml.inria.fr">OCaml</a>)
+ of an executable <a href="freescale/freescale_ocaml">emulator</a>,
+ automatically generated from the scripts above. On the tests above,
+ it runs at about 29% of the speed of the
+ <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
+ emulation engine.
+ </p>
+
+ <p>The formalization has been the Undergraduate Thesis of
+ Mr. Cosimo Oliboni. The manuscript (italian only) can be found
+ <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
+ here</a>.
+ </p>
+
+ <h2>The Formal System λδ (lambda_delta)<a name="lambda_delta"></a></h2>
+
+ <p>The formal system λδ is a typed λ-calculus that
+ pursues the unification of terms, types, environments and contexts
+ as the main goal.
+ λδ takes some features from the Automath-related
+ λ-calculi and some from the pure type systems, but differs
+ from both in that it does not include the Π construction while it
+ provides for an abbreviation mechanism at the level of terms.
+ </p>
+
+ <p> The development presents the proofs of some important properties that
+ λδ enjoys. In particular:
+ <ul> <li> the confluence of reduction </li>
+ <li> the correctness of types </li>
+ <li> the uniqueness of types up to conversion </li>
+ <li> the subject reduction of the type assignment </li>
+ <li> the strong normalization of the typed terms </li>
+ <li> the decidability of type inference problem </li>
+ </ul>
+ </p>
+
+ <p>
+ See the <a href="http://lambda-delta.info/">λδ home page</a>
+ for more information.
+ </p>
+
+ <h1>Small Developments</h1>
+
+ <h2>Pointed regular expressions<a name="freescale"></a></h2>
+ <p>
+ The <a href="re/">script</a> present:
+ </p>
+
+ <ul>
+ <li>a formalization of the syntax and semantics of pointed regular
+ expressions, that are regular expressions where points are put
+ in front of atoms to describe where the next character recognized
+ by the expression should be. Multiple points represent the union
+ of multiple languages. A pointed regular expression corresponds
+ to a state of a regular automaton for the regular expression
+ obtained erasing all points.</li>
+ <li>a formalization of the construction of the automaton for a regular
+ expression by means of iterative computation of pointed regular
+ expressions.</li>
+ <li>a proof of correctness of the construction (to be completed)</li>
+ </ul>
+
+ <p>The development requires the SVN version of Matita to be executed.</p>
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <meta name="keywords" content="Matita, prover, assistant" />
+ <title>Matita - Home Page</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar.shtml" -->
+ <!--#include virtual="news.shtml" -->
+ <div class="main">
+
+ <div class="topimage">
+ <img src="images/matita-text-big.png" alt="Matita" />
+ <a href="matita_it.shtml">
+ <img src="flags/wit.gif" alt="italian flag" />
+ </a>
+ </div>
+
+ <p class="spaced">
+ Matita (that means <em>pencil</em> in italian) is an experimental,
+ interactive theorem prover under development at the
+ <a href="http://www.cs.unibo.it">Computer Science Department</a> of the
+ <a href="http://www.unibo.it">University of Bologna</a>.
+ </p>
+
+<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-matita.png">
+ <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
+ </a>
+ </span>
+
+ Matita is based on the
+ Calculus of (Co)Inductive Constructions, and is compatible, at some
+ extent, with <a href="http://coq.inria.fr">Coq</a>.
+ It is a reasonably small and simple application, whose
+ architectural and software complexity is meant to be mastered by
+ students, providing a tool particularly suited for testing innovative
+ ideas and solutions.
+ Matita adopts a tactic based editing mode; (XML-encoded) proof objects
+ are produced for storage and exchange.
+ </p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-matita-href.png">
+ <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
+ </a>
+ <a class="quiet" href="images/screenshot-matita-selection.png">
+ <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
+ </a>
+ </span>
+ The graphical interface has been inspired by CtCoq and
+ <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+ It supports high quality bidimensional rendering of
+ proofs and formulae transformed on-the-fly to
+ <a href="http://www.w3.org/Math/">MathML</a> markup</p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
+ <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
+ </a>
+ <a class="quiet" href="images/screenshot-cicbrowser-query.png">
+ <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
+ </a>
+ <!--
+ <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
+ <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
+ </a>
+ -->
+ </span>
+
+ The <a href="library.shtml">knowledge base</a> can be
+ <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+ (locally or on the World Wide Web) and
+ <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
+ content-based queries</a>; </p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-tinycals.png">
+ <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
+ </a>
+ </span>
+ The tactical language, part of the proof language, has
+ step-by-step semantics, enabling inspection and replaying of deeply
+ structured proof scripts. </p>
+
+ <p>Matita is partially supported by the following Projects: </p>
+ <ul>
+ <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
+ Types Project</a></li>
+ <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
+ <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
+ </ul>
+
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+<!-- $Id: matita.shtml 6610 2006-07-14 12:06:30Z zacchiro $ -->
+<!--#include virtual="xhtml-header.shtml" -->
+<html>
+ <head>
+ <meta name="keywords" content="Matita, prover, assistant" />
+ <title>Matita - Home Page Italiana</title>
+ <!--#include virtual="xhtml-meta.shtml" -->
+ </head>
+ <body>
+ <!--#include virtual="menubar_it.shtml" -->
+ <!--#include virtual="news_it.shtml" -->
+ <div class="main">
+
+ <div class="topimage">
+ <img src="images/matita-text-big.png" alt="Matita" />
+ <a href="matita.shtml">
+ <img src="flags/wgb.gif" alt="english flag" />
+ </a>
+ </div>
+
+ <p class="spaced">
+ Matita e' un tool sperimentale di supporto alla dimostrazione
+ interattiva di teoremi, in via di sviluppo al
+ <a href="http://www.cs.unibo.it">Dipartimento di Scienze
+ dell'Informazione</a> della
+ <a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
+ </p>
+
+<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-matita.png">
+ <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
+ </a>
+ </span>
+
+ Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed
+ parzialmente compatibile con l'analogo strumento francese
+ <a href="http://coq.inria.fr">Coq</a>.
+ Matita e' una applicazione ragionevolmente semplice e piccola,
+ la cui complessita' architetturale puo' essere
+ padroneggiata da laureandi, facendone uno strumento particolarmente
+ utile per la sperimentazione di nuove idee e soluzioni in ambito
+ universitario.
+ Matita adotta una filosofia di scrittura delle prove basata su
+ tattiche; lambda-termini di prova (codificati in XML) sono prodotti
+ per la memorizzazione di lungo periodo e lo scambio di dati
+ con altri sistemi.
+ </p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-matita-href.png">
+ <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
+ </a>
+ <a class="quiet" href="images/screenshot-matita-selection.png">
+ <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
+ </a>
+ </span>
+ L'interfaccia grafica e' stata ispirata da CtCoq e
+ <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+ Supporta una resa bidimensionale di alta qualita' delle espressioni
+ basata sul markup
+ <a href="http://www.w3.org/Math/">MathML</a>.</p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
+ <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
+ </a>
+ <a class="quiet" href="images/screenshot-cicbrowser-query.png">
+ <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
+ </a>
+ <!--
+ <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
+ <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
+ </a>
+ -->
+ </span>
+
+ La <a href="library.shtml">base di conoscenza matematica</a> puo'
+ essere
+ <a href="http://helm.cs.unibo.it/browse/">visitata</a> come un ipertesto
+ (localmente o sul World Wide Web) e si possono effettuare
+ <a href="http://helm.cs.unibo.it/whelp/">ricerche</a> basate su
+ interrogazioni contenutistiche; </p>
+
+ <p class="spaced">
+ <span class="screenshots">
+ <a class="quiet" href="images/screenshot-tinycals.png">
+ <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
+ </a>
+ </span>
+ Il linguaggio delle tattiche, parte del vernacolo di prova,
+ ha una semantica passo-passo che consente di ispezionare e
+ eseguire in modo non atomico anche scripts altamente strutturati.</p>
+
+ <p>Matita e' finanziato parzialmente dai seguenti progetti:
+ <ul>
+ <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
+ Types Project</a>
+ <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
+ <li><a href=http://dama.cs.unibo.it/>Dama</a></li>
+ </ul>
+ </p>
+ <!--#include virtual="bottombar.shtml" -->
+ </div>
+ </body>
+</html>
--- /dev/null
+<!-- $Id$ -->
+
+<div class="menu">
+ <a class="quiet" href="index.shtml">
+ <img src="images/matita-small.png" alt="Small Matita logo" />
+ </a>
+ <ul>
+ <li> <a href="index.shtml">Matita Home</a> </li>
+ <li> <a href="documentation.shtml">Documentation</a> </li>
+ <li>
+ <a style="background-image: url(images/matita-library.png)"
+ href="library.shtml">
+ Library
+ </a>
+ </li>
+ <li> <a href="development.shtml">Developers</a> </li>
+ <li> <a href="community.shtml">Community</a> </li>
+ <li> <a href="download.shtml">Download</a> </li>
+ </ul>
+</div>
+
--- /dev/null
+<!-- $Id: menubar.shtml 6484 2006-06-14 08:49:31Z zacchiro $ -->
+
+<div class="menu">
+ <a class="quiet" href="index.shtml">
+ <img src="images/matita-small.png" alt="Small Matita logo" />
+ </a>
+ <ul>
+ <li> <a href="matita_it.shtml">Matita Home</a> </li>
+ <li> <a href="documentation.shtml">Documentazione</a> </li>
+ <li>
+ <a style="background-image: url(images/matita-library.png)"
+ href="library.shtml">
+ Libreria
+ </a>
+ </li>
+ <li> <a href="development.shtml">Sviluppatori</a> </li>
+ <li> <a href="community.shtml">Comunita'</a> </li>
+ <li> <a href="download.shtml">Download</a> </li>
+ </ul>
+</div>
+
--- /dev/null
+/* Generated with hrd2css.pl from ./Colorer-take5.beta4/hrd/rgb/navy.hrd */
+
+.def_HorzCross {
+ color: #000000;
+ background-color: #e8e7f8;
+}
+
+.def_VertCross {
+ color: #000000;
+ background-color: #e1e0f2;
+}
+
+.def_Number {
+ color: #008c00;
+}
+
+.def_NumberDec {
+ color: #008c00;
+}
+
+.def_NumberHex {
+ color: #008000;
+}
+
+.def_NumberBin {
+ color: #005b00;
+}
+
+.def_NumberOct {
+ color: #008c00;
+}
+
+.def_NumberFloat {
+ color: #008000;
+}
+
+.def_NumberSuffix {
+ color: #006600;
+}
+
+.def_String {
+ color: #1060b6;
+}
+
+.def_StringContent {
+ color: #0f69ff;
+}
+
+.def_StringEdge {
+ color: #800000;
+}
+
+.def_CharacterContent {
+ color: #0000cc;
+}
+
+.def_Comment {
+ color: #595979;
+}
+
+.def_CommentContent {
+ color: #7F9FBF;
+ font-weight: bold;
+}
+
+.def_CommentEdge {
+ color: #606090;
+}
+
+.def_CommentDoc {
+ color: #3F7F8F;
+}
+
+.def_CommentDocEdge {
+ color: #c0bd92;
+}
+
+.def_Symbol {
+ color: #308080;
+}
+
+.def_SymbolStrong {
+ color: #406080;
+}
+
+.def_Prefix {
+ color: #0066ee;
+}
+
+.def_Operator {
+ color: #44aadd;
+}
+
+.def_Keyword {
+ color: #200080;
+ font-weight: bold;
+}
+
+.def_KeywordStrong {
+ color: #7779bb;
+ font-weight: bold;
+}
+
+.def_FunctionKeyword {
+ color: #400000;
+}
+
+.def_DeprecatedKeyword {
+ color: #008484;
+}
+
+.def_InterfaceKeyword {
+ color: #008484;
+}
+
+.def_ClassKeyword {
+ color: #6679aa;
+ font-weight: bold;
+}
+
+.def_StructKeyword {
+ color: #003060;
+}
+
+.def_TypeKeyword {
+ color: #7779bb;
+}
+
+.def_Register {
+ color: #000080;
+}
+
+.def_Constant {
+ color: #7d0045;
+}
+
+.def_Var {
+ color: #007d45;
+}
+
+.def_VarStrong {
+ color: #007997;
+}
+
+.def_Identifier {
+ color: #005fd2;
+}
+
+.def_BooleanConstant {
+ color: #0f4d75;
+}
+
+.def_Directive {
+ color: #004a43;
+}
+
+.def_Parameter {
+ color: #074726;
+}
+
+.def_ParameterUnknown {
+ color: #474796;
+}
+
+.def_Tag {
+ color: #333385;
+}
+
+.def_OpenTag {
+ color: #0057a6;
+}
+
+.def_CloseTag {
+ color: #0057a6;
+}
+
+.def_Label {
+ color: #e34adc;
+}
+
+.def_LabelStrong {
+ color: #000000;
+ background-color: #a8a800;
+}
+
+.def_Insertion {
+ color: #000000;
+ background-color: #cceeee;
+}
+
+.def_Error {
+ color: #ffffff;
+ background-color: #dd9999;
+ font-weight: bold;
+ font-style: italic;
+}
+
+.def_ErrorText {
+ color: #ee00ee;
+}
+
+.def_TODO {
+ color: #ffffff;
+ background-color: #808000;
+}
+
+.def_Debug {
+ color: #80abfd;
+ background-color: #007084;
+}
+
+.def_Path {
+ color: #40015a;
+}
+
+.def_URL {
+ color: #5555DD;
+}
+
+.def_EMail {
+ color: #7144c4;
+}
+
+.def_Date {
+ color: #009797;
+}
+
+.def_Time {
+ color: #8745a0;
+}
+
+.def_PairStart {
+ color: #d0d0ff;
+}
+
+.def_PairEnd {
+ color: #d0d0ff;
+}
+
+.def_PairStrongStart {
+ color: #880088;
+}
+
+.def_PairStrongEnd {
+ color: #880088;
+}
+
--- /dev/null
+<!-- $Id$ -->
+
+<div class="news">
+ <div class="newsheader">News</div>
+ <ul class="news">
+ <li><span class="date">8 January 2010</span><br />
+ Matita release 0.5.8 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">7 August 2009</span><br />
+ Matita-prover scores best new entry at the
+ <a href="http://www.cs.miami.edu/~tptp/CASC/22/">CADE ATP System Competition </a> (UEQ).
+ <li><span class="date">15 February 2009</span><br />
+ Matita release 0.5.7 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">1 December 2008</span><br />
+ Matita release 0.5.6 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">17 November 2008</span><br />
+ Matita release 0.5.5 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">19 October 2008</span><br />
+ Matita release 0.5.4 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">23 July 2008</span><br />
+ Matita release 0.5.3 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">2 July 2008</span><br />
+ Matita release 0.5.2 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">10 May 2008</span><br />
+ Matita release 0.5.0 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">18 Dec 2007</span><br />
+ Matita release candidate 0.4.98 available for <a href="download.shtml">download</a>.
+ </li>
+ <li><span class="date">18 Dec 2007</span><br />
+ Added a tutorial and some exercises to the <a href="documentation.shtml">documentation</a>
+ page.
+ </li>
+ <li><span class="date">20 Mar 2007</span><br />
+ A course on Matita at the
+ <a href="http://typessummerschool07.cs.unibo.it">Types Summer School 2007</a>.
+ </li>
+ <li><span class="date">24 Jan 2007</span><br />
+ Solution for the <a href="http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=Submitted_solutions">Poplmark challenge</a> (part 1a)
+ </li>
+ <li><span class="date">1 Dic 2006</span><br />
+ <a href="http://www.ciim26.unimore.it/comunicazioni.html">
+ Presentation</a> of Matita to the Italian Association for
+ Mathematics.
+ </li>
+ <li> <span class="date">21 Aug 2006</span><br />
+ Matita-prover on <a href="http://www.cs.miami.edu/~tptp">TPTP</a>.
+ </li>
+ <li> <span class="date">18 Jul 2006</span><br />
+ <a href="library/">the scripts</a> of the library are now
+ on-line
+ </li>
+ <li> <span class="date">14 Jun 2006</span><br />
+ <a href="community.shtml#lists">mailing lists</a> for Matita are now
+ available
+ </li>
+ </ul>
+</div>
+
--- /dev/null
+news.shtml
\ No newline at end of file
--- /dev/null
+<small>
+ <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+
+<ul>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Higher order proof reconstruction from paramodulation-based refutations:
+ the unit equality case
+ </span>
+ <a class="paper_download" href="PAPERS/hopr.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ In this paper we address the problem of reconstructing a
+ higher order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted equational
+ framework. The automatic procedure is based on superposition rules for
+ the unit equality case. Proof transformation techniques aimed to improve
+ the readability of the final proof are discussed.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Spurious Disambiguation Error Detection
+ </span>
+ <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ The disambiguation approach to the input of formulae enables the user to
+ type correct formulae in a terse syntax close to the usual ambiguous
+ mathematical notation. When it comes to incorrect formulae we want to
+ present only errors related to the interpretation meant by the user, hiding
+ errors related to other interpretations (spurious errors). We propose a
+ heuristic to recognize spurious errors, which has been integrated with our
+ former efficient disambiguation algorithm.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Crafting a Proof Assistant
+ </span>
+ <a class="paper_download" href="PAPERS/matita_types.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the Proceedings of Types 2006: Conference of
+ the Types Project. Nottingham, UK -- April 18-21, 2006.
+ </span>
+ <span class="paper_abstract">
+ Proof assistants are complex applications whose develop-
+ ment has never been properly systematized or documented. This work is
+ a contribution in this direction, based on our experience with the devel-
+ opment of Matita: a new interactive theorem prover based—as Coq—on
+ the Calculus of Inductive Constructions (CIC). In particular, we analyze
+ its architecture focusing on the dependencies of its components, how they
+ implement the main functionalities, and their degree of reusability.
+ The work is a first attempt to provide a ground for a more direct com-
+ parison between different systems and to highlight the common func-
+ tionalities, not only in view of reusability but also to encourage a more
+ systematic comparison of different softwares and architectural solutions.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ User Interaction with the Matita Proof Assistant
+ </span>
+ <a class="paper_download" href="PAPERS/matita.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in Journal of Automated Reasoning, Special Issue
+ on User Interfaces for Theorem Proving.
+ </span>
+ <span class="paper_abstract">
+ Matita is a new, document-centric, tactic-based interactive theorem
+ prover. This paper focuses on some of the distinctive features of the user interaction
+ with Matita, mostly characterized by the organization of the library as a search-
+ able knowledge base, the emphasis on a high-quality notational rendering, and the
+ complex interplay between syntax, presentation, and semantics.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Tinycals: step by step tacticals
+ </span>
+ <a class="paper_download" href="PAPERS/tinycals.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
+ WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
+ 142, ISSN:1571-0661
+ </span>
+ <span class="paper_abstract">
+ Most of the state-of-the-art proof assistants are based on procedural
+ proof languages, scripts, and rely on LCF tacticals as the primary tool
+ for tactics composition. In this paper we discuss how these ingredients
+ do not interact well with user interfaces based on the same interaction
+ paradigm of Proof General (the de facto standard in this field),
+ identifying in the coarse-grainedness of tactical evaluation the key
+ problem.
+
+ We propose tinycals as an alternative to a subset of LCF tacticals,
+ showing that the user does not experience the same problem if tacticals
+ are evaluated in a more fine-grained manner. We present the formal
+ operational semantics of tinycals as well as their implementation in the
+ Matita proof assistant.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
+ <span class="paper_title">
+ From notation to semantics: there and back again
+ </span>
+ <a class="paper_download" href="PAPERS/notation.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2006: The 5th
+ International Conference on Mathematical Knowledge Management.
+ Wokingham, UK -- August 11-12, 2006.
+ </span>
+ <span class="paper_abstract">
+ Mathematical notation is a structured, open, and ambiguous language. In
+ order to support mathematical notation in MKM applications one must
+ necessarily take into account presentational as well as semantic aspects.
+ The former are required to create a familiar, comfortable, and usable
+ interface to interact with. The latter are necessary in order to process
+ the information meaningfully. In this paper we investigate a framework
+ for dealing with mathematical notation in a meaningful, extensible way,
+ and we show an effective instantiation of its architecture to the field
+ of interactive theorem proving. The framework builds upon well-known
+ concepts and widely-used technologies and it can be easily adopted by
+ other MKM applications.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ A content based mathematical search engine: Whelp
+ </span>
+ <a class="paper_download" href="PAPERS/whelp.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
+ Paris, France -- December 15-18, 2004. LNCS 3839/2004, Springer-Verlag
+ Heidelberg, ISBN 3-540-31428-8, pp. 17-32
+ </span>
+ <span class="paper_abstract">
+ The prototype of a content based search engine for mathematical knowledge
+ supporting a small set of queries requiring matching and/or typing
+ operations is described. The prototype, called Whelp, exploits a metadata
+ approach for indexing the information that looks far more flexible than
+ traditional indexing techniques for structured expressions like
+ substitution, discrimination, or context trees. The prototype has been
+ instantiated to the standard library of the Coq proof assistant extended
+ with many user contributions.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Efficient Ambiguous Parsing of Mathematical Formulae
+ </span>
+ <a class="paper_download" href="PAPERS/disambiguation.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of MKM 2004
+ Third International Conference on Mathematical Knowledge Management.
+ September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
+ Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
+ </span>
+ <span class="paper_abstract">
+ Mathematical notation has the characteristic of being ambiguous:
+ operators can be overloaded and information that can be deduced is often
+ omitted. Mathematicians are used to this ambiguity and can easily
+ disambiguate a formula making use of the context and of their ability to
+ find the right interpretation.
+
+ Software applications that have to deal with formulae usually avoid these
+ issues by fixing an unambiguous input notation. This solution is annoying
+ for mathematicians because of the resulting tricky syntaxes and becomes a
+ show stopper to the simultaneous adoption of tools characterized by
+ different input languages.
+
+ In this paper we present an efficient algorithm suitable for ambiguous
+ parsing of mathematical formulae. The only requirement of the algorithm
+ is the existence of a validity predicate over abstract syntax trees of
+ incomplete formulae with placeholders. This requirement can be easily
+ fulfilled in the applicative area of interactive proof assistants, and in
+ several other areas of Mathematical Knowledge Management.
+ </span>
+ </li>
+
+</ul>
--- /dev/null
+<!-- $Id$ -->
+<!--#include virtual="xhtml-header.shtml" -->
+<html>
+ <head>
+ <title>Matita - Splash</title>
+ </head>
+ <style>
+ a {text-decoration:none}
+ img.invisible { display: none; }
+
+ dl#matitaMap {
+ margin-left:auto;
+ margin-right:auto;
+ margin-top:50px;
+ padding: 0;
+ background: url(images/matita.png) top left no-repeat;
+ height: 590px;
+ width: 485px;
+ position: relative;
+ }
+
+ dt{ margin: 0; padding: 0; position: absolute; font-size: 85%; display: none; }
+ dd{ margin: 0; padding: 0; position: absolute; font-size: 85%; }
+
+ dd#developersDef{ top: 206px; left: 30px; }
+ dd#developersDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
+ dd#developersDef a span{ display: none; }
+ dd#developersDef a:hover{ position: absolute; background: transparent url(images/bg0.png) ; top: 0px}
+
+ dd#documentationDef{ top: 277px; left: 30px; }
+ dd#documentationDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
+ dd#documentationDef a span{ display: none; }
+ dd#documentationDef a:hover{ position: absolute; background: transparent url(images/bg1.png) ; top: 0px}
+
+ dd#communityDef{ top: 348px; left: 30px; }
+ dd#communityDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
+ dd#communityDef a span{ display: none; }
+ dd#communityDef a:hover{ position: absolute; background: transparent url(images/bg2.png) ; top: 0px}
+
+ dd#downloadDef{ top: 419px; left: 30px; }
+ dd#downloadDef a{ position: absolute; width: 426px; height: 70px; text-decoration: none; }
+ dd#downloadDef a span{ display: none; }
+ dd#downloadDef a:hover{ position: absolute; background: transparent url(images/bg3.png) ; top: 0px}
+
+ div#ex {margin-left:auto; margin-right:auto}
+ </style>
+
+ <body>
+
+<div id="ex" >
+<img src="images/matita.png" width="485" height="590" border="0" class="invisible" />
+
+ <dl id="matitaMap">
+ <dt id="developers">1. Developers</dt>
+ <dd id="developersDef"><a href="development.shtml"></a></dd>
+ <dt id="documentation">2. Documentation</dt>
+ <dd id="documentationDef"><a href="documentation.shtml"></a></dd>
+ <dt id="community">3. Community</dt>
+ <dd id="communityDef"><a href="community.shtml"></a></dd>
+ <dt id="download">4. Download</dt>
+ <dd id="downloadDef"><a href="download.shtml"></a></dd>
+ </dl>
+ </div>
+
+ </body>
+</html>
--- /dev/null
+/*
+ * CSS stylesheet for the website http://matita.cs.unibo.it/
+ *
+ * $Id$
+ */
+
+/* page layout */
+
+div.menu {
+ position: absolute;
+ left: 0px;
+ width: 150px;
+ text-align: center;
+ font-size: 10pt;
+}
+
+div.main {
+ position: absolute;
+ top: 0px;
+ left: 150px;
+ width: 650px;
+ padding-left:20px;
+ font-size: 10pt;
+}
+
+div.news {
+ position: absolute;
+ top: 25px;
+ left: 845px;
+ font-size: 10pt;
+ width: 150px;
+ background: #eaeaea;
+ padding: 5px;
+ display: block;
+ height: 90%;
+ overflow: hidden;
+}
+
+/* site-wide typesetting */
+
+body {
+ font-family: sans-serif;
+ font-size: 12pt;
+ background-image: url(images/sheetbg.png);
+ background-repeat: repeat;
+}
+
+h1 {
+ font-size: 18pt;
+ color: #808080;
+
+ text-align: center;
+}
+
+h2 {
+ font-size: 16pt;
+ color: #808080;
+
+ border-bottom-style: solid;
+ border-width: 3px;
+ border-color: #cb8080;
+}
+
+h3 {
+ font-size: 14pt;
+ color: #808080;
+}
+
+h4 {
+ font-size: 13pt;
+ color: #808080;
+}
+
+a {
+ margin: 2px;
+ color: #591622;
+ text-decoration: underline;
+}
+
+a:hover {
+ text-decoration: underline;
+ background-color: #ecf6f9;
+}
+
+ul {
+ list-style-type: square;
+}
+
+p.spaced {
+ padding-bottom: 2em;
+}
+
+/* menu */
+
+div.menu ul {
+ list-style-type: none;
+ padding-left: 10px;
+ padding-right: 10px;
+}
+
+div.menu ul li {
+ color: #591622;
+ font-style : italic;
+ text-decoration : none;
+
+ border-bottom-style: solid;
+ border-color: #cb8080;
+ margin-bottom: 15px;
+}
+
+div.menu ul li a {
+ display: block;
+ text-align: right;
+ text-decoration: none;
+ vertical-align: middle;
+ height: 45px;
+ background-repeat: no-repeat;
+}
+
+a.menu:hover {
+ color: #591622;
+ text-decoration : none;
+ background-color: #ecf6f9;
+}
+
+/* news */
+
+div.news ul {
+ padding-left: 0px;
+ list-style: inside;
+}
+
+div.news span.date {
+ font-style: italic;
+}
+
+/* fancy classes */
+
+samp.tiny {
+ font-size: 8pt;
+}
+
+ul.wide li {
+ padding-bottom: 5px;
+}
+
+.center {
+ text-align: center;
+}
+
+div.topimage {
+ text-align: left;
+ padding-top: 28px;
+ padding-bottom: 28px;
+}
+
+div.bottombar {
+ display: block;
+ width: auto;
+ margin-top: 40px;
+}
+
+div.uplined {
+ height: auto;
+ padding-top: 10px;
+ width: 40%;
+ border-color: #cb8080;
+ border-top-style: solid;
+ border-top-width: 3px;
+}
+
+a.quiet:link,visited,hover {
+ background-color: transparent;
+ text-decoration: none;
+ border-style: none;
+}
+
+a.quiet img {
+ border-style:none;
+}
+
+span.screenshots {
+ float: right;
+}
+
+/* papers */
+
+li.paper {
+ padding-bottom: 5px;
+}
+
+span.paper_info {
+ display: block;
+}
+span.paper_abstract {
+ display: none;
+}
+span.paper_abstract:before {
+ content: "Abstract: ";
+ font-weight: bold;
+ font-style: normal;
+}
+span.paper_download {
+ display: block;
+ float: right;
+}
+a.paper_download { /* snipet from ikiwiki rss button, thanks! */
+ background: #ff6600;
+ color: white !important;
+ border-left: 0.5px solid #cc9966;
+ border-top: 1px solid #ccaa99;
+ border-right: 1px solid #993300;
+ border-bottom: 1px solid #331100;
+ padding: 0px 0.5em 0px 0.5em;
+ font-family: helvetica, arial, sans-serif;
+ font-size: 80%;
+ text-decoration: none;
+ margin-top: 1em;
+}
+
+span.paper_author {
+ font-style: italic;
+}
+
+span.paper_title {
+ font-weight: bold;
+}
+
+dt {
+ margin-top:1em;
+ font-weight: bold;
+}
+
+ul.news li {
+ margin-bottom: 1em;
+ list-style-type: none;
+}
+
+ul.news li span.date {
+ font-weight: bold;
+}
+
+div.news div.newsheader {
+ text-align: center;
+ margin-left:auto;
+ margin-right:auto;
+ font-weight: bold;
+}
--- /dev/null
+<!--
+<small>
+ <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+-->
+
+<ul>
+
+ <li class="paper">
+ <a name="freescale"/>
+ <span class="paper_author">
+ Cosimo Arndt Oliboni
+ </span><br/>
+ <span class="paper_title">
+ Matita come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva
+ dei Microcontroller a 8 bit Freescale
+ </span>
+ <a class="paper_download" href="PAPERS/oliboni.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Undergraduate thesis, University of Bologna, 2008.
+ </span>
+ <span class="XXXpaper_abstract">
+ We describe an executable formalization of the operational semantics of
+ every microcontroller of the Freescale 8-bit families (HC05, HC08, HCS08,
+ RS08). The formalization is done in Matita and heavily relies on dependent
+ types (for static checking) and executable exhaustive tests (to avoid
+ under-specification and specification errors). Real world programs have
+ been compiled to assembly (using CodeWarrior) and executed both with
+ the emulator formalized in Matita and its extracted OCaml version (for
+ performance reasons). All aspects of memory management and execution are
+ captured, up to the point of precisely characterizing the number of clock
+ cycles required by any single instruction. The manuscript is in Italian
+ only.
+ </span>
+ </li>
+
+</ul>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- $Id$ -->
+<?xml-stylesheet type="text/css" href="style.css" ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
--- /dev/null
+<!-- $Id$ -->
+ <link type="text/css" rel="stylesheet" href="style.css"/>
--- /dev/null
+<papers>
+ <!-- matita {{{ -->
+ <paper name="matita">
+ <authors>
+ <author>Andrea Asperti</author>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Enrico Tassi</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ The Matita Proof Assistant
+ </title>
+ <abstract>
+ Matita is a new document-centric proof assistant that integrates several
+ Mathematical Knowledge Management tools and techniques. In this paper we
+ describe the architecture of Matita and the peculiarities of its user
+ interface.
+ </abstract>
+ <info>
+ Submitted to <a href="http://www-unix.mcs.anl.gov/JAR/">Journal of
+ Automated Reasoning</a>, Special Issue on User Interfaces for Theorem
+ Proving
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- tinycals {{{ -->
+ <paper name="tinycals">
+ <authors>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Enrico Tassi</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ Tinycals: step by step tacticals
+ </title>
+ <abstract>
+ Most of the state-of-the-art proof assistants are based on procedural
+ proof languages, scripts, and rely on LCF tacticals as the primary tool
+ for tactics composition. In this paper we discuss how these ingredients
+ do not interact well with user interfaces based on the same interaction
+ paradigm of Proof General (the de facto standard in this field),
+ identifying in the coarse-grainedness of tactical evaluation the key
+ problem.
+
+ We propose tinycals as an alternative to a subset of LCF tacticals,
+ showing that the user does not experience the same problem if tacticals
+ are evaluated in a more fine-grained manner. We present the formal
+ operational semantics of tinycals as well as their implementation in the
+ Matita proof assistant.
+ </abstract>
+ <info>
+ Submitted to
+ <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP 2006</a>
+ User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006.
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- notation {{{ -->
+ <paper name="notation">
+ <authors>
+ <author>Luca Padovani</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ From notation to semantics: there and back again
+ </title>
+ <abstract>
+ Mathematical notation is a structured, open, and ambiguous language. In
+ order to support mathematical notation in MKM applications one must
+ necessarily take into account presentational as well as semantic aspects.
+ The former are required to create a familiar, comfortable, and usable
+ interface to interact with. The latter are necessary in order to process
+ the information meaningfully. In this paper we investigate a framework
+ for dealing with mathematical notation in a meaningful, extensible way,
+ and we show an effective instantiation of its architecture to the field
+ of interactive theorem proving. The framework builds upon well-known
+ concepts and widely-used technologies and it can be easily adopted by
+ other MKM applications.
+ </abstract>
+ <info>
+ Accepted for publication in the proceedings of
+ <a href="http://www.reading.ac.uk/MKM06/">MKM 2006</a>: The
+ 5th International Conference on Mathematical Knowledge Management.
+ Wokingham, UK -- August 11-12, 2006.
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- whelp {{{ -->
+ <paper name="whelp">
+ <authors>
+ <author>Andrea Asperti</author>
+ <author>Ferruccio Guidi</author>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Enrico Tassi</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ A content based mathematical search engine: Whelp
+ </title>
+ <abstract>
+ The prototype of a content based search engine for mathematical knowledge
+ supporting a small set of queries requiring matching and/or typing
+ operations is described. The prototype, called Whelp, exploits a metadata
+ approach for indexing the information that looks far more flexible than
+ traditional indexing techniques for structured expressions like
+ substitution, discrimination, or context trees. The prototype has been
+ instantiated to the standard library of the Coq proof assistant extended
+ with many user contributions.
+ </abstract>
+ <info>
+ In Proceedings of
+ <a href="http://types2004.lri.fr/">TYPES 2004 conference</a> Types for
+ Proofs and Programs. Paris, France -- December 15-18, 2004.
+ LNCS 3839/2004, Springer-Verlag Heidelberg, ISBN 3-540-31428-8, pp. 17-32
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- disambiguation {{{ -->
+ <paper name="disambiguation">
+ <authors>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ Efficient Ambiguous Parsing of Mathematical Formulae
+ </title>
+ <abstract>
+ Mathematical notation has the characteristic of being ambiguous:
+ operators can be overloaded and information that can be deduced is often
+ omitted. Mathematicians are used to this ambiguity and can easily
+ disambiguate a formula making use of the context and of their ability to
+ find the right interpretation.
+
+ Software applications that have to deal with formulae usually avoid these
+ issues by fixing an unambiguous input notation. This solution is annoying
+ for mathematicians because of the resulting tricky syntaxes and becomes a
+ show stopper to the simultaneous adoption of tools characterized by
+ different input languages.
+
+ In this paper we present an efficient algorithm suitable for ambiguous
+ parsing of mathematical formulae. The only requirement of the algorithm
+ is the existence of a validity predicate over abstract syntax trees of
+ incomplete formulae with placeholders. This requirement can be easily
+ fulfilled in the applicative area of interactive proof assistants, and in
+ several other areas of Mathematical Knowledge Management.
+ </abstract>
+ <info>
+ In Proceedings of <a href="http://mizar.uwb.edu.pl/MKM2004/">MKM 2004</a>
+ Third International Conference on Mathematical Knowledge Management.
+ September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
+ Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
+ </info>
+ </paper>
+ <!-- }}} -->
+</papers>
+<!-- vim:set foldmethod=marker: -->
--- /dev/null
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+ <xsl:output omit-xml-declaration="yes" />
+
+ <xsl:template match="papers">
+ <ul>
+ <xsl:apply-templates />
+ </ul>
+ </xsl:template>
+
+ <xsl:template match="paper">
+ <li class="paper">
+ <xsl:apply-templates select="authors" />
+ <br />
+ <xsl:apply-templates select="title" />
+ <xsl:element name="a">
+ <xsl:attribute name="class">paper_download</xsl:attribute>
+ <xsl:attribute name="href">
+ <xsl:text>papers/</xsl:text>
+ <xsl:value-of select="@name" />
+ <xsl:text>.pdf</xsl:text>
+ </xsl:attribute>
+ <span class="pdf_logo">.pdf</span>
+ </xsl:element>
+ <xsl:element name="a">
+ <xsl:attribute name="class">paper_download</xsl:attribute>
+ <xsl:attribute name="href">
+ <xsl:text>papers/</xsl:text>
+ <xsl:value-of select="@name" />
+ <xsl:text>.ps</xsl:text>
+ </xsl:attribute>
+ <span class="ps_logo">.ps</span>
+ </xsl:element>
+ <br />
+ <xsl:apply-templates select="info" />
+ <br />
+ <xsl:apply-templates select="abstract" />
+ </li>
+ </xsl:template>
+
+ <xsl:template match="authors">
+ <span class="paper_author">
+ <xsl:for-each select="author">
+ <xsl:apply-templates />
+ <xsl:if test="position()!=last()">
+ <xsl:text>, </xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ </span>
+ </xsl:template>
+
+ <xsl:template match="title">
+ <span class="paper_title">
+ <xsl:apply-templates />
+ </span>
+ </xsl:template>
+
+ <xsl:template match="info">
+ <span class="paper_info">
+ <xsl:apply-templates />
+ </span>
+ </xsl:template>
+
+ <xsl:template match="abstract">
+ <span class="paper_abstract">
+ <xsl:apply-templates />
+ </span>
+ </xsl:template>
+
+</xsl:stylesheet>
projects / helm.git / commitdiff
