3 Search Results for "Ishihara, Hajime"

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/LIPIcs.FSCD.2020.25
A Gentzen-Style Monadic Translation of Gödel’s System T

Authors: Chuangjie Xu

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We introduce a syntactic translation of Gödel’s System 𝖳 parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen’s negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of 𝖳-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.
Cite as

Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 25:1-25:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{xu:LIPIcs.FSCD.2020.25,
  author =	{Xu, Chuangjie},
  title =	{{A Gentzen-Style Monadic Translation of G\"{o}del’s System T}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.25},
  URN =		{urn:nbn:de:0030-drops-123472},
  doi =		{10.4230/LIPIcs.FSCD.2020.25},
  annote =	{Keywords: monadic translation, G\"{o}del’s System T, logical relation, negative translation, majorizability, continuity, bar recursion, Agda}
}
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}
}
  • Refine by Author
  • 2 Ishihara, Hajime
  • 1 Bridges, Douglas
  • 1 Coquand, Thierry
  • 1 Negri, Sara
  • 1 Schuster, Peter
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Proof theory
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Program analysis
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Agda
  • 1 Apartness
  • 1 Gödel’s System T
  • 1 automated theorem proving
  • 1 bar recursion
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2005
  • 1 2020
  • 1 2022

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact