(Re-)Presentations and Transformations of Proofs

PTP-04

Cork, Ireland, July 5th, 2004

in connection with IJCAR 2004

Program Committee

P. Andrews (CMU, Pittsburgh)
S. Autexier (DFKI Saarbrücken, co-chair)
Y. Bertot (INRIA Sophia-Antipolis)
A. Fiedler (U. Saarbrücken, co-chair)
F. Kamareddine (Heriot Watt U., Edinburgh)
C. Kreitz (U. Potsdam)
R. Matuszewski (U. Bialystok)
R. Nederpelt (Eindhoven U. Technology)
F. Pfenning (CMU, Pittsburgh)
C. Schürmann (Yale U., New Haven)

Call for papers

Postscript, pdf, ASCII

Important dates

Submission Deadline: March 28, 2004
Notification of acceptance: May 24, 2004
Final version due: June 6, 2004
Workshop date: July 4 or 5, 2004

Contact

If you need further information do not hesitate to contact us by sending an e-mail to mailto:ptp-04@ags.uni-sb.de?subject=PTP-Information.

Topic

Over the past thirty years there has been significant progress in the field of automated theorem proving with respect to the reasoning power of inference engines: many mathematical problems could be proven with a machine and the use of formal methods in software engineering and hardware verification is becoming a reality.

Another important ingredient of an automated reasoning system, however, is its ability to communicate with its users. For many applications such as mathematical assistant systems, an effective communication between the system and its users is critical for the acceptance of a system. Only if a system also talks his language will a user be convinced by machine-found proofs and feel his understanding of the topic improved. In mathematics tutoring systems, which teach mathematical topics to their users, as well as in mathematics assistant systems, natural language interfaces are most important in order to allow the users to focus on the mathematical content without hindering them by imposing a cumbersome interface language.

More recently, in order to avoid multiple inventions of the wheel, the desire to exchange mathematical knowledge between different systems emerged allowing one system to make use of results of another system. Such an exchange, however, requires that the systems either share the representation of the mathematical knowledge (speak a common language) or transform the knowledge between their respective representations. Moreover, transforming the great wealth of mathematical knowledge that has been collected and stored in books over the centuries into a machine-processable form has been a major aim and will be for the foreseeable future.

This informal workshop aims to create an intimate and stimulating setting to bring together researchers from various fields working with or interested in this exciting issue to exchange ideas and results. In particular, we want to focus on:

  • representations of mathematical knowledge (such as proofs) including
    • formal representations
    • semi-formal representations
    • informal representations
    • the natural language or multi-modal representations
    • cognitive models of human representations of mathematics
  • transformations between different forms of representations in all possible directions

Submission

Electronic submissions in PostScript or PDF are solicited. Papers can be up to 15 pages long and comply with the following IJCAR-workshop formatting guidelines:

\documentclass[a4paper,11pt]{article}
\usepackage{times,mathptm}
\textwidth 14.63cm
\textheight 22cm
\oddsidemargin 0.65cm
\evensidemargin 0.65cm
\topmargin 0.55cm
\headheight 0.0pt
\headsep 0.0pt

The submitted papers will undergo a standard refereeing process by the program committee. Please submit papers in postscript or PDF format by e-mail to mailto:ptp-04@ags.uni-sb.de?subject=Paper submission. Upon submission, the name, address, and e-mail of the contact author should be included in the e-mail.

Proceedings

The workshop proceedings will be published as a SEKI technical report and will be available online.

Serge Autexier
Last modified: Thu Jan 15 16:02:48 CET 2004 Created: Fri Jan 9 15:06:47 CET 2004