Proof, Computation, Complexity 2017

News

General Information

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 including program extraction from proofs, type theory, new developments in structural proof theory, and implicit computational complexity.

Commemorative Plaque for Paul Bernays

The town of Göttingen honors famous characters which had been living or working in this town by commemorative plaques on their houses. Celebrating the centenary of Paul Bernays's return to Göttingen in 1917 as David Hilbert's main collaborator for the study of the foundations of mathematics, there will be an unveiling ceremony of a commemorative plaque for Paul Bernays on Wednesday afternoon at Nikolausberger Weg 43. This ceremony will be part of the PCC workshop, and Michael Rathjen, Leeds, will give a short laudatory speech on Paul Bernays.

Venue

Mathematisches Institut der Universität Göttingen
Bunsenstr. 3-5, 37073 Göttingen

The talks are taking place in Lecture hall no.3, in German "Hörsaal 3".

Accommodation

Funding

Invited speaker

Johann (Janos) Makowsky (Technion, Haifa, Israel) is our invited speaker.

Title: The decidability of Geometry: From Hilbert-Bernays to Tarski and beyond.
Abstract: We discuss the decidability of Elementary Geometry from Hilbert-Bernays till contemporary computer assisted theorem proving in Geometry.

Programme

Wednesday 26th

9h Opening (Room: Hörsaal 3)

9h15-10h Reinhard Kahle: Hilbert and Bernays

We review the collaboration of David Hilbert and Paul Bernays in the 1920s and early 1930s in Göttingen.

10h-10h30 Coffee break

10h30-11h15 Olga Petrovska (joint work with Ulrich Berger): Natural Language Proofs for Program Extraction

Common software development techniques usually include substantial testing and bug fixing process. This process is costly in terms of time. It is prone to human errors as new bugs can be introduced and certain aspects may be overlooked due to testing not being exhaustive in many cases. An alternative approach to software development is program extraction. This technique implies proving correctness properties of software specifications formally in a proof assistant environment and then extracting software from such proof. However, most commonly used proof assistants are very restrictive in terms of language they use. The aim of this research is allowing a more natural proof style and avoiding the need to adjust to the proof assistant’s requirements.
Script is a prototype proof search system that is currently being developed as a part of this research. Its aim is creating a pipeline, which starts with natural language proofs as its input and enables to extract correct programs in the end of the process. In Script natural language proofs are transformed into their formal representations. Namely, each phrase in the proof script is processed by the system and is added to the context of the proof. Proof search checks whether it is possible to derive conclusions stated in the proof script using natural deduction rules. The formal system used is currently first-order logic, but the ultimate goal is to extend it to a constructive version of Church’s simple theory of types, which is a formulation of higher-order logic based on simply typed lambda calculus. When the user enters a complete natural proof, the system should generate a formal proof object in natural deduction and extract a program using a realizability interpretation.
Realizability gives a theoretical basis for program extraction. In this particular case lambda terms are used as realizers. Since lambda calculus can represent notions and properties of all functional languages, transforming lambda terms into actual program is fairly simple. The system has a lot in common with the interactive proof system Minlog developed at the University of Munich. The main difference is that our realizers are type free while Minog uses typed realizers.
The aim of this talk is to present theoretical background of program extraction from proofs, and realizability interpretation in particular as proposed by U.Berger/T.Hou. It will also provide a brief overview of language used in current proof assistants and give an outline of the main challenges of processing natural language proofs in a proof assistant environment. Additionally, we will report on the initial work, namely current development stage of Script.

11h15-12h00 Iosif Petrakis: Typoids in Univalent Type Theory

Bishop's notion of set is interpreted in Martin-Loef's type theory through the notion of setoid. A setoid is a type A paired with an equivalence relation on A such that the equivalence between any two points of A is a proposition. The morphisms between setoids are the functions between them that respect the corresponding equivalences. The resulting category of setoids is cartesian closed. Considering the equivalence between two points to be any type we study the notions of typoid and typoid functions between them. The notion of a univalent type, a type which satisfies an abstract version of Voevodsky's univalence axiom, can be described in this setting. In this work in progress we study the category of typoids and we prove some fundamental properties of univalent typoids.

