The Coq mailing list

["PTP'04 Workshop" <ptp-04 AT ags.uni-sb.de>]

[Apologies for multiple copies of this announcement]

                     IJCAR'04 Workshop on

     (Re-)Presentations and Transformations of Proofs (PTP'04)
     =========================================================
 
                       July 5th, 2004
                    University College Cork
                  Cork, County Cork, Ireland 

               http://www.ags.uni-sb.de/~ptp-04/


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

Electronic submissions in PostScript or PDF are solicited.  Papers can
be up to 15  pages long and  comply with the IJCAR-workshop formatting
guidelines. The  submitted  papers will undergo  a standard refereeing
process  by the program  committee.  The workshop  proceedings will be
published as a SEKI technical report and will be available online.


Deadlines:
==========

Paper submissions due:          Sunday, March 28, 2004.
Notification letters sent:      Monday, May 24, 2004.
Final camera-ready copies due:  Sunday, June 6, 2004.

 

Program Committee
=================

Peter Andrews, CMU, Pittsburgh, USA
Serge Autexier, DFKI, Saarbruecken, Germany (co-chair)
Yves Bertot, INRIA, Sophia-Antipolis, France
Armin Fiedler, Saarland University, Saarbruecken, Germany (co-chair)
Fairouz Kamareddine, Heriot Watt University, Edinburgh, UK
Christoph Kreitz, University of Potsdam, Germany
Roman Matuszewski, University of Bialystok, Poland
Rob Nederpelt, Eindhoven University of Technology, Eindhoven, The Netherlands
Frank Pfenning, CMU, Pittsburgh, USA
Carsten Schuermann, Yale University, New Haven, USA