-
Sequent Calculi for Data-Aware Modal Logics
Authors:
Carlos Areces,
Valentin Cassano,
Danae Dutto,
Raul Fervari
Abstract:
This document serves as a companion to the paper of the same title, wherein we introduce a Gentzen-style sequent calculus for HXPathD. It provides full technical details and proofs from the main paper. As such, it is intended as a reference for readers seeking a deeper understanding of the formal results, including soundness, completeness, invertibility, and cut elimination for the calculus.
This document serves as a companion to the paper of the same title, wherein we introduce a Gentzen-style sequent calculus for HXPathD. It provides full technical details and proofs from the main paper. As such, it is intended as a reference for readers seeking a deeper understanding of the formal results, including soundness, completeness, invertibility, and cut elimination for the calculus.
△ Less
Submitted 22 May, 2025;
originally announced May 2025.
-
Deontic Action Logics: A Modular Algebraic Perspective
Authors:
Carlos Areces,
Valentin Cassano,
Pablo Castro,
Raul Fervari
Abstract:
In a seminal work, K. Segerberg introduced a deontic logic called DAL to investigate normative reasoning over actions. DAL marked the beginning of a new area of research in Deontic Logic by shifting the focus from deontic operators on propositions to deontic operators on actions. In this work, we revisit DAL and provide a complete algebraization for it. In our algebraization we introduce deontic a…
▽ More
In a seminal work, K. Segerberg introduced a deontic logic called DAL to investigate normative reasoning over actions. DAL marked the beginning of a new area of research in Deontic Logic by shifting the focus from deontic operators on propositions to deontic operators on actions. In this work, we revisit DAL and provide a complete algebraization for it. In our algebraization we introduce deontic action algebras -- algebraic structures consisting of a Boolean algebra for interpreting actions, a Boolean algebra for interpreting formulas, and two mappings from one Boolean algebra to the other interpreting the deontic concepts of permission and prohibition. We elaborate on how the framework underpinning deontic action algebras enables the derivation of different deontic action logics by removing or imposing additional conditions over either of the Boolean algebras. We leverage this flexibility to demonstrate how we can capture in this framework several logics in the DAL family. Furthermore, we introduce four variations of DAL by: (a) enriching the algebra of formulas with propositions on states, (b) adopting a Heyting algebra for state propositions, (c) adopting a Heyting algebra for actions, and (d) adopting Heyting algebras for both. We illustrate these new deontic action logics with examples and establish their algebraic completeness.
△ Less
Submitted 19 February, 2025;
originally announced February 2025.
-
Data-Aware Hybrid Tableaux
Authors:
Carlos Areces,
Valentin Cassano,
Raul Fervari
Abstract:
Labelled tableaux have been a traditional approach to define satisfiability checking procedures for Modal Logics. In many cases, they can also be used to obtain tight complexity bounds and lead to efficient implementations of reasoning tools. More recently, it has been shown that the expressive power provided by the operators characterizing Hybrid Logics (nominals and satisfiability modalities) ca…
▽ More
Labelled tableaux have been a traditional approach to define satisfiability checking procedures for Modal Logics. In many cases, they can also be used to obtain tight complexity bounds and lead to efficient implementations of reasoning tools. More recently, it has been shown that the expressive power provided by the operators characterizing Hybrid Logics (nominals and satisfiability modalities) can be used to \emph{internalize} labels, leading to well-behaved inference procedures for fairly expressive logics. The resulting procedures are attractive because they do not use external mechanisms outside the language of the logic at hand, and have good logical and computational properties.
Many tableau systems based on Hybrid Logic have been investigated, with more recent efforts concentrating on Modal Logics that support data comparison operators. Here, we introduce an internalized tableau calculus for XPath, arguably one of the most prominent approaches for querying semistructured data. More precisely, we define data-aware tableaux for XPath featuring data comparison operators and enriched with nominals and the satisfiability modalities from Hybrid Logic. We prove that the calculus is sound, complete and terminating. Moreover, we show that tableaux can be explored in polynomial space, therefore establishing that the satisfiability problem for the logic is PSPACE-complete. Finally, we explore different extensions of the calculus, in particular how to handle data trees and other frame classes.
△ Less
Submitted 26 June, 2025; v1 submitted 17 June, 2024;
originally announced June 2024.
-
Beyond the Spell: A Dynamic Logic Analysis of Misdirection
Authors:
Benjamin Icard,
Raul Fervari
Abstract:
Misdirection can be defined as the intentional action of causing some misrepresentation in an agent, or in a group of agents. Such misrepresentations may result from verbal actions, as in linguistic deception, or from visual actions, as in visual misdirection. Examples of visual misdirection abound (e.g. in nature, in the military), with magic tricks providing a vivid illustration. So far, various…
▽ More
Misdirection can be defined as the intentional action of causing some misrepresentation in an agent, or in a group of agents. Such misrepresentations may result from verbal actions, as in linguistic deception, or from visual actions, as in visual misdirection. Examples of visual misdirection abound (e.g. in nature, in the military), with magic tricks providing a vivid illustration. So far, various types of verbal misdirection have been investigated from a formal perspective (e.g. lying, bluffing) but little attention has been paid to the particular case of visual misdirection. In this paper, we introduce a dynamic epistemic logic to represent not only verbal misdirection on agents' beliefs but also visual misdirection on agents' observations. We illustrate the dynamics of the logic by modelling a classic magic trick known as the French Drop. We also provide a sound and complete axiom system for the logic, and discuss the expressivity and scope of the setting.
△ Less
Submitted 3 April, 2025; v1 submitted 25 January, 2024;
originally announced January 2024.
-
How Easy it is to Know How: An Upper Bound for the Satisfiability Problem
Authors:
Carlos Areces,
Valentin Cassano,
Raul Fervari,
Pablo Castro,
Andres Saravia
Abstract:
We investigate the complexity of the satisfiability problem for a modal logic expressing `knowing how' assertions, related to an agent's abilities to achieve a certain goal. We take one of the most standard semantics for this kind of logics based on linear plans. Our main result is a proof that checking satisfiability of a `knowing how' formula can be done in $Σ_2^P$. The algorithm we present reli…
▽ More
We investigate the complexity of the satisfiability problem for a modal logic expressing `knowing how' assertions, related to an agent's abilities to achieve a certain goal. We take one of the most standard semantics for this kind of logics based on linear plans. Our main result is a proof that checking satisfiability of a `knowing how' formula can be done in $Σ_2^P$. The algorithm we present relies on eliminating nested modalities in a formula, and then performing multiple calls to a satisfiability checking oracle for propositional logic.
△ Less
Submitted 29 September, 2023;
originally announced September 2023.
-
Uncertainty-Based Knowing How Logic
Authors:
Carlos Areces,
Raul Fervari,
Andrés R. Saravia,
Fernando R. Velázquez-Quesada
Abstract:
We introduce a novel semantics for a multi-agent epistemic operator of knowing how, based on an indistinguishability relation between plans. Our proposal is, arguably, closer to the standard presentation of knowing that modalities in classical epistemic logic. We study the relationship between this new semantics and previous approaches, showing that our setting is general enough to capture them. W…
▽ More
We introduce a novel semantics for a multi-agent epistemic operator of knowing how, based on an indistinguishability relation between plans. Our proposal is, arguably, closer to the standard presentation of knowing that modalities in classical epistemic logic. We study the relationship between this new semantics and previous approaches, showing that our setting is general enough to capture them. We also study the logical properties of the new semantics. First, we define a sound and complete axiomatization. Second, we define a suitable notion of bisimulation and prove correspondence theorems. Finally, we investigate the computational complexity of the model checking and satisfiability problems for the new logic.
△ Less
Submitted 3 April, 2023;
originally announced April 2023.
-
Uncertainty-Based Semantics for Multi-Agent Knowing How Logics
Authors:
Carlos Areces,
Raul Fervari,
Andrés R. Saravia,
Fernando R. Velázquez-Quesada
Abstract:
We introduce a new semantics for a multi-agent epistemic operator of knowing how, based on an indistinguishability relation between plans. Our proposal is, arguably, closer to the standard presentation of knowing that modalities in classical epistemic logic. We study the relationship between this semantics and previous approaches, showing that our setting is general enough to capture them. We als…
▽ More
We introduce a new semantics for a multi-agent epistemic operator of knowing how, based on an indistinguishability relation between plans. Our proposal is, arguably, closer to the standard presentation of knowing that modalities in classical epistemic logic. We study the relationship between this semantics and previous approaches, showing that our setting is general enough to capture them. We also define a sound and complete axiomatization, and investigate the computational complexity of its model checking and satisfiability problems.
△ Less
Submitted 21 June, 2021;
originally announced June 2021.
-
Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
Authors:
Bartosz Bednarczyk,
Stéphane Demri,
Raul Fervari,
Alessio Mansutti
Abstract:
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) i…
▽ More
We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(*) contains the separating conjunction * from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(*) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(*) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete. As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.
△ Less
Submitted 16 July, 2020;
originally announced July 2020.
-
Axiomatizing Hybrid XPath with Data
Authors:
Carlos Areces,
Raul Fervari
Abstract:
In this paper we introduce sound and strongly complete axiomatizations for XPath with data constraints extended with hybrid operators. First, we present HXPath=, a multi-modal version of XPath with data, extended with nominals and the hybrid operator @. Then, we introduce an axiomatic system for HXPath=, and we prove it is strongly complete with respect to the class of abstract data models, i.e.,…
▽ More
In this paper we introduce sound and strongly complete axiomatizations for XPath with data constraints extended with hybrid operators. First, we present HXPath=, a multi-modal version of XPath with data, extended with nominals and the hybrid operator @. Then, we introduce an axiomatic system for HXPath=, and we prove it is strongly complete with respect to the class of abstract data models, i.e., data models in which data values are abstracted as equivalence relations. We prove a general completeness result similar to the one presented in, e.g., [BtC06], that ensures that certain extensions of the axiomatic system we introduce are also complete. The axiomatic systems that can be obtained in this way cover a large family of hybrid XPath languages over different classes of frames, for which we present concrete examples. In addition, we investigate axiomatizations over the class of tree models, structures widely used in practice. We show that a strongly complete, finitary, first-order axiomatization of hybrid XPath over trees does not exist, and we propose two alternatives to deal with this issue. We finally introduce filtrations to investigate the status of decidability of the satisfiability problem for these languages.
△ Less
Submitted 19 July, 2021; v1 submitted 31 March, 2020;
originally announced April 2020.
-
An Algebraic Approach for Action Based Default Reasoning
Authors:
Pablo F. Castro,
Valentin Cassano,
Raul Fervari,
Carlos Areces
Abstract:
Often, we assume that an action is permitted simply because it is not explicitly forbidden; or, similarly, that an action is forbidden simply because it is not explicitly permitted. This kind of assumptions appear, e.g., in autonomous computing systems where decisions must be taken in the presence of an incomplete set of norms regulating a particular scenario. Combining default and deontic reasoni…
▽ More
Often, we assume that an action is permitted simply because it is not explicitly forbidden; or, similarly, that an action is forbidden simply because it is not explicitly permitted. This kind of assumptions appear, e.g., in autonomous computing systems where decisions must be taken in the presence of an incomplete set of norms regulating a particular scenario. Combining default and deontic reasoning over actions allows us to formally reason about such assumptions. With this in mind, we propose a logical formalism for default reasoning over a deontic action logic. The novelty of our approach is twofold. First, our formalism for default reasoning deals with actions and action operators, and it is based on the deontic action logic originally proposed by Segerberg. Second, inspired by Segerberg's approach, we use tools coming from the theory of Boolean Algebra. These tools allow us to extend Segerberg's algebraic completeness result to the setting of Default Logics.
△ Less
Submitted 21 July, 2019;
originally announced July 2019.
-
Strategically knowing how
Authors:
Raul Fervari,
Andreas Herzig,
Yanjun Li,
Yanjing Wang
Abstract:
In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve $φ$ means that there exists a (uniform) strategy such that the agent knows that it can make sure $φ$. We give an intuitive axiomatization of our logic an…
▽ More
In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve $φ$ means that there exists a (uniform) strategy such that the agent knows that it can make sure $φ$. We give an intuitive axiomatization of our logic and prove the soundness, completeness, and decidability of the logic. The crucial axioms relating knowing that and knowing how illustrate our understanding of knowing how in this setting. This logic can be used in representing both knowledge-that and knowledge-how.
△ Less
Submitted 15 May, 2017;
originally announced May 2017.
-
Relation-Changing Logics as Fragments of Hybrid Logics
Authors:
Carlos Areces,
Raul Fervari,
Guillaume Hoffmann,
Mauricio Martel
Abstract:
Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. I…
▽ More
Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. In general, these logics are undecidable, but we use our translations to identify decidable fragments. We also compare the expressive power of relation-changing modal logics with hybrid logics.
△ Less
Submitted 13 September, 2016;
originally announced September 2016.
-
Axiomatizations for downward XPath on Data Trees
Authors:
Sergio Abriola,
María Emilia Descotte,
Raul Fervari,
Santiago Figueira
Abstract:
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This data-aware logic predicts over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the d…
▽ More
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This data-aware logic predicts over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e. there is no comparison by constants). Our axioms are in the style of equational logic, extending the axiomatization of data-oblivious XPath, by B. ten Cate, T. Litak and M. Marx. We axiomatize the full logic with tests by "equality" and "inequality", and also a simpler fragment with "equality" tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests.
△ Less
Submitted 13 March, 2017; v1 submitted 13 May, 2016;
originally announced May 2016.
