PCC - Proof, Computation, Complexity

International workshop

June 17th - 19th, 2004, Dresden

Aims and Scope Contributions Further information Preliminary Program

Aims and Scope

The aim of PCC is to stimulate research in proof theory, computation, and complexity, focusing on issues which combine logical and computational aspects. Topics may include applications of formal inference systems in computer science, as well as new developments in proof theory motivated by computer science demands. Specific areas of interest are (non-exhaustively listed) foundations for specification and programming languages, logical methods in specification and program development, new developments in structural proof theory, and implicit computational complexity.

The workshop PCC '04 is held in conjunction with the Summer School on Proof Theory and Automated Theorem Proving in Dresden. Past events were held 2003 in Dresden, in conjunction with the Summer School on Proof Theory, Computation, and Complexity, and 2002 in Tübingen.


PCC is intended to be a lively forum for presenting and discussing recent work. Participants who want to contribute a talk are asked to submit an abstract (LaTeX, 1-2 pages). The collection of abstracts will be available at the meeting.

Deadline: May 14th, 2004
Submission of abstracts: pcc@informatik.unibw-muenchen.de

Organization, registration and further information

The workshop PCC '04 is held in conjunction with the Summer School on Proof Theory and Automated Theorem Proving in Dresden. This event is organized by the International Center for Computational Logic, Paola Bruscoli, Birgit Elbl, Sylvia Epp, Bertram Fronhöfer, Alessio Guglielmi, Steffen Hölldobler, Reinhard Kahle and Mariana Stantcheva. For registration and further information consult the main page of the combined event.

Preliminary Program

Thursday, June 17

14:00 Start

Ulrich Berger A computational interpretation of open induction
Pascal Hitzler Rule-based reasoning over conceptual knowledge
Coffee Break
Roberto Maieli Modularity of proofs
Lutz Straßburger On proof nets for classical logic

Friday, June 18

9:30 Morning Session

Kai Brünnler Herbrand's theorem without cut elimination
Ozan Kahrmanogullari Plans as formulae with a non-commutative logical operator
Coffee Break
Lars Kristiansen Small complexity classes and fragments of Gödel's system T
Karl-Heinz Niggl A short note on a simplified μ-measure on stack programs

14:15 Afternoon Session

Michael Arndt Locations in logic: historical root
Coffee Break
Gilda Ferreira Weak theories of arithmetic and the counting hierarchy
David Steiner On the proof theory of higher type functionals based on primitive recursive operations

Saturday, June 19

9:30 Start

Rajeev Goré A general theorem on termination of rewriting
Stéphane Lengrand The sequent calculus of constructions
Coffee Break
Pedrag Janicic On predicting the grammar of a normal-form
Birgit Elbl Some notes on transforming proofs for presentation
Reinhard Kahle A note on the well-founded semantics for extended logic programs