Accepted Papers
The list of accepted papers below is ordered alphabetically
by first author surname.
Links to preprints (on http://ArXiv.org) and to the final
published articles (on http://www.springerlink.com) will be
added as they become available.
The full proceedings of the conference are available from
Springer (LNAI 6167). You can find information about it at
http://www.springeronline.com/978-3-642-14127-0
or access the online version at
http://www.springerlink.com/content/978-3-642-14127-0/
-
Smart matching
Andrea Asperti, Enrico Tassi
Abstract:
One of the most annoying aspects in the formalization
of mathematics is the need of transforming notions to
match a given, existing result. This kind of
transformations, often based on a conspicuous
background knowledge in the given scientific domain
(mostly expressed in the form of equalities or
isomorphisms), are usually implicit in the
mathematical discourse, and it would be highly
desirable to obtain a similar behaviour in interactive
provers. The paper describes the superposition-based
implementation of this feature inside the Matita
interactive theorem prover, focusing in particular on
the so called smart application tactic, supporting
smart matching between a goal and a given result.
-
Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System
Xiaoyu Chen
Abstract:
Electronic Geometry Textbook is a knowledge management
system that manages geometric textbook knowledge to
enable users to construct and share dynamic geometry
textbooks interactively and efficiently. Based on a
knowledge base organizing and storing the knowledge
represented in specific languages, the system
implements interfaces for maintaining the data
representing that knowledge as well as relations among
those data, for automatically generating readable
documents for viewing or printing, and for
automatically discovering the relations among
knowledge data. An interface has been developed for
users to create geometry textbooks with automatic
checking, in real time, of the consistency of the
structure of each resulting textbook. By integrating
an external geometric theorem prover and an external
dynamic geometry software package, the system offers
the facilities for automatically proving theorems and
generating dynamic figures in the created textbooks.
This paper provides a comprehensive account of the
current version of Electronic Geometry Textbook.
-
An OpenMath Content Dictionary for Tensor Concepts
Joseph Collins
Abstract:
We introduce a new OpenMath content dictionary named
“tensor1” containing symbols for the
expression of tensor formulas. These symbols support
the expression of non-Cartesian coordinates and
invariant, multilinear expressions in the context of
coordinate transformations. While current OpenMath
symbols support the expression of linear algebra
formulas using matrices and vectors, we find that
there is an underlying assumption of Cartesian, or
standard, coordinates that makes the expression of
general tensor formulas difficult, if not impossible.
In introducing these new OpenMath symbols for the
expression of tensor formulas, we attempt to maintain,
as much as possible, consistency with prior OpenMath
symbol definitions for linear algebra.
-
On Duplication in Mathematical Repositories
Adam Grabowski, Christoph Schwarzweller
Abstract:
Building a repository of proof-checked mathematical
knowledge is without any doubt a lot of work, and
besides the actual formalization process there is also
the task of maintaining the repository. Thus it seems
obvious to keep a repository as small as possible, in
particular each piece of mathematical knowledge should
be formalized only once. In this paper, however, we
claim that it might be reasonable or even necessary to
duplicate knowledge in a mathematical repository. We
analyze different situations and reasons for doing so,
provide a number of examples supporting our thesis and
discuss some implications for building mathematical
repositories.
-
Adapting Mathematical Domain Reasoners
Bastiaan Heeren, Johan Jeuring
Abstract:
Mathematical learning environments help students in
mastering mathematical knowledge. Mature environments
typically offer thousands of interactive exercises.
Providing feedback to students solving interactive
exercises requires domain reasoners for doing the
exercise-specific calculations. Since a domain
reasoner has to solve an exercise in the same way a
student should solve it, the structure of domain
reasoners should follow the layered structure of the
mathematical domains. Furthermore, learners, teachers,
and environment builders have different requirements
for adapting domain reasoners, such as providing more
details, disallowing or enforcing certain solutions,
and combining multiple mathematical domains in a new
domain. In previous work we have shown how domain
reasoners for solving interactive exercises can be
expressed in terms of rewrite strategies, rewrite
rules, and views. This paper shows how users can adapt
and configure such domain reasoners to their own
needs. This is achieved by enabling users to
explicitly communicate the components that are used
for solving an exercise.
-
Integrating multiple sources to answer questions in Algebraic Topology
Jönathan Heras, Vico Pascual, Ana Romero, Julio Rubio
Abstract:
We present in this paper an evolution of a tool from a
user interface for a concrete Computer Algebra system
for Algebraic Topology (the Kenzo system), to a
front-end allowing the interoperability among
different sources for computation and deduction. The
architecture allows the system not only to interface
several systems, but also to make them cooperate in
shared calculations.
-
sTeXIDE: An Integrated Development Environment for sTeX Collections
Constantin Jucovschi, Michael Kohlhase
Abstract:
Authoring documents in MKM formats like OMDoc is a
very tedious task. After years of working on a
semantically annotated corpus of STEX documents
(GenCS), we identified a set of common, time-consuming
subtasks, which can be supported in an integrated
authoring environment.
We have adapted the modular Eclipse IDE into STEXIDE,
an authoring solution for enhancing productivity in
contributing to STEX based corpora. STEXIDE supports
context-aware command completion, module management,
semantic macro retrieval, and theory graph navigation.
-
Proofs, proofs, proofs, and proofs
Manfred Kerber
Abstract:
In logic there is a clear concept of what constitutes
a proof and what not. A proof is essentially defined
as a finite sequence of formulae which are either
axioms or derived by proof rules from formulae earlier
in the sequence. Sociologically, however, it is more
difficult to say what should constitute a proof and
what not. In this paper we will look at different
forms of proofs and try to clarify the concept of
proof in the wider meaning of the term. This has
implications on how proofs should be represented
formally.
-
Dimensions of Formality: A Case Study for MKM in Software Engineering
Andrea Kohlhase, Michael Kohlhase, Christoph Lange
Abstract:
We study the formalization of a collection of
documents created for a Software Engineering project
from an MKM perspective. We analyze how document and
collection markup formats can cope with an open-ended,
multi-dimensional space of primary and secondary
classifications and relationships.We show that
RDFa-based extensions of MKM formats, employing
flexible “metadata” relationships
referencing specific vocabularies for distinct
dimensions, are well-suited to encode this and to put
it into service. This formalized knowledge can be used
for enriching interactive document browsing, for
enabling multi-dimensional metadata queries over
documents and collections, and for exporting Linked
Data to the Semantic Web and thus enabling further
reuse.
-
Towards MKM in the Large: Modular Representation and Scalable Software Architecture
Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev
Abstract:
MKM has been defined as the quest for technologies to
manage mathematical knowledge. MKM “in the
small” is well-studied, so the real problem is
to scale up to large, highly interconnected corpora:
“MKM in the large”. We contend that
advances in two areas are needed to reach this goal.
We need representation languages that support
incremental processing of all primitive MKM
operations, and we need software architectures and
implementations that implement these operations
scalably on large knowledge bases.
We present instances of both in this paper: the MMT
framework for modular theory-graphs that integrates
meta-logical foundations, which forms the base of the
next OMDOC version; and TNTBase, a versioned storage
system for XMLbased document formats. TNTBase becomes
an MMT database by instantiating it with special MKM
operations for MMT.
-
The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents
Andriy Kovalchuk, Vyacheslav Levitsky, Igor Samolyuk, Valentyn Yanchuk
Abstract:
Implementation of an editing process for Content
MathML formulas in common visual style is a real
challenge for a software developer who does not really
want the user to have to understand the structure of
Content MathML in order to edit an expression, since
it is expected that users are often not that
technically minded. In this paper, we demonstrate how
this aim is achieved in the context of the Formulator
project and discuss features of this MathML editor,
which provides a user with a WYSIWYG editing style
while authoring MathML documents with Content or mixed
markup. We also present the approach taken to enhance
availability of the MathML editor to end-users,
demonstrating an online version of the editor that
runs inside a Web browser.
-
Notations Around the World: Census and Exploitation
Paul Libbrecht
Abstract:
Mathematical notations around the world are diverse.
Not as much as requiring computing machines' makers to
adapt to each culture, but as much as to disorient a
person landing on a web-page with a text in
mathematics.
In order to understand better this diversity, we are
building a census of notations: it should allow any
content creator or mathematician to grasp which
mathematical notation is used in which language and
culture. The census is built collaboratively,
collected in pages with a given semantic and
presenting observations of the widespread notations
being used in existing materials by a graphical
extract. We contend that our approach should dissipate
the fallacies found here and there about the notations
in “other cultures” so that a better
understanding of the cultures can be realized.
The exploitation of the census in the math-bridge
project is also presented: this project aims at taking
learners “where they are in their
math-knowledge” and bring them to a level ready
to start engineering studies. The census serves as
definitive reference for the transformation elements
that generate the rendering of formulae in
web-browsers.
-
Evidence Algorithm and System for Automated Deduction: A Retrospective View
Alexander Lyaletski, Konstantin Verchinine
Abstract:
A research project aimed at the development of an
automated theorem proving system was started in Kiev
(Ukraine) in early 1960s. The mastermind of the
project, Academician V.Glushkov, baptized it
“Evidence Algorithm“, EA. The work on the
project lasted, off and on, more than 40 years. In the
framework of the project, the Russian and English
versions of the System for Automated Deduction, SAD,
were constructed. They may be already seen as powerful
theorem proving assistants. The paper gives a
retrospective view to the whole history of the
development of the EA and SAD. Theoretical and
practical results obtained on the long way are
systematized. No comparison with similar projects is
made.
-
On Building a Knowledge Base for Stability Theory
Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller
Abstract:
A lot of mathematical knowledge has been formalized
and stored in repositories by now: Different
mathematical theorems and theories have been taken
into consideration and included in mathematical
repositories. Applications more distant from pure
mathematics, however — though based on these
theories — often need more detailed knowledge
about the underlying theories. In this paper we
present an example Mizar formalization from the area
of electrical engineering focusing on stability theory
which is based on complex analysis. We discuss what
kind of special knowledge is necessary and which
amount of this knowledge is included in existing
repositories.
-
Proviola: a Tool for Proof Re-animation
Carst Tankink, James McKinna, Herman Geuvers, Freek Wiedijk
Abstract:
To improve on existing models of interaction with a
proof assistant (PA), in particular for storage and
replay of proofs, we introduce three related concepts,
those of: a proof movie, consisting of frames which
record both user input and the corresponding PA
response; a camera, which films a user’s
interactive session with a PA as a movie; and a
proviola, which replays a movie frame-by-frame to a
third party. In this paper we describe the movie data
structure and we discuss a prototype implementation of
the camera and proviola based on the ProofWeb system.
ProofWeb uncouples the interaction with a PA via a
webinterface (the client) from the actual PA that
resides on the server. Our camera films a movie by
“listening” to the ProofWeb
communication.
The first reason for developing movies is to uncouple
the reviewing of a formal proof from the PA used to
develop it: the movie concept enables users to discuss
small code fragments without the need to install the
PA or to load a whole library into it.
Other advantages include the possibility to develop a
separate commentary track to discuss or explain the PA
interaction. We assert that a combined camera+proviola
provides a generic layer between a client (user) and a
server (PA). Finally we claim that movies are the
right type of data to be stored in an encyclopedia of
formalized mathematics, based on our experience in
filming the Coq standard library.
-
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
Abstract:
Formal mathematics has so far not taken full advantage
of ideas from collaborative tools such as wikis and
distributed version control systems (DVCS). We argue
that the field could profit from such tools, serving
both newcomers and experts alike. We describe a
preliminary system for such collaborative development
based on the Git DVCS. We focus, initially, on the
Mizar system and its library of formalized
mathematics.
|
