From 29a6362af7185c72a146b50815ad1574225a027f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 10 Jun 2006 17:06:57 +0000 Subject: [PATCH] added support for displaying the list of papers related to matita in the documentation page (currently commented out) --- helm/www/matita/Makefile | 5 + helm/www/matita/style.css | 18 ++++ helm/www/matita/xml/papers.xml | 156 +++++++++++++++++++++++++++ helm/www/matita/xsl/papers2xhtml.xsl | 70 ++++++++++++ 4 files changed, 249 insertions(+) create mode 100644 helm/www/matita/xml/papers.xml create mode 100644 helm/www/matita/xsl/papers2xhtml.xsl diff --git a/helm/www/matita/Makefile b/helm/www/matita/Makefile index b0a56d902..0c73ec7f3 100644 --- a/helm/www/matita/Makefile +++ b/helm/www/matita/Makefile @@ -16,6 +16,7 @@ all: @echo @echo " manual # import the (xhtml version of the) user manual" @echo " images # build images for the splash screen" + @echo " papers # build the papers page from xml/papers.xml" @echo clean: @@ -28,6 +29,10 @@ manual-stamp: $(DOCS_SRC_DIR)/*.xml $(DOCS_SRC_DIR)/*.xsl cp $(DOCS_SRC_DIR)/*.html $(DOCS_SRC_DIR)/*.css $(DOCS_DEST_DIR)/ touch $@ +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 \ diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css index ef9fd1cb1..38ad69c8b 100644 --- a/helm/www/matita/style.css +++ b/helm/www/matita/style.css @@ -152,3 +152,21 @@ span.screenshots { float: right; } +/* papers */ + +li.paper { + padding-bottom: 5px; +} + +span.paper_abstract { + display: none; +} + +span.paper_author { + font-style: italic; +} + +span.paper_title { + font-weight: bold; +} + diff --git a/helm/www/matita/xml/papers.xml b/helm/www/matita/xml/papers.xml new file mode 100644 index 000000000..b85999761 --- /dev/null +++ b/helm/www/matita/xml/papers.xml @@ -0,0 +1,156 @@ + + + + + Andrea Asperti + Claudio Sacerdoti Coen + Enrico Tassi + Stefano Zacchiroli + + + The Matita Proof Assistant + + + 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. + + + Submitted to Journal of + Automated Reasoning, Special Issue on User Interfaces for Theorem + Proving + + + + + + + Claudio Sacerdoti Coen + Enrico Tassi + Stefano Zacchiroli + + + Tinycals: step by step tacticals + + + 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. + + + Submitted to + UITP 2006 + User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006. + + + + + + + Luca Padovani + Stefano Zacchiroli + + + From notation to semantics: there and back again + + + 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. + + + Accepted for publication in the proceedings of + MKM 2006: The + 5th International Conference on Mathematical Knowledge Management. + Wokingham, UK -- August 11-12, 2006. + + + + + + + Andrea Asperti + Ferruccio Guidi + Claudio Sacerdoti Coen + Enrico Tassi + Stefano Zacchiroli + + + A content based mathematical search engine: Whelp + + + 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. + + + 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 + + + + + + + Claudio Sacerdoti Coen + Stefano Zacchiroli + + + Efficient Ambiguous Parsing of Mathematical Formulae + + + 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. + + + 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 + + + + + diff --git a/helm/www/matita/xsl/papers2xhtml.xsl b/helm/www/matita/xsl/papers2xhtml.xsl new file mode 100644 index 000000000..f0f278c3e --- /dev/null +++ b/helm/www/matita/xsl/papers2xhtml.xsl @@ -0,0 +1,70 @@ + + + + + +
    + +
+ + + +
  • + +
    + + + paper_download + + papers/ + + .pdf + + + + + paper_download + + papers/ + + .ps + + + +
    + +
    + +
    • +     + + + + + + + , + + + + + + + + + + + + + + + + + + + + + + + +     -- 2.39.2