Cork, Ireland, July 5th, 2004
in connection with IJCAR 2004
Program CommitteeP. 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 papersPostscript, pdf, ASCII
If you need further information do not hesitate to contact us by sending an e-mail to mailto:firstname.lastname@example.org?subject=PTP-Information.
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:
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:
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:email@example.com?subject=Paper submission. Upon submission, the name, address, and e-mail of the contact author should be included in the e-mail.
The workshop proceedings will be published as a SEKI technical report and will be available online.