Workshop Proof Transformation and Presentation and Proof Complexities

 Siena, June 19, 2001

 in connection with IJCAR 2001 

International Joint Conference on Automated Reasoning


Program Committee

Richard Bornat (London, UK)
Bruno Buchberger (RISC, Austria)
Ingo Dahn (Koblenz, Germany)
Uwe Egly (Vienna, Austria, Co-Chair)
Armin Fiedler (Saarbrücken, Germany, Co-Chair)
Helmut Horacek (DFKI, Germany, Co-Chair)
Roman Matuszewski (Bialystok, Poland)
Aarne Ranta (Gothemburg, Sweden)
Stephan Schmitt (Madrid, Spain, Co-Chair)
Helmut Schwichtenberg (Munich, Germany)
Jörg Siekmann (DFKI, Germany)

Call for papers

PostScript, ps.gz, PDF

Important dates

Submission deadline: April 15, 2001
Notification of acceptance: April 30, 2001
Final version due: May 20, 2001
Early registration: to be announced

Worshop Program



For further information, send an e-mail to 


The output of an automated reasoning system, i.e., a proof of some kind, is usually hard to follow and of little intuitive clarity. Therefore proof representations need to be manipulated by transformation and presentation techniques, which serve the purpose of bridging differences in representation variants. Apart from variations in syntax and associated conventions, there are a number of more fundamental differences to be bridged, including differences in granularity, explicitness and, in particular, abstraction which requires dedicated methods and, sometimes, considerable computational resources. The presentation of proofs can be performed in a variety of form, sophistication, and quality. Depending on the kinds of presentation envisioned, a number of tasks have to be accomplished and appropriately orchestrated, including choice of media and their coordination (natural language text, graphics, formulas), content selection (leaving parts considered inferable implicit), textual structures, and sentence patterns.

Presenting proofs in a humanly understandable form becomes crucial whenever it is not sufficient to know that a theorem is valid but also to obtain some evidence how the proof steps have been established. Many practical applications of automated deduction require these kinds of proof transformations and presentations, e.g., when automated theorem provers are integrated as inference engines into interactive proof assistants, such as Coq, HOL, Isabelle, KIV, NuPRL, OMEGA, and PVS, for generating programs from proofs, and for generation of human language proofs. The possibility to support interactive development systems with powerful automated inference engines is a major step for large scale applications in various fields of Computer Science. Building adequate interfaces for such integrations depends on fundamental research and experimental experiences in proof transformations, proof presentations, and complexities of proofs.

In April 1997, the First International Workshop on Proof Transformation and Presentation took place at Schloss Dagstuhl in Germany, which was rather successful in terms of participation and scientific discussions. The workshop proposed for IJCAR is intended as a follow-up of the Dagstuhl workshop, and it is intended to hold this workshop now on a regular basis. Topics of interest include, but are not limited to:

  • proof presentations in classical and non-classical logics
  • generalization and structuring of proofs
  • generation of proofs in natural language and graphics
  • systems and implementations
  • applications (e.g., integration of automated and interactive theorem proving)
  • logical embeddings
  • complexity of proof transformations and logical embeddings.


Submissions addressing one of above topics (but not limited to) are encouraged in one of the following two categories:

  • A. Regular paper: Submissions in this category should describe completed work or work in progress, including descriptions of research, tools, and applications. The length of submitted papers should be at most 10 pages in LNCS style.
  • B. Discussion paper: Submissions in this category are intended to initiate discussions. They should address controversial issues and may include provocative statements. The length of papers should be 2-5 pages in LNCS style.

Authors should send submissions in postscript format by e-mail to The papers are required to be formatted according to the LNCS guidelines in A4 format. Informal proceedings will be available at the workshop and are provided by IJCAR. 


All authors of accepted papers and PC members will be invited. Other researchers who are interested in participating should send an e-mail to by May 13, 2001. 

Note that all participants must register to IJCAR.

Last modified: Wed May 30 17:09:56 MEST 2001