-
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
The Matita Proof Assistant
.pdf
.ps
Submitted to 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.
-
Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Tinycals: step by step tacticals
.pdf
.ps
Submitted to UITP 2006 User Interfaces for Theorem Provers. Seattle, WA
-- August 21, 2006.
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
for tactics composition. In this paper we discuss how these ingredients
do not interact well with user interfaces based on the same interaction
paradigm of Proof General (the de facto standard in this field),
identifying in the coarse-grainedness of tactical evaluation the key
problem.
We propose tinycals as an alternative to a subset of LCF tacticals,
showing that the user does not experience the same problem if tacticals
are evaluated in a more fine-grained manner. We present the formal
operational semantics of tinycals as well as their implementation in the
Matita proof assistant.
-
Luca Padovani, Stefano Zacchiroli
From notation to semantics: there and back again
.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
necessarily take into account presentational as well as semantic aspects.
The former are required to create a familiar, comfortable, and usable
interface to interact with. The latter are necessary in order to process
the information meaningfully. In this paper we investigate a framework
for dealing with mathematical notation in a meaningful, extensible way,
and we show an effective instantiation of its architecture to the field
of interactive theorem proving. The framework builds upon well-known
concepts and widely-used technologies and it can be easily adopted by
other MKM applications.
-
Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
A content based mathematical search engine: Whelp
.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
operations is described. The prototype, called Whelp, exploits a metadata
approach for indexing the information that looks far more flexible than
traditional indexing techniques for structured expressions like
substitution, discrimination, or context trees. The prototype has been
instantiated to the standard library of the Coq proof assistant extended
with many user contributions.
-
Claudio Sacerdoti Coen, Stefano Zacchiroli
Efficient Ambiguous Parsing of Mathematical Formulae
.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
omitted. Mathematicians are used to this ambiguity and can easily
disambiguate a formula making use of the context and of their ability to
find the right interpretation.
Software applications that have to deal with formulae usually avoid these
issues by fixing an unambiguous input notation. This solution is annoying
for mathematicians because of the resulting tricky syntaxes and becomes a
show stopper to the simultaneous adoption of tools characterized by
different input languages.
In this paper we present an efficient algorithm suitable for ambiguous
parsing of mathematical formulae. The only requirement of the algorithm
is the existence of a validity predicate over abstract syntax trees of
incomplete formulae with placeholders. This requirement can be easily
fulfilled in the applicative area of interactive proof assistants, and in
several other areas of Mathematical Knowledge Management.