Search Results

Documents authored by Ishihara, Hajime

Document
DOI: 10.4230/DagRep.14.1.1
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}
}
Document
DOI: 10.4230/DagSemProc.04351.9
Compactness in apartness spaces?

Authors: Douglas Bridges, Hajime Ishihara, Peter Schuster, and Luminita S. Vita

Published in: Dagstuhl Seminar Proceedings, Volume 4351, Spatial Representation: Discrete vs. Continuous Computational Models (2005)

Abstract
A major problem in the constructive theory of apartness spaces is that of finding a good notion of compactness. Such a notion should (i) reduce to ``complete plus totally bounded'' for uniform spaces and (ii) classically be equivalent to the usual Heine-Borel-Lebesgue property for the apartness topology. The constructive counterpart of the smallest uniform structure compatible with a given apartness, while not constructively a uniform structure, offers a possible solution to the compactness-definition problem. That counterpart turns out to be interesting in its own right, and reveals some additional properties of an apartness that may have uses elsewhere in the theory.
Cite as

Douglas Bridges, Hajime Ishihara, Peter Schuster, and Luminita S. Vita. Compactness in apartness spaces?. In Spatial Representation: Discrete vs. Continuous Computational Models. Dagstuhl Seminar Proceedings, Volume 4351, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{bridges_et_al:DagSemProc.04351.9,
  author =	{Bridges, Douglas and Ishihara, Hajime and Schuster, Peter and Vita, Luminita S.},
  title =	{{Compactness in apartness spaces?}},
  booktitle =	{Spatial Representation: Discrete vs. Continuous Computational Models},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4351},
  editor =	{Ralph Kopperman and Michael B. Smyth and Dieter Spreen and Julian Webster},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04351.9},
  URN =		{urn:nbn:de:0030-drops-1175},
  doi =		{10.4230/DagSemProc.04351.9},
  annote =	{Keywords: Apartness , constructive , compact uniform space}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact