Search Results

Documents authored by Fernández-Duque, David

Document
DOI: 10.4230/LIPIcs.CSL.2025.25
Exponential Lower Bounds on Definable Fixed Points

Authors: Konstantinos Papafilippou and David Fernández-Duque

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
It is known that the μ-calculus is no more expressive than basic modal logic over the class of finite partial orders, as well as over the class of finite, strict partial orders. Nevertheless, we show that the μ-calculus is exponentially more succinct, even when a reflexive modality is added as primitive. As corollaries, we obtain a lower bound for the fixed-point theorem for Gödel-Löb logic and a variant for Grzegorczyk logic, as well as lower bounds on interpolants for the interpolation theorem of Gödel-Löb logic.
Cite as

Konstantinos Papafilippou and David Fernández-Duque. Exponential Lower Bounds on Definable Fixed Points. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{papafilippou_et_al:LIPIcs.CSL.2025.25,
  author =	{Papafilippou, Konstantinos and Fern\'{a}ndez-Duque, David},
  title =	{{Exponential Lower Bounds on Definable Fixed Points}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.25},
  URN =		{urn:nbn:de:0030-drops-227827},
  doi =		{10.4230/LIPIcs.CSL.2025.25},
  annote =	{Keywords: Modal logic, Provability Logic, Fixed-Point Theorem, mu-calculus, Interpolation, Succinctness}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.19
Dynamic Cantor Derivative Logic

Authors: David Fernández-Duque and Yoàv Montacute

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
Topological semantics for modal logic based on the Cantor derivative operator gives rise to derivative logics, also referred to as d-logics. Unlike logics based on the topological closure operator, d-logics have not previously been studied in the framework of dynamical systems, which are pairs (X,f) consisting of a topological space X equipped with a continuous function f: X → X. We introduce the logics wK4C, K4C and GLC and show that they all have the finite Kripke model property and are sound and complete with respect to the d-semantics in this dynamical setting. In particular, we prove that wK4C is the d-logic of all dynamic topological systems, K4C is the d-logic of all T_D dynamic topological systems, and GLC is the d-logic of all dynamic topological systems based on a scattered space. We also prove a general result for the case where f is a homeomorphism, which in particular yields soundness and completeness for the corresponding systems wK4H, K4H and GLH. The main contribution of this work is the foundation of a general proof method for finite model property and completeness of dynamic topological d-logics. Furthermore, our result for GLC constitutes the first step towards a proof of completeness for the trimodal topo-temporal language with respect to a finite axiomatisation - something known to be impossible over the class of all spaces.
Cite as

David Fernández-Duque and Yoàv Montacute. Dynamic Cantor Derivative Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fernandezduque_et_al:LIPIcs.CSL.2022.19,
  author =	{Fern\'{a}ndez-Duque, David and Montacute, Yo\`{a}v},
  title =	{{Dynamic Cantor Derivative Logic}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.19},
  URN =		{urn:nbn:de:0030-drops-157397},
  doi =		{10.4230/LIPIcs.CSL.2022.19},
  annote =	{Keywords: dynamic topological logic, Cantor derivative, temporal logic, modal logic}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.6
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors: Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.
Cite as

Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6,
  author =	{de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.},
  title =	{{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6},
  URN =		{urn:nbn:de:0030-drops-113649},
  doi =		{10.4230/LIPIcs.TIME.2019.6},
  annote =	{Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.14
A Decidable Intuitionistic Temporal Logic

Authors: Joseph Boudou, Martín Diéguez, and David Fernández-Duque

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We introduce the logic ITL^e, an intuitionistic temporal logic based on structures (W,R,S), where R is used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITL^e are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a 'persistent' version of the logic, ITL^p, whose models are similar to Cartesian products. We prove that, unlike ITL^e, ITL^p does not have the finite model property.
Cite as

Joseph Boudou, Martín Diéguez, and David Fernández-Duque. A Decidable Intuitionistic Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{boudou_et_al:LIPIcs.CSL.2017.14,
  author =	{Boudou, Joseph and Di\'{e}guez, Mart{\'\i}n and Fern\'{a}ndez-Duque, David},
  title =	{{A Decidable Intuitionistic Temporal Logic}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.14},
  URN =		{urn:nbn:de:0030-drops-77016},
  doi =		{10.4230/LIPIcs.CSL.2017.14},
  annote =	{Keywords: intuitionistic logic, temporal logic, products of modal logics}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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