5 Search Results for "M�ry, Dominique"

Document
DOI: 10.4230/LIPIcs.CSL.2024.29
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions

Authors: Yannick Forster, Dominik Kirst, and Niklas Mück

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.
Cite as

Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2024.29,
  author =	{Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas},
  title =	{{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29},
  URN =		{urn:nbn:de:0030-drops-196728},
  doi =		{10.4230/LIPIcs.CSL.2024.29},
  annote =	{Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2021.36
Filling Crosswords Is Very Hard

Authors: Laurent Gourvès, Ararat Harutyunyan, Michael Lampis, and Nikolaos Melissinos

Published in: LIPIcs, Volume 212, 32nd International Symposium on Algorithms and Computation (ISAAC 2021)

Abstract
We revisit a classical crossword filling puzzle which already appeared in Garey&Jonhson’s book. We are given a grid with n vertical and horizontal slots and a dictionary with m words and are asked to place words from the dictionary in the slots so that shared cells are consistent. We attempt to pinpoint the source of intractability of this problem by carefully taking into account the structure of the grid graph, which contains a vertex for each slot and an edge if two slots intersect. Our main approach is to consider the case where this graph has a tree-like structure. Unfortunately, if we impose the common rule that words cannot be reused, we discover that the problem remains NP-hard under very severe structural restrictions, namely, if the grid graph is a union of stars and the alphabet has size 2, or the grid graph is a matching (so the crossword is a collection of disjoint crosses) and the alphabet has size 3. The problem does become slightly more tractable if word reuse is allowed, as we obtain an m^{tw} algorithm in this case, where tw is the treewidth of the grid graph. However, even in this case, we show that our algorithm cannot be improved to obtain fixed-parameter tractability. More strongly, we show that under the ETH the problem cannot be solved in time m^o(k), where k is the number of horizontal slots of the instance (which trivially bounds tw). Motivated by these mostly negative results, we also consider the much more restricted case where the problem is parameterized by the number of slots n. Here, we show that the problem does become FPT (if the alphabet has constant size), but the parameter dependence is exponential in n². We show that this dependence is also justified: the existence of an algorithm with running time 2^o(n²), even for binary alphabet, would contradict the randomized ETH. Finally, we consider an optimization version of the problem, where we seek to place as many words on the grid as possible. Here it is easy to obtain a 1/2-approximation, even on weighted instances, simply by considering only horizontal or only vertical slots. We show that this trivial algorithm is also likely to be optimal, as obtaining a better approximation ratio in polynomial time would contradict the Unique Games Conjecture. The latter two results apply whether word reuse is allowed or not.
Cite as

Laurent Gourvès, Ararat Harutyunyan, Michael Lampis, and Nikolaos Melissinos. Filling Crosswords Is Very Hard. In 32nd International Symposium on Algorithms and Computation (ISAAC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 212, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{gourves_et_al:LIPIcs.ISAAC.2021.36,
  author =	{Gourv\`{e}s, Laurent and Harutyunyan, Ararat and Lampis, Michael and Melissinos, Nikolaos},
  title =	{{Filling Crosswords Is Very Hard}},
  booktitle =	{32nd International Symposium on Algorithms and Computation (ISAAC 2021)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-214-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{212},
  editor =	{Ahn, Hee-Kap and Sadakane, Kunihiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2021.36},
  URN =		{urn:nbn:de:0030-drops-154690},
  doi =		{10.4230/LIPIcs.ISAAC.2021.36},
  annote =	{Keywords: Crossword Puzzle, Treewidth, ETH}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2021.17
Tracing Isomanifolds in ℝ^d in Time Polynomial in d Using Coxeter-Freudenthal-Kuhn Triangulations

Authors: Jean-Daniel Boissonnat, Siargey Kachanovich, and Mathijs Wintraecken

Published in: LIPIcs, Volume 189, 37th International Symposium on Computational Geometry (SoCG 2021)

Abstract
Isomanifolds are the generalization of isosurfaces to arbitrary dimension and codimension, i.e. submanifolds of ℝ^d defined as the zero set of some multivariate multivalued smooth function f: ℝ^d → ℝ^{d-n}, where n is the intrinsic dimension of the manifold. A natural way to approximate a smooth isomanifold M is to consider its Piecewise-Linear (PL) approximation M̂ based on a triangulation 𝒯 of the ambient space ℝ^d. In this paper, we describe a simple algorithm to trace isomanifolds from a given starting point. The algorithm works for arbitrary dimensions n and d, and any precision D. Our main result is that, when f (or M) has bounded complexity, the complexity of the algorithm is polynomial in d and δ = 1/D (and unavoidably exponential in n). Since it is known that for δ = Ω (d^{2.5}), M̂ is O(D²)-close and isotopic to M, our algorithm produces a faithful PL-approximation of isomanifolds of bounded complexity in time polynomial in d. Combining this algorithm with dimensionality reduction techniques, the dependency on d in the size of M̂ can be completely removed with high probability. We also show that the algorithm can handle isomanifolds with boundary and, more generally, isostratifolds. The algorithm for isomanifolds with boundary has been implemented and experimental results are reported, showing that it is practical and can handle cases that are far ahead of the state-of-the-art.
Cite as

Jean-Daniel Boissonnat, Siargey Kachanovich, and Mathijs Wintraecken. Tracing Isomanifolds in ℝ^d in Time Polynomial in d Using Coxeter-Freudenthal-Kuhn Triangulations. In 37th International Symposium on Computational Geometry (SoCG 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 189, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{boissonnat_et_al:LIPIcs.SoCG.2021.17,
  author =	{Boissonnat, Jean-Daniel and Kachanovich, Siargey and Wintraecken, Mathijs},
  title =	{{Tracing Isomanifolds in \mathbb{R}^d in Time Polynomial in d Using Coxeter-Freudenthal-Kuhn Triangulations}},
  booktitle =	{37th International Symposium on Computational Geometry (SoCG 2021)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-184-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{189},
  editor =	{Buchin, Kevin and Colin de Verdi\`{e}re, \'{E}ric},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2021.17},
  URN =		{urn:nbn:de:0030-drops-138163},
  doi =		{10.4230/LIPIcs.SoCG.2021.17},
  annote =	{Keywords: Coxeter triangulation, Kuhn triangulation, permutahedron, PL-approximations, isomanifolds/solution manifolds/isosurfacing}
}
Document
DOI: 10.4230/DagRep.4.2.17
The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)

Authors: Dominique Méry, Bernhard Schätz, and Alan Wassyng

Published in: Dagstuhl Reports, Volume 4, Issue 2 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14062 "The Pacemaker Challenge: Developing Certifiable Medical Devices". The aim of the seminar was to bring together leading researchers and industrial partners of this field; the seminary ended up with 24 participants from 8 countries: Canada, Denmark, France, The Unites States, Germany, United Kingdom, Brazil. Through a series of presentations, discussions, and working group meetings, the seminar attempted to get a general view of the field of medical devices and certification issues through the pacemaker challenge. The seminar brought together, on the one hand, researchers from the different notations and various tools. The main outcome of the seminar is the exchange of information between different groups and the project of a book.
Cite as

Dominique Méry, Bernhard Schätz, and Alan Wassyng. The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062). In Dagstuhl Reports, Volume 4, Issue 2, pp. 17-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{mery_et_al:DagRep.4.2.17,
  author =	{M\'{e}ry, Dominique and Sch\"{a}tz, Bernhard and Wassyng, Alan},
  title =	{{The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062)}},
  pages =	{17--37},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{2},
  editor =	{M\'{e}ry, Dominique and Sch\"{a}tz, Bernhard and Wassyng, Alan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.2.17},
  URN =		{urn:nbn:de:0030-drops-45436},
  doi =		{10.4230/DagRep.4.2.17},
  annote =	{Keywords: Embedded systems, Real-time systems, Medical devices, Model-driven development, Software certification, Validation \& verification, Formal methods}
}
Document
DOI: 10.4230/DagSemProc.06021.8
Robustness and Randomness

Authors: Dominique Michelucci, Jean Michel Moreau, and Sebti Foufou

Published in: Dagstuhl Seminar Proceedings, Volume 6021, Reliable Implementation of Real Number Algorithms: Theory and Practice (2006)

Abstract
Robustness problems of computational geometry algorithms is a topic that has been subject to intensive research efforts from both computer science and mathematics communities. Robustness problems are caused by the lack of precision in computations involving floating-point instead of real numbers. This paper reviews methods dealing with robustness and inaccuracy problems. It discussed approaches based on exact arithmetic, interval arithmetic and probabilistic methods. The paper investigates the possibility to use randomness at certain levels of reasoning to make geometric constructions more robust.
Cite as

Dominique Michelucci, Jean Michel Moreau, and Sebti Foufou. Robustness and Randomness. In Reliable Implementation of Real Number Algorithms: Theory and Practice. Dagstuhl Seminar Proceedings, Volume 6021, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{michelucci_et_al:DagSemProc.06021.8,
  author =	{Michelucci, Dominique and Moreau, Jean Michel and Foufou, Sebti},
  title =	{{Robustness and Randomness}},
  booktitle =	{Reliable Implementation of Real Number Algorithms: Theory and Practice},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6021},
  editor =	{Peter Hertling and Christoph M. Hoffmann and Wolfram Luther and Nathalie Revol},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06021.8},
  URN =		{urn:nbn:de:0030-drops-7167},
  doi =		{10.4230/DagSemProc.06021.8},
  annote =	{Keywords: Robustness, interval, randomness, inaccuracy, geometric computation}
}
  • Refine by Author
  • 1 Boissonnat, Jean-Daniel
  • 1 Forster, Yannick
  • 1 Foufou, Sebti
  • 1 Gourvès, Laurent
  • 1 Harutyunyan, Ararat
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Approximation algorithms analysis
  • 1 Theory of computation → Computational geometry
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Parameterized complexity and exact algorithms
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Computability theory
  • 1 Constructive mathematics
  • 1 Constructive type theory
  • 1 Coq proof assistant
  • 1 Coxeter triangulation
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2021
  • 1 2006
  • 1 2014
  • 1 2024

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