Arrow Research search

Author name cluster

David Fernández-Duque

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

22 papers
2 author rows

Possible papers

22

CSL Conference 2025 Conference Paper

Exponential Lower Bounds on Definable Fixed Points

  • Konstantinos Papafilippou
  • David Fernández-Duque

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.

Details

AIJ Journal 2025 Journal Article

Gödel–Dummett linear temporal logic

  • Juan Pablo Aguilera
  • Martín Diéguez
  • David Fernández-Duque
  • Brett McLean

We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This Gödel temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that Gödel temporal logic is PSPACE-complete. We also provide a deductive calculus for Gödel temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus.

Details DOI

AIJ Journal 2025 Journal Article

The topology of surprise

  • Alexandru Baltag
  • Nick Bezhanishvili
  • David Fernández-Duque

In this paper we present a topological epistemic logic, with modalities for knowledge (modelled as the universal modality), knowability (represented by the topological interior operator), and unknowability of the actual world. The last notion has a non-self-referential reading (modelled by Cantor derivative: the set of limit points of a given set) and a self-referential one (modelled by Cantor's perfect core of a given set: its largest subset without isolated points, where x is isolated iff { x } is open). We completely axiomatize this logic, showing that it is decidable and pspace-complete, and we apply it to the analysis of a famous epistemic puzzle: the Surprise Exam Paradox.

Details DOI

KR Conference 2024 Conference Paper

A Sound and Complete Axiomatisation for Intuitionistic Linear Temporal Logic

  • David Fernández-Duque
  • Brett McLean
  • Lukas Zenger

Intuitionistic linear temporal logic (iLTL) has been studied extensively, especially in the last decade. It enjoys natural semantics over intuitionistic Kripke frames equipped with an order-preserving function representing the temporal dynamics, known as 'expanding models'. This leads to a logic that is known to be decidable but whose axiomatisation has long remained open. We propose an extension of iLTL with the co-implication connective of Hilbert–Brouwer logic and call it 'bi-intuitionistic linear temporal logic' (biLTL). We establish that this extension is still decidable for the class of expanding models. We moreover give a sound and complete Hilbert-style calculus for it, the first for any logic extending iLTL. As a corollary, the topological semantics for intuitionistic propositional logic cannot be extended to a topological semantics for Hilbert-Brouwer logic, which thus establishes co-implication as a distinctive feature of the Kripke semantics for bi-intuitionistic logic.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Dynamic Tangled Derivative Logic of Metric Spaces

  • David Fernández-Duque
  • Yoàv Montacute

Dynamical systems are abstract models of interaction between space and time. They are often used in fields such as physics and engineering to understand complex processes, but due to their general nature, they have found applications for studying computational processes, interaction in multi-agent systems, machine learning algorithms and other computer science related phenomena. In the vast majority of applications, a dynamical system consists of the action of a continuous `transition function' on a metric space. In this work, we consider decidable formal systems for reasoning about such structures. Spatial logics can be traced back to the 1940's, but our work follows a more dynamic turn that these logics have taken due to two recent developments: the study of the topological mu-calculus, and the the integration of linear temporal logic with logics based on the Cantor derivative. In this paper, we combine dynamic topological logics based on the Cantor derivative and the `next point in time' operators with an expressively complete fixed point operator to produce a combination of the topological mu-calculus with linear temporal logic. We show that the resulting logics are decidable and have a natural axiomatisation. Moreover, we prove that these logics are complete for interpretations on the Cantor space, the rational numbers, and subspaces thereof.

PDF Details DOI

KR Conference 2023 Conference Paper

A Family of Decidable Bi-intuitionistic Modal Logics

  • David Fernández-Duque
  • Brett McLean
  • Lukas Zenger

We investigate intuitionistic logics extended both with the co-implication connective of Hilbert-Brouwer logic and with diamond and box modalities. We use a Kripke semantics based on frames with two 'forth' confluence conditions on the modal relation with respect to the intuitionistic relation. We give sound and strongly complete axiomatisations for entailment on this class of frames, and give similar axiomatisations for the subclasses of frames satisfying any combination of reflexivity, transitivity, and seriality. We then prove that all of these logics are decidable, by proving that they have the finite frame property.

PDF Details DOI

JELIA Conference 2023 Conference Paper

The Universal Tangle for Spatial Reasoning

  • David Fernández-Duque
  • Konstantinos Papafilippou

Abstract The topological \(\mu \) -calculus has gathered attention in recent years as a powerful framework for representation of spatial knowledge. In particular, spatial relations can be represented over finite structures in the guise of weakly transitive ( wK4 ) frames. In this paper we show that the topological \(\mu \) -calculus is equivalent to a simple fragment based on a variant of the ‘tangle’ operator. Similar results were proven for transitive frames by Dawar and Otto, using modal characterisation theorems for the corresponding classes of frames. However, since these theorems are not available in our setting, which has the upshot of providing a more explicit translation and upper bounds on formula size.

Details

AAAI Conference 2023 Conference Paper

Untangled: A Complete Dynamic Topological Logic

  • David Fernández-Duque
  • Yoàv Montacute

Dynamical systems are general models of change or movement over time with a broad area of applicability to many branches of science, including computer science and AI. Dynamic topological logic (DTL) is a formal framework for symbolic reasoning about dynamical systems. DTL can express various liveness and reachability conditions on such systems, but has the drawback that the only known axiomatisation requires an extended language. In this paper, we consider dynamic topological logic restricted to the class of scattered spaces. Scattered spaces appear in the context of computational logic as they provide semantics for provability and enjoy definable fixed points. We exhibit the first sound and complete dynamic topological logic in the original language of DTL. In particular, we show that the version of DTL based on the class of scattered spaces is finitely axiomatisable, and that the natural axiomatisation is sound and complete.

PDF Details DOI

KR Conference 2022 Conference Paper

A Gödel Calculus for Linear Temporal Logic

  • Juan Pablo Aguilera
  • Martín Diéguez
  • David Fernández-Duque
  • Brett McLean

We consider GTL, a variant of linear temporal logic based on Gödel-Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be PSPACE-complete. In this paper we provide a deductive calculus for GTL, and show this calculus to be sound and complete for the above-mentioned semantics.

PDF Details DOI

I&C Journal 2022 Journal Article

Deducibility and independence in Beklemishev's autonomous provability calculus

  • David Fernández-Duque
  • Eduardo Hermo-Reyes

Beklemishev introduced an ordinal notation system for the Feferman-Schütte ordinal Γ 0 based on the autonomous expansion of provability algebras. In this paper we present the logic BC (for Bracket Calculus). The language of BC extends said ordinal notation system to a strictly positive modal language. Thus, unlike other provability logics, BC is based on a self-contained signature that gives rise to an ordinal notation system instead of modalities indexed by some ordinal given a priori. The presented logic is proven to be equivalent to RC Γ 0, that is, to the strictly positive fragment of GLP Γ 0. We then define a combinatorial statement based on BC and show it to be independent of the theory ATR 0 of Arithmetical Transfinite Recursion, a theory of second order arithmetic far more powerful than Peano Arithmetic.

Details DOI

CSL Conference 2022 Conference Paper

Dynamic Cantor Derivative Logic

  • David Fernández-Duque
  • Yoàv Montacute

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.

Details

KR Conference 2022 Conference Paper

The Topology of Surprise

  • Alexandru Baltag
  • Nick Bezhanishvili
  • David Fernández-Duque

In this paper we present a topological epistemic logic, with modalities for knowledge (modeled as the universal modality), knowability (represented by the topological interior operator), and unknowability of the actual world. The last notion has a non-self-referential reading (modeled by Cantor derivative: the set of limit points of a given set) and a self-referential one (modeled by Cantor's perfect core of a given set: its largest subset without isolated points). We completely axiomatize this logic, showing that it is decidable and PSPACE-complete, and we apply it to the analysis of a famous epistemic puzzle: the Surprise Exam Paradox.

PDF Details DOI

FLAP Journal 2021 Journal Article

Bisimulations for Intuitionistic Temporal Logics.

  • Philippe Balbiani
  • Joseph Boudou
  • Martín Diéguez
  • David Fernández-Duque

We introduce bisimulations for the logic ITLe with ◯ (‘next’), U (‘until’) and R (‘release’), an intuitionistic temporal logic based on structures (W, ≼, S), where ≼ is used to interpret intuitionistic implication and S is a ≼-monotone function used to interpret the temporal modalities. Our main results are that ◇ (‘eventually’), which is definable in terms of U, cannot be defined in terms of ◯ and ◻, and similarly that ◻ (‘henceforth’), definable in terms of R, cannot be defined in terms of ◯ and U, even over the smaller class of here-and-there models.

Details

I&C Journal 2021 Journal Article

To drive or not to drive: A logical and computational analysis of European transport regulations

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

This paper analyses a selection of articles from European transport regulations that contain algorithmic information, but may be problematic to implement. We focus on issues regarding the interpretation of tachograph data and requirements on weekly rest periods. We first show that the interpretation of data prescribed by these regulations is highly sensitive to minor variations in input, such that near-identical driving patterns may be regarded both as lawful and as unlawful. We then show that the content of the regulation may be represented in monadic second order logic, but argue that a more computationally tame fragment would be preferable for applications. As a case study we consider its representation in linear temporal logic, but show that a representation of the legislation requires formulas of unfeasible complexity, if at all possible.

Details DOI

JELIA Conference 2019 Conference Paper

Axiomatic Systems and Topological Semantics for Intuitionistic Temporal Logic

  • Joseph Boudou
  • Martín Diéguez
  • David Fernández-Duque
  • Fabián Romero

Abstract The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible to extend functional languages with new features via type theory, while from its semantical perspective several logics for reasoning about dynamical systems and several semantics for logic programming have their roots in this framework. In this paper we propose four axiomatic systems for intuitionistic linear temporal logic and show that each of these systems is sound for a class of structures based either on Kripke frames or on dynamic topological systems. Our topological semantics features a new interpretation for the ‘henceforth’ modality that is a natural intuitionistic variant of the classical one. Using the soundness results, we show that the four logics obtained from the axiomatic systems are distinct.

Details

IJCAI Conference 2019 Conference Paper

Stratified Evidence Logics

  • Philippe Balbiani
  • David Fernández-Duque
  • Andreas Herzig
  • Emiliano Lorini

Evidence logics model agents' belief revision process as they incorporate and aggregate information obtained from multiple sources. This information is captured using neighbourhood structures, where individual neighbourhoods represent pieces of evidence. In this paper we propose an extended framework which allows one to explicitly quantify either the number of evidence sets, or effort, needed to justify a given proposition, provide a complete deductive calculus and a proof of decidability, and show how existing frameworks can be embedded into ours.

PDF Details

TIME Conference 2019 Conference Paper

The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

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

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.

Details

FLAP Journal 2018 Journal Article

Succinctness in Subsystems of the Spatial μ-Calculus.

  • David Fernández-Duque
  • Petar Iliev

In this paper we systematically explore questions of succinctness in modal logics employed in spatial reasoning. We show that the closure operator, despite being less expressive, is exponentially more succinct than the limit-point operator, and that the µ-calculus is exponentially more succinct than the equallyexpressive tangled limit operator. These results hold for any class of spaces containing at least one crowded metric space or containing all spaces based on ordinals below ω ω, with the usual limit operator. We also show that these results continue to hold even if we enrich the less succinct language with the universal modality.

PDF Details

CSL Conference 2017 Conference Paper

A Decidable Intuitionistic Temporal Logic

  • Joseph Boudou
  • Martín Diéguez
  • David Fernández-Duque

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.

Details

AAMAS Conference 2016 Conference Paper

A Logical Theory of Belief Dynamics for Resource-Bounded Agents

  • Philippe Balbiani
  • David Fernández-Duque
  • Emiliano Lorini

The paper presents a new logic for reasoning about the formation of beliefs through perception or through inference in non-omniscient resource-bounded agents. The logic distinguishes the concept of explicit belief from the concept of background knowledge. This distinction is reflected in its formal semantics and axiomatics: (i) we use a non- standard semantics putting together a neighbourhood semantics for explicit beliefs and relational semantics for background knowledge, and (ii) we have specific axioms in the logic highlighting the relationship between the two concepts. Mental operations of perceptive type and inferential type, having effects on epistemic states of agents, are primitives in the object language of the logic. At the semantic level, they are modelled as special kinds of model-update operations, in the style of dynamic epistemic logic (DEL). Results about axiomatization, decidability and complexity for the logic are given in the paper.

PDF

TCS Journal 2013 Journal Article

A colouring protocol for the generalized Russian cards problem

  • Andrés Cordón-Franco
  • Hans van Ditmarsch
  • David Fernández-Duque
  • Fernando Soler-Toscano

In the generalized Russian cards problem, Alice, Bob and Cath draw a, b and c cards, respectively, from a deck of size a + b + c. Alice and Bob must then communicate their entire hand to each other, without Cath learning the owner of a single card she does not hold. Unlike many traditional problems in cryptography, however, they are not allowed to encode or hide the messages they exchange from Cath. The problem is then to find methods through which they can achieve this. We propose a general four-step solution based on finite vector spaces, and call it the “colouring protocol”, as it involves colourings of lines. Our main results show that the colouring protocol may be used to solve the generalized Russian cards problem in cases where a is a power of a prime, c = O ( a 2 ) and b = O ( c 2 ). This improves substantially on the set of parameters for which solutions are known to exist; in particular, it had not been shown previously that the problem could be solved in cases where the eavesdropper has more cards than one of the communicating players.

Details DOI
v2026.09.13