]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/papers.shtml
...
[helm.git] / helm / www / matita / papers.shtml
1 <small>
2   <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
3 </small>
4
5 <ul>
6   
7   <li class="paper">
8   <span class="paper_author">
9     Andrea Asperti, Enrico Tassi
10   </span><br/>
11   <span class="paper_title">
12     Higher order proof reconstruction from paramodulation-based refutations:
13     the unit equality case
14   </span>
15   <a class="paper_download" href="PAPERS/hopr.pdf">
16     <span class="pdf_logo">.pdf</span>
17   </a>
18   <span class="paper_info">
19     Accepted for publication in the proceedings of MKM 2007: The 6th
20     International Conference on Mathematical Knowledge Management.
21   </span>
22   <span class="paper_abstract">
23     In this paper we address the problem of reconstructing a
24     higher order, checkable proof object starting from a proof trace left by a
25     first order automatic proof searching procedure, in a restricted equational
26     framework. The automatic procedure is based on superposition rules for
27     the unit equality case. Proof transformation techniques aimed to improve
28     the readability of the final proof are discussed.
29   </span>
30   </li>
31   
32   <li class="paper">
33   <span class="paper_author">
34     Claudio Sacerdoti Coen, Stefano Zacchiroli
35   </span><br/>
36   <span class="paper_title">
37     Spurious Disambiguation Error Detection
38   </span>
39   <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
40     <span class="pdf_logo">.pdf</span>
41   </a>
42   <span class="paper_info">
43     Accepted for publication in the proceedings of MKM 2007: The 6th
44     International Conference on Mathematical Knowledge Management.
45   </span>
46   <span class="paper_abstract">
47     The disambiguation approach to the input of formulae enables the user to
48     type correct formulae in a terse syntax close to the usual ambiguous
49     mathematical notation. When it comes to incorrect formulae we want to
50     present only errors related to the interpretation meant by the user, hiding
51     errors related to other interpretations (spurious errors). We propose a
52     heuristic to recognize spurious errors, which has been integrated with our
53     former efficient disambiguation algorithm.
54   </span>
55   </li>
56   
57   <li class="paper">
58   <span class="paper_author">
59     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
60   </span><br/>
61   <span class="paper_title">
62     Crafting a Proof Assistant
63   </span>
64   <a class="paper_download" href="PAPERS/matita_types.pdf">
65     <span class="pdf_logo">.pdf</span>
66   </a>
67   <span class="paper_info">
68     Accepted for publication in the Proceedings of Types 2006: Conference of
69     the Types Project. Nottingham, UK -- April 18-21, 2006.
70   </span>
71   <span class="paper_abstract">
72      Proof assistants are complex applications whose develop-
73      ment has never been properly systematized or documented. This work is
74      a contribution in this direction, based on our experience with the devel-
75      opment of Matita: a new interactive theorem prover based—as Coq—on
76      the Calculus of Inductive Constructions (CIC). In particular, we analyze
77      its architecture focusing on the dependencies of its components, how they
78      implement the main functionalities, and their degree of reusability.
79      The work is a first attempt to provide a ground for a more direct com-
80      parison between different systems and to highlight the common func-
81      tionalities, not only in view of reusability but also to encourage a more
82      systematic comparison of different softwares and architectural solutions.
83   </span>
84   </li>
85   
86   
87   <li class="paper">
88   <span class="paper_author">
89     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
90   </span><br/>
91   <span class="paper_title">
92     User Interaction with the Matita Proof Assistant
93   </span>
94   <a class="paper_download" href="PAPERS/matita.pdf">
95     <span class="pdf_logo">.pdf</span>
96   </a>
97   <span class="paper_info">
98     Accepted for publication in Journal of Automated Reasoning, Special Issue
99     on User Interfaces for Theorem Proving.
100   </span>
101   <span class="paper_abstract">
102      Matita is a new, document-centric, tactic-based interactive theorem
103      prover. This paper focuses on some of the distinctive features of the user interaction
104      with Matita, mostly characterized by the organization of the library as a search-
105      able knowledge base, the emphasis on a high-quality notational rendering, and the
106      complex interplay between syntax, presentation, and semantics.
107   </span>
108   </li>
109   
110   
111   <li class="paper">
112   <span class="paper_author">
113     Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
114   </span><br/>
115   <span class="paper_title">
116       Tinycals: step by step tacticals
117   </span>
118   <a class="paper_download" href="PAPERS/tinycals.pdf">
119     <span class="pdf_logo">.pdf</span>
120   </a>
121   <span class="paper_info">
122     In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
123     WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
124     142, ISSN:1571-0661
125   </span>
126   <span class="paper_abstract">
127       Most of the state-of-the-art proof assistants are based on procedural
128       proof languages, scripts, and rely on LCF tacticals as the primary tool
129       for tactics composition. In this paper we discuss how these ingredients
130       do not interact well with user interfaces based on the same interaction
131       paradigm of Proof General (the de facto standard in this field),
132       identifying in the coarse-grainedness of tactical evaluation the key
133       problem.
134
135       We propose tinycals as an alternative to a subset of LCF tacticals,
136       showing that the user does not experience the same problem if tacticals
137       are evaluated in a more fine-grained manner. We present the formal
138       operational semantics of tinycals as well as their implementation in the
139       Matita proof assistant.
140   </span>
141   </li>
142   
143   
144   <li class="paper">
145   <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
146   <span class="paper_title">
147       From notation to semantics: there and back again
148   </span>
149   <a class="paper_download" href="PAPERS/notation.pdf">
150     <span class="pdf_logo">.pdf</span>
151   </a>
152   <span class="paper_info">
153       Accepted for publication in the proceedings of MKM 2006: The 5th
154       International Conference on Mathematical Knowledge Management.
155       Wokingham, UK -- August 11-12, 2006.
156   </span>
157   <span class="paper_abstract">
158       Mathematical notation is a structured, open, and ambiguous language.  In
159       order to support mathematical notation in MKM applications one must
160       necessarily take into account presentational as well as semantic aspects.
161       The former are required to create a familiar, comfortable, and usable
162       interface to interact with.  The latter are necessary in order to process
163       the information meaningfully.  In this paper we investigate a framework
164       for dealing with mathematical notation in a meaningful, extensible way,
165       and we show an effective instantiation of its architecture to the field
166       of interactive theorem proving. The framework builds upon well-known
167       concepts and widely-used technologies and it can be easily adopted by
168       other MKM applications.
169   </span>
170   </li>
171   
172   
173   <li class="paper">
174   <span class="paper_author">
175     Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
176   </span><br/>
177   <span class="paper_title">
178       A content based mathematical search engine: Whelp
179   </span>
180   <a class="paper_download" href="PAPERS/whelp.pdf">
181     <span class="pdf_logo">.pdf</span>
182   </a>
183   <span class="paper_info">
184       In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
185       Paris, France -- December 15-18, 2004.  LNCS 3839/2004, Springer-Verlag
186       Heidelberg, ISBN 3-540-31428-8, pp. 17-32
187   </span>
188   <span class="paper_abstract">
189       The prototype of a content based search engine for mathematical knowledge
190       supporting a small set of queries requiring matching and/or typing
191       operations is described. The prototype, called Whelp, exploits a metadata
192       approach for indexing the information that looks far more flexible than
193       traditional indexing techniques for structured expressions like
194       substitution, discrimination, or context trees. The prototype has been
195       instantiated to the standard library of the Coq proof assistant extended
196       with many user contributions.
197   </span>
198   </li>
199   
200   
201   <li class="paper">
202   <span class="paper_author">
203     Claudio Sacerdoti Coen, Stefano Zacchiroli
204   </span><br/>
205   <span class="paper_title">
206     Efficient Ambiguous Parsing of Mathematical Formulae
207   </span>
208   <a class="paper_download" href="PAPERS/disambiguation.pdf">
209     <span class="pdf_logo">.pdf</span>
210   </a>
211   <span class="paper_info">
212       In Proceedings of MKM 2004
213       Third International Conference on Mathematical Knowledge Management.
214       September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
215       Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
216   </span>
217   <span class="paper_abstract">
218       Mathematical notation has the characteristic of being ambiguous:
219       operators can be overloaded and information that can be deduced is often
220       omitted.  Mathematicians are used to this ambiguity and can easily
221       disambiguate a formula making use of the context and of their ability to
222       find the right interpretation.
223
224       Software applications that have to deal with formulae usually avoid these
225       issues by fixing an unambiguous input notation. This solution is annoying
226       for mathematicians because of the resulting tricky syntaxes and becomes a
227       show stopper to the simultaneous adoption of tools characterized by
228       different input languages.
229
230       In this paper we present an efficient algorithm suitable for ambiguous
231       parsing of mathematical formulae. The only requirement of the algorithm
232       is the existence of a validity predicate over abstract syntax trees of
233       incomplete formulae with placeholders. This requirement can be easily
234       fulfilled in the applicative area of interactive proof assistants, and in
235       several other areas of Mathematical Knowledge Management.
236   </span>
237   </li>
238   
239 </ul>