-
Complexity of the Model Checking problem for inquisitive propositional and modal logic
Authors:
Gianluca Grilletti,
Ivano Ciardelli
Abstract:
The aim of this paper is to study the complexity of the model checking problem MC for inquisitive propositional logic InqB and for inquisitive modal logic InqM, that is, the problem of deciding whether a given finite structure for the logic satisfies a given formula. In recent years, this problem has been thoroughly investigated for several variations of dependence and teams logics, systems closel…
▽ More
The aim of this paper is to study the complexity of the model checking problem MC for inquisitive propositional logic InqB and for inquisitive modal logic InqM, that is, the problem of deciding whether a given finite structure for the logic satisfies a given formula. In recent years, this problem has been thoroughly investigated for several variations of dependence and teams logics, systems closely related to inquisitive logic. Building upon some ideas presented by Yang, we prove that the model checking problems for InqB and InqM are both AP-complete.
△ Less
Submitted 28 March, 2024; v1 submitted 21 March, 2024;
originally announced March 2024.
-
Esakia Duals of Regular Heyting Algebras
Authors:
Gianluca Grilletti,
Davide Emilio Quadrellaro
Abstract:
We investigate in this article regular Heyting algebras by means of Esakia duality. In particular, we give a characterisation of Esakia spaces dual to regular Heyting algebras and we show that there are continuum-many varieties of Heyting algebras generated by regular Heyting algebras. We also study several logical applications of these classes of objects and we use them to provide novel topologic…
▽ More
We investigate in this article regular Heyting algebras by means of Esakia duality. In particular, we give a characterisation of Esakia spaces dual to regular Heyting algebras and we show that there are continuum-many varieties of Heyting algebras generated by regular Heyting algebras. We also study several logical applications of these classes of objects and we use them to provide novel topological completeness theorems for inquisitive logic, $\mathtt{DNA}$-logics and dependence logic.
△ Less
Submitted 25 August, 2023; v1 submitted 20 March, 2023;
originally announced March 2023.
-
Geometric Model Checking of Continuous Space
Authors:
Nick Bezhanishvili,
Vincenzo Ciancia,
David Gabelaia,
Gianluca Grilletti,
Diego Latella,
Mieke Massink
Abstract:
Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of…
▽ More
Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.
△ Less
Submitted 21 November, 2022; v1 submitted 13 May, 2021;
originally announced May 2021.
-
Lattices of Intermediate Theories via Ruitenburg's Theorem
Authors:
Gianluca Grilletti,
Davide Emilio Quadrellaro
Abstract:
For every univariate formula $χ$ we introduce a lattices of intermediate theories: the lattice of $χ$-logics. The key idea to define chi-logics is to interpret atomic propositions as fixpoints of the formula $χ^2$, which can be characterised syntactically using Ruitenburg's theorem. We develop an algebraic duality between the lattice of $χ$-logics and a special class of varieties of Heyting algebr…
▽ More
For every univariate formula $χ$ we introduce a lattices of intermediate theories: the lattice of $χ$-logics. The key idea to define chi-logics is to interpret atomic propositions as fixpoints of the formula $χ^2$, which can be characterised syntactically using Ruitenburg's theorem. We develop an algebraic duality between the lattice of $χ$-logics and a special class of varieties of Heyting algebras. This approach allows us to build five distinct lattices corresponding to the possible fixpoints of univariate formulas|among which the lattice of negative variants of intermediate logics. We describe these lattices in more detail.
△ Less
Submitted 2 April, 2020;
originally announced April 2020.
-
A logic for temporal conditionals and a solution to the Sea Battle Puzzle
Authors:
Fengkui Ju,
Gianluca Grilletti,
Valentin Goranko
Abstract:
Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle's famous "Sea Battle Tomorrow" puzzle leads to a fatalistic conclusion: whether there will be a sea battle tomorrow or not, but that is necessarily the case now. We propose a branchin…
▽ More
Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle's famous "Sea Battle Tomorrow" puzzle leads to a fatalistic conclusion: whether there will be a sea battle tomorrow or not, but that is necessarily the case now. We propose a branching-time logic LTC to formalise reasoning about temporal conditionals and provide that logic with adequate formal semantics. The logic LTC extends the Nexttime fragment of CTL*, with operators for model updates, restricting the domain to only future moments where antecedent is still possible to satisfy. We provide formal semantics for these operators that implements the restrictor interpretation of antecedents of temporalized conditionals, by suitably restricting the domain of discourse. As a motivating example, we demonstrate that a naturally formalised in our logic version of the `Sea Battle' argument renders it unsound, thereby providing a solution to the problem with fatalist conclusion that it entails, because its underlying reasoning per cases argument no longer applies when these cases are treated not as material implications but as temporal conditionals. On the technical side, we analyze the semantics of LTC and provide a series of reductions of LTC-formulae, first recursively eliminating the dynamic update operators and then the path quantifiers in such formulae. Using these reductions we obtain a sound and complete axiomatization for LTC, and reduce its decision problem to that of the modal logic KD.
△ Less
Submitted 26 May, 2024; v1 submitted 8 November, 2017;
originally announced November 2017.
