10 Search Results for "Pratt-Hartmann, Ian"


Document
Track B: Automata, Logic, Semantics, and Theory of Programming
On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Authors: Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)


Abstract
We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

Cite as

Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann. On the Limits of Decision: the Adjacent Fragment of First-Order Logic. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 111:1-111:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.ICALP.2023.111,
  author =	{Bednarczyk, Bartosz and Kojelis, Daumantas and Pratt-Hartmann, Ian},
  title =	{{On the Limits of Decision: the Adjacent Fragment of First-Order Logic}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{111:1--111:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.111},
  URN =		{urn:nbn:de:0030-drops-181632},
  doi =		{10.4230/LIPIcs.ICALP.2023.111},
  annote =	{Keywords: decidability, satisfiability, variable-ordered logics, complexity}
}
Document
Adding Transitivity and Counting to the Fluted Fragment

Authors: Ian Pratt-Hartmann and Lidia Tendera

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)


Abstract
We study the impact of adding both counting quantifiers and a single transitive relation to the fluted fragment - a fragment of first-order logic originating in the work of W.V.O. Quine. The resulting formalism can be viewed as a multi-variable, non-guarded extension of certain systems of description logic featuring number restrictions and transitive roles, but lacking role-inverses. We establish the finite model property for our logic, and show that the satisfiability problem for its k-variable sub-fragment is in (k+1)-NExpTime. We also derive ExpSpace-hardness of the satisfiability problem for the two-variable, fluted fragment with one transitive relation (but without counting quantifiers), and prove that, when a second transitive relation is allowed, both the satisfiability and the finite satisfiability problems for the two-variable fluted fragment with counting quantifiers become undecidable.

Cite as

