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