Workshop on
Mathematically Intelligent Proof Search
MIPS 2010
Paris, France, 10th July 2010
The workshop on Mathematically Intelligent Proof Search explores the
relationship between mathematical theory development and proof construction.
It aims most directly at taking steps towards a deeper understanding of this
relationship in both informal and formal contexts, but has the central,
long-term goal of bringing these two contexts closer together in a
systematic way. This would pave the way for having machines analyze
mathematical texts and uncover leading ideas or heuristics for parts of
mathematics.
In either context, theory development and proof construction are deeply
connected: the choice of a language, expanded by definitions, and of a
corresponding inference mechanism correlates with how effectively proofs can
be obtained and how well mathematical arguments can be communicated. Thus
languages can range from mathematical vernaculars that are close to natural
languages to purely formal ones; inference mechanisms can structure
arguments conceptually but may also be based on automated proof procedures
that are mathematically intelligent.
MIPS will bring together researchers from Computer Science, Linguistics,
Mathematics and Philosophy who are interested in the whole subject or parts
of it, in order to get an overview of the state of the art, present original
results and discuss directions for future research:
The scope of MIPS thus includes topics such as
- formalization and automated proof search for mathematical
theories:
- domains of specific interests are set theory and geometry
- interactive verification and automated proof search
- alternative formalizations and their adaptive selection
|
|
- analysis and generation of mathematical texts
- natural language vs. controlled natural language
- domain specific vs. generic lexika text analysis
- textlinguistic aspects of mathematical texts
- cognitive aspects of the conceptualization and representation of mathematical texts
- adaptive document generation styles
|
with practical applications for
- authoring of mathematical texts
- verification of mathematical documents
- dynamic proof tutoring in mathematics
We encourage researchers working at points of contact among these
fields to share their views, work, or results by submitting a
title and abstract or short paper (2-5 pages in PDF format) and
taking part in the workshop. Please submit your work via EasyChair
http://www.easychair.org/conferences/?conf=mips2010.
Any questions you may have about the workshop should be send to mips2010@easychair.org
Submission of title and abstracts: | June 18, 2010 |
Notification of acceptance: | June 24, 2010 |
The accepted work should be presented at the workshop, which will
be a mixture of invited and accepted presentations. The
abstracts/short papers of the accepted and invited presentations
will be collected in informal proceedings and made available at
the workshop.
