From: Stefano Zacchiroli Date: Mon, 28 May 2007 09:22:25 +0000 (+0000) Subject: removed spurious br X-Git-Tag: make_still_working~6279 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=11e0af974ee0c386bbdbed90c307d190cefad64f;p=helm.git removed spurious br --- diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml index 5b95763db..2e67afd9a 100644 --- a/helm/www/matita/papers.shtml +++ b/helm/www/matita/papers.shtml @@ -36,7 +36,7 @@ Accepted for publication in the proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. -
+ In this paper we address the problem of reconstructing a higher order, checkable proof object starting from a proof trace left by a @@ -60,7 +60,7 @@ Accepted for publication in the proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. -
+
The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous @@ -85,7 +85,7 @@ Accepted for publication in the Proceedings of Types 2006: Conference of the Types Project. Nottingham, UK -- April 18-21, 2006. -
+
Proof assistants are complex applications whose develop- ment has never been properly systematized or documented. This work is @@ -115,7 +115,7 @@ Accepted for publication in Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving. -
+
Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction @@ -140,7 +140,7 @@ 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 -
+ 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 @@ -171,7 +171,7 @@ Accepted for publication in the proceedings of MKM 2006: The 5th International Conference on Mathematical Knowledge Management. Wokingham, UK -- August 11-12, 2006. -
+ Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must @@ -202,7 +202,7 @@ 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 -
+ The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing @@ -231,7 +231,7 @@ 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 -
+ Mathematical notation has the characteristic of being ambiguous: operators can be overloaded and information that can be deduced is often