Ian Pratt-Hartmann and Lidia Tendera. Adding Transitivity and Counting to the Fluted Fragment. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 32:1-32:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{pratthartmann_et_al:LIPIcs.CSL.2023.32,
  author =	{Pratt-Hartmann, Ian and Tendera, Lidia},
  title =	{{Adding Transitivity and Counting to the Fluted Fragment}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.32},
  URN =		{urn:nbn:de:0030-drops-174933},
  doi =		{10.4230/LIPIcs.CSL.2023.32},
  annote =	{Keywords: fluted logic, transitivity, counting, satisfiability, decidability, complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Fluted Logic with Counting

Authors: Ian Pratt-Hartmann

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
The fluted fragment is a fragment of first-order logic in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that the fluted fragment possesses the finite model property. In this paper, we extend the fluted fragment by the addition of counting quantifiers. We show that the resulting logic retains the finite model property, and that the satisfiability problem for its (m+1)-variable sub-fragment is in m-NExpTime for all positive m. We also consider the satisfiability and finite satisfiability problems for the extension of any of these fragments in which the fluting requirement applies only to sub-formulas having at least three free variables.

Cite as

Ian Pratt-Hartmann. Fluted Logic with Counting. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 141:1-141:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{pratthartmann:LIPIcs.ICALP.2021.141,
  author =	{Pratt-Hartmann, Ian},
  title =	{{Fluted Logic with Counting}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{141:1--141:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.141},
  URN =		{urn:nbn:de:0030-drops-142101},
  doi =		{10.4230/LIPIcs.ICALP.2021.141},
  annote =	{Keywords: Fluted fragment, counting quantifiers, satisfiability, complexity}
}
Document
Verified Decision Procedures for Modal Logics

Authors: Minchao Wu and Rajeev Goré

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We describe a formalization of modal tableaux with histories for the modal logics K, KT and S4 in Lean. We describe how we formalized the static and transitional rules, the non-trivial termination and the correctness of loop-checks. The formalized tableaux are essentially executable decision procedures with soundness and completeness proved. Termination is also proved in order to define them as functions in Lean. All of these decision procedures return a concrete Kripke model in cases where the input set of formulas is satisfiable, and a proof constructed via the tableau rules witnessing unsatisfiability otherwise. We also describe an extensible formalization of backjumping and its verified implementation for the modal logic K. As far as we know, these are the first verified decision procedures for these modal logics.

Cite as

Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{wu_et_al:LIPIcs.ITP.2019.31,
  author =	{Wu, Minchao and Gor\'{e}, Rajeev},
  title =	{{Verified Decision Procedures for Modal Logics}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.31},
  URN =		{urn:nbn:de:0030-drops-110866},
  doi =		{10.4230/LIPIcs.ITP.2019.31},
  annote =	{Keywords: Formal Methods, Interactive Theorem Proving, Modal Logic, Lean}
}
Document
Short Paper
lambdaProlog(QS): Functional Spatial Reasoning in Higher Order Logic Programming (Short Paper)

Authors: Beidi Li, Mehul Bhatt, and Carl Schultz

Published in: LIPIcs, Volume 142, 14th International Conference on Spatial Information Theory (COSIT 2019)


Abstract
We present a framework and proof-of-concept implementation for functional spatial reasoning within high-order logic programming. The developed approach extends lambdaProlog to support reasoning over spatial variables via Constraint Handling Rules. We implement our approach within Embeddable lambdaProlog Interpreter (ELPI) and demonstrate key features from combined reasoning over spatial functions and relations. The reported research is an ongoing development of the declarative spatial reasoning paradigm.

Cite as

Beidi Li, Mehul Bhatt, and Carl Schultz. lambdaProlog(QS): Functional Spatial Reasoning in Higher Order Logic Programming (Short Paper). In 14th International Conference on Spatial Information Theory (COSIT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 142, pp. 26:1-26:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.COSIT.2019.26,
  author =	{Li, Beidi and Bhatt, Mehul and Schultz, Carl},
  title =	{{lambdaProlog(QS): Functional Spatial Reasoning in Higher Order Logic Programming}},
  booktitle =	{14th International Conference on Spatial Information Theory (COSIT 2019)},
  pages =	{26:1--26:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-115-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{142},
  editor =	{Timpf, Sabine and Schlieder, Christoph and Kattenbeck, Markus and Ludwig, Bernd and Stewart, Kathleen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2019.26},
  URN =		{urn:nbn:de:0030-drops-111183},
  doi =		{10.4230/LIPIcs.COSIT.2019.26},
  annote =	{Keywords: Spatial reasoning, Functional logic programming, Lambda-Prolog}
}
Document
The Fluted Fragment with Transitivity

Authors: Ian Pratt-Hartmann and Lidia Tendera

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Cite as

Ian Pratt-Hartmann and Lidia Tendera. The Fluted Fragment with Transitivity. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{pratthartmann_et_al:LIPIcs.MFCS.2019.18,
  author =	{Pratt-Hartmann, Ian and Tendera, Lidia},
  title =	{{The Fluted Fragment with Transitivity}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{18:1--18:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.18},
  URN =		{urn:nbn:de:0030-drops-109626},
  doi =		{10.4230/LIPIcs.MFCS.2019.18},
  annote =	{Keywords: First-Order logic, Decidability, Satisfiability, Transitivity, Complexity}
}
Document
Quine's Fluted Fragment is Non-Elementary

Authors: Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)


Abstract
We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.

Cite as

Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. Quine's Fluted Fragment is Non-Elementary. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 39:1-39:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{pratthartmann_et_al:LIPIcs.CSL.2016.39,
  author =	{Pratt-Hartmann, Ian and Szwast, Wieslaw and Tendera, Lidia},
  title =	{{Quine's Fluted Fragment is Non-Elementary}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.39},
  URN =		{urn:nbn:de:0030-drops-65791},
  doi =		{10.4230/LIPIcs.CSL.2016.39},
  annote =	{Keywords: Quine, fluted fragment, Purdy, non-elementary, satisfiability, decidability}
}
Document
Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra

Authors: Toshiki Kataoka and Dusko Pavlovic

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)


Abstract
While computer programs and logical theories begin by declaring the concepts of interest, be it as data types or as predicates, network computation does not allow such global declarations, and requires concept mining and concept analysis to extract shared semantics for different network nodes. Powerful semantic analysis systems have been the drivers of nearly all paradigm shifts on the web. In categorical terms, most of them can be described as bicompletions of enriched matrices, generalizing the Dedekind-MacNeille-style completions from posets to suitably enriched categories. Yet it has been well known for more than 40 years that ordinary categories themselves in general do not permit such completions. Armed with this new semantical view of Dedekind-MacNeille completions, and of matrix bicompletions, we take another look at this ancient mystery. It turns out that simple categorical versions of the limit superior and limit inferior operations characterize a general notion of Dedekind-MacNeille completion, that seems to be appropriate for ordinary categories, and boils down to the more familiar enriched versions when the limits inferior and superior coincide. This explains away the apparent gap among the completions of ordinary categories, and broadens the path towards categorical concept mining and analysis, opened in previous work.

Cite as

Toshiki Kataoka and Dusko Pavlovic. Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 130-155, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{kataoka_et_al:LIPIcs.CALCO.2015.130,
  author =	{Kataoka, Toshiki and Pavlovic, Dusko},
  title =	{{Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{130--155},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.130},
  URN =		{urn:nbn:de:0030-drops-55317},
  doi =		{10.4230/LIPIcs.CALCO.2015.130},
  annote =	{Keywords: concept analysis, semantic indexing, category, completion, algebra}
}
Document
Two-variable Logic with Counting and a Linear Order

Authors: Witold Charatonik and Piotr Witkowski

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


Abstract
We study the finite satisfiability problem for the two-variable fragment of the first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and its successor, in presence of other binary predicate symbols, is decidable, but it is as expressive (and as complex) as Vector Addition Systems.

Cite as

Witold Charatonik and Piotr Witkowski. Two-variable Logic with Counting and a Linear Order. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 631-647, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{charatonik_et_al:LIPIcs.CSL.2015.631,
  author =	{Charatonik, Witold and Witkowski, Piotr},
  title =	{{Two-variable Logic with Counting and a Linear Order}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{631--647},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.631},
  URN =		{urn:nbn:de:0030-drops-54436},
  doi =		{10.4230/LIPIcs.CSL.2015.631},
  annote =	{Keywords: Two-variable logic, counting quantifiers, linear order, satisfiability, complexity}
}
Document
From TimeML to TPL

Authors: Ian Pratt-Hartmann

Published in: Dagstuhl Seminar Proceedings, Volume 5151, Annotating, Extracting and Reasoning about Time and Events (2005)


Abstract
This paper describes a subset of the temporal mark-up language TimeML, and explains its relation to various formalisms found in the literature on interval temporal logic. The subset of TimeML we describe can be viewed as an interval temporal logic with a tractable satisfiability problem, but very limited expressive power. Most crucially, that logic does not permit quantification over events. The contribution of this paper is to point out that, by choosing an appropriate interval temporal logic, it is possible to introduce quantification into representations of event-structure without sacrificing decidability.

Cite as

Ian Pratt-Hartmann. From TimeML to TPL. In Annotating, Extracting and Reasoning about Time and Events. Dagstuhl Seminar Proceedings, Volume 5151, pp. 1-11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2005)


Copy BibTex To Clipboard

@InProceedings{pratthartmann:DagSemProc.05151.8,
  author =	{Pratt-Hartmann, Ian},
  title =	{{From TimeML to TPL}},
  booktitle =	{Annotating, Extracting and Reasoning about Time and Events},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5151},
  editor =	{Graham Katz and James Pustejovsky and Frank Schilder},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05151.8},
  URN =		{urn:nbn:de:0030-drops-3128},
  doi =		{10.4230/DagSemProc.05151.8},
  annote =	{Keywords: Information Extraction, Interval temporal logic}
}
  • Refine by Author
  • 6 Pratt-Hartmann, Ian
  • 3 Tendera, Lidia
  • 1 Bednarczyk, Bartosz
  • 1 Bhatt, Mehul
  • 1 Charatonik, Witold
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Complexity theory and logic
  • 2 Theory of computation → Finite Model Theory
  • 1 Computing methodologies → Spatial and physical reasoning
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 5 satisfiability
  • 4 complexity
  • 3 decidability
  • 2 counting quantifiers
  • 1 Complexity
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 3 2019
  • 2 2015
  • 2 2023
  • 1 2005
  • 1 2016
  • Show More...

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