Home

Registration

Programme

Programme Committee, Organization

Workshops

Sponsors

Call for Papers

Submission

---

Important Dates

1 March 2007:

Deadline for electronic submissions of title and abstract

4 March 2007:

Deadline for electronic submissions of full papers

2 April 2007:

Notification of acceptance/rejection

13 April 2007:

Camera ready copies due

13 May 2007:

Early Registration

27--30 June 2007:

Conference at RISC, Hagenberg, Austria

---

Relevant Links

• Springer Proceedings LNAI 4573
• Mathematical User-Interfaces Workshop 2007 (MathUI07)
• 8th OpenMath Meeting
• MKM Interest Group
• email to co-chairs
• Previous Conferences
• Calculemus 2007
• RISC Summer 2007
• Mirror on MKM Page

Mathematical Knowledge Management 2007 27 - 30 June 2007 -- RISC, Hagenberg, Austria -- RISC Summer 2007

---

Programme:

Invited Speakers:

Neil J. A. Sloane	AT&T Shannon Labs, Florham Park, NJ, USA	The On-Line Encyclopedia of Integer Sequences
Peter Murray Rust	University of Cambridge, Dep. of Chemistry, UK	Mathematics and scientific markup

The programme is arranged so that the attendees of MKM can also attend talks by some of the invited speakers of Calculemus:

Thomas Hales	University of Pittsburgh
John Harrison	Intel Inc.
Peter Paule	RISC-Linz

Workshops:

The following workshops are affiliated with MKM 2007:

• W3C Math Working Group Face-to-Face Meeting (23-24 June 2007)
• 8th OpenMath Meeting (25-26 June 2007)
• Mathematical User-Interfaces Workshop 2007 (MathUI07) (27 June 2007)

Schedule (changes possible, but not intented):

An overview of the schedule of MKM and Calculemus as well as their satellite workshops is shown in the table below. The colour codes are:

Calculemus main conference

MKM main conference

Calculemus satellite event

MKM satellite event

Social event

Sat 23rd

Sun 24th

Mon 25th

Tue 26th

Wed 27th

Thu 28th

Fri 29th

Sat 30th

Room

Room

Room

Room

Room

Room

Room

Room

Sem

Sem

I

II

I

II

I

II

I

II

I

II

I

II

09:00

-

09:30

W3C face2face

W3C face2face

OpenMath MathML JEM

OpenMath MathML JEM

Invited talk: R. Hähnle

MathUI

Invited Talk: P. Paule

Invited Talk: T. Hales

Talk 15-16

PLMMS

09:30

-

10:00

10:00

-

10:30

Coffee

Coffee

Coffee

Coffee

Coffee

Coffee

Coffee

Coffee

10:30

-

11:00

W3C face2face

W3C face2face

OpenMath MathML JEM

OpenMath MathML JEM

Talk 3-5

MathUI

Talk 1-3

Talk 6-8

Talk 7-9

Talk 12-13

Talk 17

PLMMS

11:00

-

11:30

WING registration

Business M.

11:30

-

12:00

Lunch

Lunch

Lunch

Lunch

Lunch

Lunch

Lunch

Lunch

13:30

-

14:00

W3C face2face

W3C face2face

OpenMath MathML JEM

Invited talk: D. Kapur

OpenMath MathML JEM

Invited talk: A. Voronkov

Invited Talk: J. Harrison

Invited Talk: N. Sloane

Invited Talk: P. Murray Rust

Talk 18-19

PLMMS

14:00

-

14:30

14:30

-

15:00

Coffee

Coffee

Coffee

Coffee

Coffee

Coffee

Coffee

15:00

-

15:30

W3C face2face

W3C face2face

OpenMath MathML JEM

Talk 1-2

OpenMath MathML JEM

Talk 6-8

Talk 1-3

MathUI

Talk 4-6

Talk 9-11 Work in Progress

Talk 10-12

Business M.

Talk 20-22

PLMMS

15:30

-

16:00

16:00

-

16:30

16:45

-

17:15

W3C face2face

W3C face2face

OpenMath MathML JEM

OpenMath MathML JEM

Conclusion

Talk 4-5

MathUI

Panel Discussion

Talk 13-14

PLMMS

Talk 23

17:15

-

17:45

17:45

-

18:15

Life after Five in Hagenberg

18:30

-

19:00

Soccer

19:00

-

19:30

WING Workshop Dinner (in Linz)

Jazz & Dine (Philipp Nykrin Trio Live)

Wine & Dine (Tasting of Austrian Wines)

19:30

-

20:00

20:00

-

20:30

Banquet (in Linz)

20:30

-

21:00

21:00

-

Thursday, 28 June 2007

Invited Talk

 9:00-10:00:   Peter Paule, RISC (Calculemus):

10:00-10:30:   Coffee break

Applications

Session Chair: Manfred Kerber

10:30-11:00: [Talk 1] James Davenport:
The Utility of OpenMath

