"Respresentation of mathematical knowledge"
at the ECAI96 in Budapest (12.-13.8.96)
http://www.dfki.uni-sb.de/ecai96/call-for-workshops.html
http://wwwis.cs.utwente.nl:8080/mars/ECAI96.html
-----------------------------------------------------------------------------
!!!!! DEADLINE for the proposal is 1.Nov 1995 !!!!!
-----------------------------------------------------------------------------
Please reply as FAST AS POSSIBLE, if you
-- want to organize the workshop with us (we need two more
organisators),
-- want to hold a talk at the workshop.
Enclosed you will find our draft for the workshop proposal.
Any suggestions on the content/intent of the workshop are highly encouraged.
please reply to:
fermat@immd8.informatik.uni-erlangen.de
-----------------------------------------------------------------------------
The FERMAT-Group.
-----------------------------------------------------------------------------
Workshop-Proposal for ECAI96:
"Representation of mathematical knowledge"
The workshop is about representation formalisms for mathematical
knowledge. The overall goal of the workshop is to answer the central
question:
"What is the best knowledge representation formalism for
representing mathematics (in its entirety)?"
The question is not easy to answer and several workshops and
even more discussions will be necessary to tackle the problem
accurately and from various directions. One might ask some more
'sub-questions' like:
- Is an enumeration of mathematical concepts an adequate
representation of mathematical knowledge?
- Which role plays the level of understanding of mathematical
concepts in the representation of mathematical knowledge?
- Do we first need an ontology for mathematics before the
quest for an adequate representation formalism can be started?
- Which types of knowledge build-up expert mathematical knowledge?
- Is it possible to find a representation which supports more than
one view of mathematics?
What is mathematics, anyway? There exists several views about the
philosophy of mathematics:
- Mathematics is viewed as a formal science. 'Proof' is the central
concept as a means to establish the validity or falsity of
mathematical assertions. The basic activity for researchers in
artificial intelligence and theoretical computer science is the
building of proof machines, capable to prove theorems and to check
proofs. A (logic) calculus is used to represent mathematical
knowledge and some basic inference rules. Dozens of proof systems
have been (and will be) developed to mechanize the process of
proof. A list of current proof systems include McCune's OTTER (a
resolution-based) theorem prover (that accepts the theorem and the
theory to be represented in horn logic or predicate logic);
Weyrauch's et al. FOL systems. etc.
Mathematicians, however, argue that a formal representation of
mathematics represents only the formal aspect of
mathematics. They claim that mathematics is also a creative
science, where intuition plays a fundamental role. Intuition and
creativity, they argue, can not be represented as a set of
valid formulas. Some mathematicians argue, that they completely
ignore first order logic or whatever logic calculi at all.
Lenat's AM system is the reference for an AI systems modelling the
creative side of mathematics. Lenat used a frame formalism and some
250 heuristics; both representations will be discussed now:
- Mathematics at the concept level. This is a somehow semantical
view of mathematics. 'Definition' is the central concept as a
means to build consistent concept hierarchies in
order to describe the mathematical world accurately. In the past,
AI researchers used frames and semantic networks to represent this
kind of mathematics. These representations focus on objects, their
properties and interrelations. The frames approach supports the
representation of mathematical concepts in that way that the
knowledge associated with an object is representationally attached
to that object.
- Mathematics at the heuristic level. Heuristics are used to choose
the right action at the right time (in order to keep the
exploration space manageable). Everybody in the AI field should
know Polya's work: "How to solve it". Polya gives dozens of
heuristics for problem solving (not only) in the mathematical
field. One might use production rules/decision rules to formally
represent heuristics (in order to represent operational knowledge).
Production rules might be an adequate formalism in modeling the
decision process of problem-solving mathematicians.
Mathematicians, however, are often not able to state their
decision rules precisely. An accurate model of mathematical
activity is still lacking.
In the workshop one might discuss other views, like:
- the process view of mathematics,
- the symbol view of mathematics,
- the constraints view of mathematics and even
- non-symbolic views, like neural nets.
We argue, that all the existing basic formalisms for representing
knowledge, taken separately, are not strong enough to represent
mathematical knowledge in its different facets. Each representation
formalism emphasizes only one view of mathematical knowledge. It shows
to be difficult to express mathematical knowledge in its entirety
using one formalisms only. Mathematics and mathematicians live from
switching to different views whenever needed. Mathematical knowledge
in its totality is more than the sum of its parts.
In the workshop we will have a closer look on each of the existing
views on mathematics and representation formalisms. We first define
criteria in order to measure their 'usefulness' in representing
mathematical knowledge. These criteria will include expressive
adequacy and notational efficiency of formalisms. Obviously, a theorem
proving builder, a modeller of creativity and a mathematical hypertext
generator will not always share the same interpretation of the terms
adequacy and efficiency. The problem to be solved normally requires
the underlying representation to have certain characteristics. So,
each of these researchers may claim, that horn logic, frames or a
heuristic representation is the best representation for them.
The aims of the workshop are to:
- define requirements and criteria for a representation
language for mathematics,
- determine strengthens and shortcomings of existing
representations,
- suggest augmentations/modifications to existing representation
formalisms,
- guide future research work in order to find an adequate
representation for all scientists modelling certain aspects of the
mathematical mind.
There are many AI research groups which are concerned with the
representation of mathematical knowledge. They build problem solvers,
proof systems, theorem generators, etc.
Some of them search for a formalism which is both expressive, adequat
and user-friendly at the same time. One might imagine, that even
mathematicians may - in the near future - apply current research work.
A standard formalism for the communication of mathematical knowledge
would be very useful for the mathematics community. This might be done
via a standard common interface accessing/referring to large databases
of mathematical knowledge in a intuitive manner via the internet...
The workshop is planned as a two-day meeting. A typical workshop day
looks like that:
when | what |
---------|---------------------------|
| presentations of already |
09:00- | existing systems working |
12:30 | with representations |
| for mathematics |
---------|---------------------------|
| discussions concerning |
14:00- | already existing |
17:00 | representations of |
| mathematical knowledge |
| |
17:00- | free slot |
18:00 | on any subject |
Alternatively, one might swap presentation talks and discussion talks.
Any talk should not exceed 20 minutes. 10 minutes should be reserved
to question the talk.
What would be desirable would be the authoring of a technical paper
containing the state of the art of representation formalisms for
mathematical knowledge. Any dispute or consensus should be resolved or
protocolled in order to have some 'what to do' paper for future
research. To create a working atmosphere every workshop participant -
in order to get registrated - is required to present his views on the
subject in less than one page. After each presentation there will be
enough time for discussions. A free slot has been reserved to weaken
time limits imposed by the schedule. Both, the free slots open for
discussions on any subject and the developing of a technical paper at
the end of the workshop are the main differences to a conference
meeting.
The latest version of the proposal is available at:
http://faui80.informatik.uni-erlangen.de/IMMD8/staff/Jaksch/ecai96.html
---- end ----