14h30-15h15 Preda Mihailescu: Complexity between elegance and performance - a discussion on base of two fundamental number theoretical examples.

My talk will be a free discussion about the tension between efficiency and proof in complexity theory. I will focus on the two major problems of number theory, (the minor and major quint): Primality proving and integer factoring. But other problems may also be tangentially mentioned.

15h30 Michael Rathjen: laudatory speech on Paul Bernays

17h unveiling ceremony of a commemorative plaque for Paul Bernays

Thursday 27th (again in lecture hall "Hörsaal 3")

9h-10h Janis Makowsky: The decidability of Geometry: From Hilbert-Bernays to Tarski and beyond.

We discuss the decidability of Elementary Geometry from Hilbert-Bernays till contemporary computer assisted theorem proving in Geometry.

10h-10h30 Coffee break

10h30-11h15 René Gazzari: What is a Derivation?

An essential aspect of a derivation in the calculus of Natural Deduction is the discharge of assumptions. When defining derivations it is mentioned usually that the discharge of assumption relates some assumptions in a derivation with the inference step in which these assumptions are discharged. Little is said about the kind of entities related by the discharge, little about the discharge itself. The notions involved in the discharge of assumptions are only understood intuitively, and for this reason also the notion of a derivation .
We discuss different approaches to the formal representation of the discharge of assumptions; for one of these approaches, we provide the formal details: we introduce suitable entities (so called occurrences and their positions) representing the assumptions and the inference steps, and we provide a formally adequate definition of derivations accompanied by a suitable discharge function. If time is left, we may mention some additional aspects of Natural Deduction, where we may benefit from a formal notion of occurrences.

11h15-12h Ernst Zimmermann: Elimination by Composition in Natural Deduction

The paper introduces a new type of rules into Natural Deduction, elimination rules by composition. These rules replace usual elimination rules in the style of disjunction elimination and give a more direct treatment of additive disjunction, multiplicative conjunction, existence and modalities. Elimination rules by composition have an enormous impact on proof-structures of deductions: they do not produce cut segments, deduction trees remain mostly binary branching, there is no vacuous discharge, there is no need of permutative or commutative reductions in most cases. But for the purpose of uniqueness elimination rules by composition presuppose an additional semantical element: a decoration of formulas as parts of an instance of a rule. Nevertheless, this decoration turns out to be simply an extension of labelling of discharged assumptions in usual Natural Deduction. The new type of rules are shown within Intuitionistic Logic, Lambek Calculus, i.e. intuitionistic non-commutative linear logic and Modal Logic. Sketches for other substructural logics like linear logic are given. Reductions and normalisation strategies are shown to be smart modifications of usual methods.

13h30-14h15 Sam Sanders (joint work with Dag Normann): Nonstandard Analysis, Computability Theory, and metastability

We discuss a new connection between Nonstandard Analysis and computability theory, pioneered by the two authors, based on the following two intimately related topics.
(T.1) A basic property of Cantor space is Heine-Borel compactness: Any open cover of Cantor space, has a finite sub-cover. A natural question is: How hard is it to compute such a finite sub-cover? The so-called special and weak fan functionals compute such sub-covers, and exhibit surprising (and extreme) computational hardness.
(T.2) A basic property of Cantor space in Nonstandard Analysis is Abraham Robinson’s nonstandard compactness, i.e. that every binary sequence is ‘infinitely close’ to a standard binary sequence. We analyse the strength of this nonstandard compactness property in the spirit of Reverse Mathematics, which turns out to be intimately related to the computational properties of the special and weak fan functionals.
We connect the topics (T.1) and (T.2) to mainstream mathematics by deriving the special fan functional from slight variations of Tao’s notion of metastability. Based on the latter observation, we establish that many mathematical theorems naturally have ‘metastable versions’ which involve functionals of extreme computational hardness. We also discuss exceptions, like the infinite pigeon hole principle, whose metastable versions stay within Goedel’s T .

14h15-15h00 Angeliki Koutsoukou-Argyraki: Proof Mining for the Fixed Point Theory of Nonexpansive Semigroups (the linked PDF has the bibliography to which the abstract below refers)

