X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Fmatita%2Fpapers.shtml;h=886a87271e47a734652882b4e974812ab41fe16c;hb=3cb42e0873c101c6c5a8b9967d765b5135882685;hp=694f7143b34825b9041cc803753563f43037b041;hpb=7c8b19607fe15a92603113275d016724db8f09c7;p=helm.git
diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
index 694f7143b..886a87271 100644
--- a/helm/www/matita/papers.shtml
+++ b/helm/www/matita/papers.shtml
@@ -1,3 +1,7 @@
+
+ [ Toggle abstracts ]
+
+
-
@@ -14,7 +18,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
@@ -38,7 +42,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
@@ -63,7 +67,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
@@ -93,7 +97,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
@@ -118,7 +122,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
@@ -149,7 +153,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
@@ -180,7 +184,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
@@ -209,7 +213,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