X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fpapers.shtml;h=886a87271e47a734652882b4e974812ab41fe16c;hb=3cb42e0873c101c6c5a8b9967d765b5135882685;hp=9f5bbafaa563660c09a54a161d58c94a8284e88d;hpb=693e484d94573197108f51e3de4218492d9db3e2;p=helm.git
diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
index 9f5bbafaa..886a87271 100644
--- a/helm/www/matita/papers.shtml
+++ b/helm/www/matita/papers.shtml
@@ -1,27 +1,109 @@
+
+ [ Toggle abstracts ]
+
+
+ -
+
+ Andrea Asperti, Enrico Tassi
+
+
+ Higher order proof reconstruction from paramodulation-based refutations:
+ the unit equality case
+
+
+ .pdf
+
+
+ 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
+ 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.
+
+
+
+ -
+
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+
+
+ Spurious Disambiguation Error Detection
+
+
+ .pdf
+
+
+ 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
+ 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.
+
+
+
-
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
- The Matita Proof Assistant
+ Crafting a Proof Assistant
-
+
.pdf
-
- .ps
-
- Submitted to Journal of Automated Reasoning, Special Issue on User
- Interfaces for Theorem Proving
+ 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
+ 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.
+
+
+
+
+ -
+
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+
+ User Interaction with the Matita Proof Assistant
+
+
+ .pdf
+
+
+ Accepted for publication in Journal of Automated Reasoning, Special Issue
+ on User Interfaces for Theorem Proving.
+
- 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.
+ 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.
@@ -36,13 +118,11 @@
.pdf
-
- .ps
-
- Submitted to UITP 2006 User Interfaces for Theorem Provers. Seattle, WA
- -- August 21, 2006.
-
+ 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
@@ -69,14 +149,11 @@
.pdf
-
- .ps
-
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
@@ -103,14 +180,11 @@
.pdf
-
- .ps
-
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
@@ -134,15 +208,12 @@
.pdf
-
- .ps
-
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
-
+
Mathematical notation has the characteristic of being ambiguous:
operators can be overloaded and information that can be deduced is often