]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita1.0/xml/papers.xml
additions and corrections to basic_2
[helm.git] / helm / www / matita1.0 / xml / papers.xml
1 <papers>
2   <!-- matita {{{ -->
3   <paper name="matita">
4     <authors>
5       <author>Andrea Asperti</author>
6       <author>Claudio Sacerdoti Coen</author>
7       <author>Enrico Tassi</author>
8       <author>Stefano Zacchiroli</author>
9     </authors>
10     <title>
11       The Matita Proof Assistant
12     </title>
13     <abstract>
14       Matita is a new document-centric proof assistant that integrates several
15       Mathematical Knowledge Management tools and techniques. In this paper we
16       describe the architecture of Matita and the peculiarities of its user
17       interface.
18     </abstract>
19     <info>
20       Submitted to <a href="http://www-unix.mcs.anl.gov/JAR/">Journal of
21         Automated Reasoning</a>, Special Issue on User Interfaces for Theorem
22       Proving
23     </info>
24   </paper>
25   <!-- }}} -->
26   <!-- tinycals {{{ -->
27   <paper name="tinycals">
28     <authors>
29       <author>Claudio Sacerdoti Coen</author>
30       <author>Enrico Tassi</author>
31       <author>Stefano Zacchiroli</author>
32     </authors>
33     <title>
34       Tinycals: step by step tacticals
35     </title>
36     <abstract>
37       Most of the state-of-the-art proof assistants are based on procedural
38       proof languages, scripts, and rely on LCF tacticals as the primary tool
39       for tactics composition. In this paper we discuss how these ingredients
40       do not interact well with user interfaces based on the same interaction
41       paradigm of Proof General (the de facto standard in this field),
42       identifying in the coarse-grainedness of tactical evaluation the key
43       problem.
44
45       We propose tinycals as an alternative to a subset of LCF tacticals,
46       showing that the user does not experience the same problem if tacticals
47       are evaluated in a more fine-grained manner. We present the formal
48       operational semantics of tinycals as well as their implementation in the
49       Matita proof assistant.
50     </abstract>
51     <info>
52       Submitted to
53       <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP 2006</a>
54       User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006.
55     </info>
56   </paper>
57   <!-- }}} -->
58   <!-- notation {{{ -->
59   <paper name="notation">
60     <authors>
61       <author>Luca Padovani</author>
62       <author>Stefano Zacchiroli</author>
63     </authors>
64     <title>
65       From notation to semantics: there and back again
66     </title>
67     <abstract>
68       Mathematical notation is a structured, open, and ambiguous language.  In
69       order to support mathematical notation in MKM applications one must
70       necessarily take into account presentational as well as semantic aspects.
71       The former are required to create a familiar, comfortable, and usable
72       interface to interact with.  The latter are necessary in order to process
73       the information meaningfully.  In this paper we investigate a framework
74       for dealing with mathematical notation in a meaningful, extensible way,
75       and we show an effective instantiation of its architecture to the field
76       of interactive theorem proving. The framework builds upon well-known
77       concepts and widely-used technologies and it can be easily adopted by
78       other MKM applications.
79     </abstract>
80     <info>
81       Accepted for publication in the proceedings of
82       <a href="http://www.reading.ac.uk/MKM06/">MKM 2006</a>: The
83       5th International Conference on Mathematical Knowledge Management.
84       Wokingham, UK -- August 11-12, 2006.
85     </info>
86   </paper>
87   <!-- }}} -->
88   <!-- whelp {{{ -->
89   <paper name="whelp">
90     <authors>
91       <author>Andrea Asperti</author>
92       <author>Ferruccio Guidi</author>
93       <author>Claudio Sacerdoti Coen</author>
94       <author>Enrico Tassi</author>
95       <author>Stefano Zacchiroli</author>
96     </authors>
97     <title>
98       A content based mathematical search engine: Whelp
99     </title>
100     <abstract>
101       The prototype of a content based search engine for mathematical knowledge
102       supporting a small set of queries requiring matching and/or typing
103       operations is described. The prototype, called Whelp, exploits a metadata
104       approach for indexing the information that looks far more flexible than
105       traditional indexing techniques for structured expressions like
106       substitution, discrimination, or context trees. The prototype has been
107       instantiated to the standard library of the Coq proof assistant extended
108       with many user contributions.
109     </abstract>
110     <info>
111       In Proceedings of
112       <a href="http://types2004.lri.fr/">TYPES 2004 conference</a> Types for
113       Proofs and Programs. Paris, France -- December 15-18, 2004.
114       LNCS 3839/2004, Springer-Verlag Heidelberg, ISBN 3-540-31428-8, pp. 17-32
115     </info>
116   </paper>
117   <!-- }}} -->
118   <!-- disambiguation {{{ -->
119   <paper name="disambiguation">
120     <authors>
121       <author>Claudio Sacerdoti Coen</author>
122       <author>Stefano Zacchiroli</author>
123     </authors>
124     <title>
125       Efficient Ambiguous Parsing of Mathematical Formulae
126     </title>
127     <abstract>
128       Mathematical notation has the characteristic of being ambiguous:
129       operators can be overloaded and information that can be deduced is often
130       omitted.  Mathematicians are used to this ambiguity and can easily
131       disambiguate a formula making use of the context and of their ability to
132       find the right interpretation.
133
134       Software applications that have to deal with formulae usually avoid these
135       issues by fixing an unambiguous input notation. This solution is annoying
136       for mathematicians because of the resulting tricky syntaxes and becomes a
137       show stopper to the simultaneous adoption of tools characterized by
138       different input languages.
139
140       In this paper we present an efficient algorithm suitable for ambiguous
141       parsing of mathematical formulae. The only requirement of the algorithm
142       is the existence of a validity predicate over abstract syntax trees of
143       incomplete formulae with placeholders. This requirement can be easily
144       fulfilled in the applicative area of interactive proof assistants, and in
145       several other areas of Mathematical Knowledge Management.
146     </abstract>
147     <info>
148       In Proceedings of <a href="http://mizar.uwb.edu.pl/MKM2004/">MKM 2004</a>
149       Third International Conference on Mathematical Knowledge Management.
150       September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
151       Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
152     </info>
153   </paper>
154   <!-- }}} -->
155 </papers>
156 <!-- vim:set foldmethod=marker: -->