Proof mining is a research program in applied proof theory aiming at the extraction of constructive information (in particular computable bounds) even from nonconstructive proofs in mathematics. The extractability of the bounds for statements of a certain logical form (and within an appropriate formal framework) is a priori guaranteed by certain logical metatheorems that have been shown by employing variations of Gödel's functional Dialectica interpretation. The bounds are obtained via a study of the underlying logical structure of a proof and are explicit, computable, highly uniform and of low complexity. Proof mining finds its early origins in the ideas of Kreisel and has been developed in recent years by Kohlenbach and his collaborators. The program has been fruitfully applied in many different mathematical disciplines mostly within analysis. We will present here an instance of a recent application in nonlinear operator theory and fixed point theory in which we extract computable information for the approximate common fixed points of one-parameter nonexpansive semigroups on a subset of a Banach space. The results are included in [3] and [2] and obtained via proof mining on a proof in [4]. (A completely different bound had been obtained in [1] (also see [2]) via proof mining on a completely different proof in [5] of a generalization of the statement in [4].) We will also present an example of a metatheorem to illustrate how the extractability of the bound is guaranteed in a specific mathematical context.

15h00-15h30 Coffee break

15h30-16h15 Lars Kristiansen: On b-adic representation of computable irrational numbers

I will discuss some theorems of Specker, Mostowski and myself. If time permits, I will also discuss some variants of b-adic representations.

Contributing talks

We solicit contributions in the fields of PCC, non-exhaustively described above. Please register a contribution at the EasyChair site for PCC 2017: https://easychair.org/conferences/?conf=pcc20170 (still open, please note the trailing zero). This consists in a title, a short text-only abstract and the PDF file of a LaTeX abstract that fits on one page in format A4. (The latter PDF file is not compulsory on first submission.)

PCC is intended to be a lively forum for presenting and discussing recent work. Progress on a not yet satisfactorily solved problem may well be worth presenting - in particular if the discussions during the workshop might lead towards a solution.

Important Dates

• Deadline for proposing a contributed talk: July 3, 2017 (AoE), but the submission server remains still open for some days
• Notification of acceptance: July 10, 2017
• Registration deadline: July 21, 2017

Registration

Committees

PCC steering committee

• Reinhard Kahle, Universidade Nova de Lisboa, Portugal
• Lars Kristiansen, University of Oslo, Norway

Program Committee PCC 2017

• Reinhard Kahle, Universidade Nova de Lisboa, Portugal
• Lars Kristiansen, University of Oslo, Norway
• Ralph Matthes, IRIT, CNRS and Univ. de Toulouse, France
• Isabel Oitavem, Universidade Nova de Lisboa, Portugal

Past PCC workshops

• PCC 2016 was held in Munich, Germany, including a day-long special session to celebrate the 60th birthday of Ulrich Berger.
• PCC 2015 was held in Oslo, Norway, colocated with the Symposium on the occasion of the retirements of Herman Ruge Jervell and Dag Normann.
• PCC 2014 was held in Paris, France, colocated with TYPES 2014.
• PCC 2013 was held in Toulouse, France, colocated with TYPES 2013.
• PCC 2012 was held in Copenhagen, Denmark.
• PCC 2011 was held in Ghent, Belgium.
• PCC 2010 was held in Bern, Switzerland.
• PCC 2009 was held at LORIA - Nancy, France.
• PCC 2008 was held in Oslo, Norway.
• PCC 2007 was held in Swansea, Wales, colocated with the British Mathematical Colloquium 2007.
• PCC 2006 was held in Ilmenau, Germany.
• PCC 2005 was held in Lisbon as affiliated Workshop to ICALP'05.
• PCC 2004 was held in Dresden in conjunction with the Summer School on Proof Theory and Automated Theorem Proving.
• PCC 2003 was held in Dresden, in conjunction with the Summer School on Proof Theory, Computation, and Complexity.
• PCC 2002 was held in Tübingen.

Page maintained by:

Last modified (date in French): lun. juil. 24 10:09:59 CEST 2017