Search Results

Documents authored by Jung, Jean Christoph

Document
DOI: 10.4230/LIPIcs.STACS.2025.55
Modal Separation of Fixpoint Formulae

Authors: Jean Christoph Jung and Jędrzej Kołodziejski

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae φ,φ' whether there is a modal formula ψ that separates them, in the sense that φ ⊧ ψ and ψ ⊧ ¬φ'. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree ≤ 1, ExpTime-complete over unrestricted and over binary models, and 2-ExpTime-complete over models of outdegree bounded by some d ≥ 3. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also investigate the problem of efficient construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.
Cite as

Jean Christoph Jung and Jędrzej Kołodziejski. Modal Separation of Fixpoint Formulae. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.STACS.2025.55,
  author =	{Jung, Jean Christoph and Ko{\l}odziejski, J\k{e}drzej},
  title =	{{Modal Separation of Fixpoint Formulae}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{55:1--55:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.55},
  URN =		{urn:nbn:de:0030-drops-228804},
  doi =		{10.4230/LIPIcs.STACS.2025.55},
  annote =	{Keywords: Modal Logic, Fixpoint Logic, Separability, Interpolation}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.31
QBF Programming with the Modeling Language Bule

Authors: Jean Christoph Jung, Valentin Mayer-Eichberger, and Abdallah Saffidine

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF) - that is, propositional formulas in which the variables are existentially or universally quantified. Bule allows the user to write a high-level representation of the problem in a natural, rule-based language, that is inspired by stratified Datalog. We implemented a tool of the same name that converts the high-level representation into DIMACS format and thus provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity-theoretic properties of our modeling language, provide a library for common modeling patterns, and evaluate our language and tool on several examples.
Cite as

Jean Christoph Jung, Valentin Mayer-Eichberger, and Abdallah Saffidine. QBF Programming with the Modeling Language Bule. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.SAT.2022.31,
  author =	{Jung, Jean Christoph and Mayer-Eichberger, Valentin and Saffidine, Abdallah},
  title =	{{QBF Programming with the Modeling Language Bule}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{31:1--31:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.31},
  URN =		{urn:nbn:de:0030-drops-167058},
  doi =		{10.4230/LIPIcs.SAT.2022.31},
  annote =	{Keywords: Modeling, QBF Programming, CNF Encodings}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ICDT.2020
LIPIcs, Vol. 155, ICDT 2020, Complete Volume

Authors: Carsten Lutz and Jean Christoph Jung

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)

Abstract
LIPIcs, Vol. 155, ICDT 2020, Complete Volume
Cite as

23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 1-454, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{lutz_et_al:LIPIcs.ICDT.2020,
  title =	{{LIPIcs, Vol. 155, ICDT 2020, Complete Volume}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{1--454},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020},
  URN =		{urn:nbn:de:0030-drops-119239},
  doi =		{10.4230/LIPIcs.ICDT.2020},
  annote =	{Keywords: LIPIcs, Vol. 155, ICDT 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ICDT.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Carsten Lutz and Jean Christoph Jung

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lutz_et_al:LIPIcs.ICDT.2020.0,
  author =	{Lutz, Carsten and Jung, Jean Christoph},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.0},
  URN =		{urn:nbn:de:0030-drops-119244},
  doi =		{10.4230/LIPIcs.ICDT.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2018.15
Querying the Unary Negation Fragment with Regular Path Expressions

Authors: Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider

Published in: LIPIcs, Volume 98, 21st International Conference on Database Theory (ICDT 2018)

Abstract
The unary negation fragment of first-order logic (UNFO) has recently been proposed as a generalization of modal logic that shares many of its good computational and model-theoretic properties. It is attractive from the perspective of database theory because it can express conjunctive queries (CQs) and ontologies formulated in many description logics (DLs). Both are relevant for ontology-mediated querying and, in fact, CQ evaluation under UNFO ontologies (and thus also under DL ontologies) can be `expressed' in UNFO as a satisfiability problem. In this paper, we consider the natural extension of UNFO with regular expressions on binary relations. The resulting logic UNFOreg can express (unions of) conjunctive two-way regular path queries (C2RPQs) and ontologies formulated in DLs that include transitive roles and regular expressions on roles. Our main results are that evaluating C2RPQs under UNFOreg ontologies is decidable, 2ExpTime-complete in combined complexity, and coNP-complete in data complexity, and that satisfiability in UNFOreg is 2ExpTime-complete, thus not harder than in UNFO.
Cite as

Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider. Querying the Unary Negation Fragment with Regular Path Expressions. In 21st International Conference on Database Theory (ICDT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 98, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.ICDT.2018.15,
  author =	{Jung, Jean Christoph and Lutz, Carsten and Martel, Mauricio and Schneider, Thomas},
  title =	{{Querying the Unary Negation Fragment with Regular Path Expressions}},
  booktitle =	{21st International Conference on Database Theory (ICDT 2018)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-063-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{98},
  editor =	{Kimelfeld, Benny and Amsterdamer, Yael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2018.15},
  URN =		{urn:nbn:de:0030-drops-85971},
  doi =		{10.4230/LIPIcs.ICDT.2018.15},
  annote =	{Keywords: Query Answering, Regular Path Queries, Decidable Fragments of First-Order Logic, Computational Complexity}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.108
Conservative Extensions in Guarded and Two-Variable Fragments

Authors: Jean Christoph Jung, Carsten Lutz, Mauricio Martel, Thomas Schneider, and Frank Wolter

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO2 and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO2 or GF (even the three-variable fragment thereof), and that they are decidable and 2ExpTime-complete in the intersection GF2 of FO2 and GF.
Cite as

Jean Christoph Jung, Carsten Lutz, Mauricio Martel, Thomas Schneider, and Frank Wolter. Conservative Extensions in Guarded and Two-Variable Fragments. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 108:1-108:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.ICALP.2017.108,
  author =	{Jung, Jean Christoph and Lutz, Carsten and Martel, Mauricio and Schneider, Thomas and Wolter, Frank},
  title =	{{Conservative Extensions in Guarded and Two-Variable Fragments}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{108:1--108:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.108},
  URN =		{urn:nbn:de:0030-drops-74647},
  doi =		{10.4230/LIPIcs.ICALP.2017.108},
  annote =	{Keywords: Conservative Extensions, Decidable Fragments of First-Order Logic, Computational Complexity\}}
}
Document
DOI: 10.4230/DagSemProc.09461.5
SWORD – Module-based SAT Solving

Authors: Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
Cite as

Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler. SWORD – Module-based SAT Solving. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{wille_et_al:DagSemProc.09461.5,
  author =	{Wille, Robert and Jung, Jean Christoph and S\"{u}lflow, Andre and Drechsler, Rolf},
  title =	{{SWORD – Module-based SAT Solving}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.5},
  URN =		{urn:nbn:de:0030-drops-25069},
  doi =		{10.4230/DagSemProc.09461.5},
  annote =	{Keywords: SAT Solver, Word Level, SAT Modulo Theories}
}
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 About DROPS Imprint Privacy Contact