11:00-11:30: [Talk 2] Dennis Peters, Mark Lawford, Baltasar Trancon y Widemann:
Software Specification Using Tabular Expressions and OMDoc

11:30-12:00: [Talk 3] Miguel Abanades, Jesus Escribano, Francisco Botana:
First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems

12:00-13:30:   Lunch break

Invited Talk

Session Chair: Manfred Kerber

13:30-14:30:   Neil J. A. Sloane, AT&T Shannon Labs:
The On-Line Encyclopedia of Integer Sequences

14:30-15:00:   Coffee break

Session Chair: Mateja Jamnik

15:00-15:30: [Talk 4] Simon Colton, Daniel Wagner:
Using Formal Concept Analysis in Mathematical Discovery

15:30-16:00: [Talk 5] Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller:
Mathematical Knowledge in Electrical Engineering

16:00-16:30: [Talk 6] Ewa Borak, Anna Zalewska:
Mizar Course in Logic and Set Theory

Session Chair: William Farmer

16:45-18:15:   Panel session: Future Directions for Calculemus and MKM
(with Michael Kohlhase, Thierry Coquand, Fairouz Kamareddine, Bruno Buchberger, Andrzej Trybulec)

20:00-??:??:   Banquet

Friday, 29 June 2007

Invited Talk

9:00-10:00:   Tom Hales, Pittsburgh (Calculemus):

10:00-10:30:   Coffee break

Proofs I

Session Chair: Bengt Nordström

10:30-11:00: [Talk 7] David Aspinall, Christoph Lüth, Daniel Winterstein:
A Framework for Interactive Proof

11:00-11:30: [Talk 8] Klaus Grue:
The layers of Logiweb

11:30-12:00: [Talk 9] Feryal Fulya Horozal, Chad Brown:
Formal Representation of Mathematics in a Dependently Typed Set Theory

12:00-13:30:   Lunch break

Invited Talk

Session Chair: Robert Miner

13:30-14:30:   Peter Murray Rust, Cambridge:
Mathematics and scientific markup

14:30-15:00:   Coffee break

Proofs II

Session Chair: Olga Caprotti

15:00-15:30: [Talk 10] Enrico Tassi, Andrea Asperti:
Higher order proof reconstruction from paramodulation-based refutations

15:30-16:00: [Talk 11] Andrei Paskevich, Konstantin Verchinine, Alexander Lyaletski and Anatoly Anisimov:
Reasoning inside a formula and ontological correctness of a formal mathematical text

Repositories

Session Chair: Andrzej Trybulec

16:00-16:30: [Talk 12] Pierre Corbineau, Cezary Kaliszyk:
Cooperative repositories for formal proofs

16:45-17:15: [Talk 13] Adam Grabowski, Christoph Schwarzweller:
Revisions as an Essential Tool to Maintain Mathematical Repositories

17:15-17:45: [Talk 14] Immanuel Normann, Michael Kohlhase:
Extended Formula Normalization for Retrieval and Sharing of Mathematical Knowledge

19:00-??:??:   Wine& dine

Saturday, 30 June 2007

Search

Session Chair: Alan Sexton

9:00-9:30: [Talk 15] Gilbert Lee, Piotr Rudnicki (talk given by Josef Urban):
Alternative Aggregates in Mizar

9:30-10:00: [Talk 16] Andrea Kohlhase, Michael Kohlhase:
Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch

10:00-10:30:   Coffee break

10:30-11:00: [Talk 17] Robert Miner, Rajesh Munavalli:
An Approach to Mathematical Search through Query Formulation and Data Normalization

Business Meeting

11:00-12:00:   Business Meeting

12:00-13:30:   Lunch break

Search (Cont'd)

Session Chair: Fairouz Kamareddine

13:30-14:00: [Talk 18] Abdou Youssef:
Methods of Relevance Ranking and Hit-content Generation in Math Search

Mathematical Assistants

14:00-14:30: [Talk 19] Serge Autexier, Armin Fiedler, Thomas Neumann, Marc Wagner:
Supporting User-Defined Notations when Integrating Scientific Text-Editors with Proof Assistance Systems

14:30-15:00:   Coffee break

Session Chair: Robert Miner

15:00-15:30: [Talk 20] Fairouz Kamareddine, Robert Lamar, Manuel Maarek, J. B. Wells:
Restoring Natural Language as a Computerised Mathematics Input Method

15:30-16:00: [Talk 21] Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, J. B. Wells:
Narrative Structure of Mathematical Texts

16:00-16:30: [Talk 22] Claudio Sacerdoti Coen, Stefano Zacchiroli:
Spurious Disambiguation Error Detection

16:30-17:00: [Talk 23] Lionel Elie Mamane, Herman Geuvers:
A Document-Oriented Coq Plugin for TeXmacs

Page maintained by Manfred Kerber, University of Birmingham, School of Computer Science, Birmingham B15 2TT, England. Last update: 23 August 2010