DROPS

Document

From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)

Authors: Ingo Blechschmidt, Hajime Ishihara, Peter M. Schuster, and Gabriele Buriola

Published in: Dagstuhl Reports, Volume 14, Issue 1 (2024)

Abstract

What is the computational content of proofs? This is one of the main topics in mathematical logic, especially proof theory, that is of relevance for computer science. The well-known foundational solutions aim at rebuilding mathematics constructively almost from scratch, and include Bishop-style constructive mathematics and Martin-Löf’s intuitionistic type theory, the latter most recently in the form of the so-called homotopy or univalent type theory put forward by Voevodsky. From a more practical angle, however, the question rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. Ideally, all this is done by manipulating proofs mechanically and/or by adequate metatheorems (proof translations, automated theorem proving, program extraction from proofs, proof mining, etc.). A crucial role for answering these questions is played by coherent and geometric theories and their generalizations: not only that they are fairly widespread in modern mathematics and non-classical logics (e.g., in abstract algebra, and in temporal and modal logics); those theories are also a priori amenable for constructivisation (see Barr’s Theorem, especially its proof-theoretic variants, and the numerous Glivenko–style theorems); last but not least, effective theorem-proving for coherent theories can be automated with relative ease and clarity in relation to resolution. Specific topics that substantially involve computer science research include categorical semantics for geometric theories up to the proof-theoretic presentation of sheaf models and higher toposes; extracting the computational content of proofs and dynamical methods in quadratic form theory; the interpretation of transfinite proof methods as latent computations; complexity issues of and algorithms for geometrization of theories; the use of geometric theories in constructive mathematics including finding algorithms, ideally with integrated developments; and coherent logic for obtaining automatically readable proofs.

Cite as

Ingo Blechschmidt, Hajime Ishihara, Peter M. Schuster, and Gabriele Buriola. From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021). In Dagstuhl Reports, Volume 14, Issue 1, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{blechschmidt_et_al:DagRep.14.1.1,
  author =	{Blechschmidt, Ingo and Ishihara, Hajime and Schuster, Peter M. and Buriola, Gabriele},
  title =	{{From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{1},
  editor =	{Blechschmidt, Ingo and Ishihara, Hajime and Schuster, Peter M. and Buriola, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.1},
  URN =		{urn:nbn:de:0030-drops-204882},
  doi =		{10.4230/DagRep.14.1.1},
  annote =	{Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}

Document

DOI: 10.4230/DagRep.11.10.151

Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)

Authors: Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)

Abstract

At least from a practical and contemporary angle, the time-honoured question about the extent of intuitionistic mathematics rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. All this is ideally done by manipulating proofs mechanically or by adequate metatheorems, which includes proof translations, automated theorem proving, program extraction from proofs, proof analysis and proof mining. The question should thus be put as: What is the computational content of proofs? Guided by this central question, the present Dagstuhl seminar puts a special focus on coherent and geometric theories and their generalisations. These are not only widespread in mathematics and non-classical logics such as temporal and modal logics, but also a priori amenable for constructivisation, e.g., by Barr’s Theorem, and last but not least particularly suited as a basis for automated theorem proving. Specific topics include categorical semantics for geometric theories, complexity issues of and algorithms for geometrisation of theories including speed-up questions, the use of geometric theories in constructive mathematics including finding algorithms, proof-theoretic presentation of sheaf models and higher toposes, and coherent logic for automatically readable proofs.

Cite as

Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster. Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). In Dagstuhl Reports, Volume 11, Issue 10, pp. 151-172, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{coquand_et_al:DagRep.11.10.151,
  author =	{Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
  title =	{{Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)}},
  pages =	{151--172},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{10},
  editor =	{Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.10.151},
  URN =		{urn:nbn:de:0030-drops-159321},
  doi =		{10.4230/DagRep.11.10.151},
  annote =	{Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}

Search Results

Documents authored by Schuster, Peter M.

From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)

Abstract

Cite as

Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)

Abstract

Cite as

Thanks for your feedback!

Could not send message