Program CommitteeRichard 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 papersPostScript, ps.gz, PDFImportant datesSubmission deadline: April 15, 2001Notification of acceptance: April 30, 2001 Final version due: May 20, 2001 Early registration: to be announced Worshop ProgramPROVISIONAL PROGRAM.ContactFor further information, send an e-mail to ptp-01@ags.uni-sb.de. |
TopicThe 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:
SubmissionSubmissions addressing one of above topics (but not limited to) are encouraged in one of the following two categories:
Authors should send submissions in postscript format by e-mail to ptp-01@ags.uni-sb.de. 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. ParticipationAll authors of accepted papers and PC members will be invited. Other researchers who are interested in participating should send an e-mail to ptp-01@ags.uni-sb.de by May 13, 2001.Note that all participants must register to IJCAR. |