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