An Introduction to Proof Equivalence

About

The goal of this course is to provide an overview on important results and current research trends in proof theory around the notion of proof equivalence. This is the problem of understanding when two formal derivations represent ``the same proof, both intuitively and in more precise semantical terms. The search for more canonical representations of logical arguments has lead to the design of new proof systems based on ideas from graph theory or category theory. Research on proof equivalence has received considerable attention in the proof-theory community, and has led in recent years to several applications in computer science (e.g. for program equivalence or proof-search). However, a structured presentation of fundamental results and perspectives in this area is still missing, and we consider this course as a first step in the direction of filling this gap.

Course leader

Matteo Acclavio and Paolo Pistone

Target group

Students

Fee info