We study notions of (virtual) group knowledge and group belief within multi-agent evidence models, obtained by extending the topological semantics of evidence-based belief and fallible knowledge from individuals to groups. We completely axiomatize and show the decidability of the logic of ("hard" and "soft") group evidence, and do the same for an especially interesting fragment of it: the logic of group knowledge and group belief. We also extend these languages with dynamic evidence-sharing operators, and completely axiomatize the corresponding logics, showing that they are co-expressive with their static bases.
Dynamic Quantum Logic (DQL) has been used as a logical framework for manually proving the correctness of quantum programs. This paper presents an automated approach to quantum program verification at the cost of simplifying DQL to Basic Dynamic Quantum Logic (BDQL). We first formalize quantum states, quantum gates, and projections in bra-ket notation and use a set of laws from quantum mechanics and matrix operations to reason on quantum computation. We then formalize the semantics of BQDL and specify the behavior and desired properties of quantum programs in the scope of BDQL. Formal verification of whether a quantum program satisfies desired properties is conducted automatically through an equational simplification process. We use Maude, a rewriting logic-based specification/programming language, to implement our approach. To demonstrate the effectiveness of our automated approach, we successfully verified the correctness of five quantum protocols: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, and Quantum Gate Teleportation, using our support tool.
The logic of the hide and seek game LHS was proposed to reason about search missions and interactions between agents in pursuit-evasion environments. As proved in literature, having an equality constant in the language of LHS drastically increases its computational complexity: the satisfiability problem for LHS with multiple relations is undecidable. In this work we improve the existing result by showing that LHS with a single relation is undecidable. With the existing findings, we provide a van Benthem style characterization theorem for the expressive power of the logic. Finally, by `splitting' the language of LHS-, a crucial fragment of LHS without the equality constant, into two `isolated parts', we provide a complete Hilbert style proof system for LHS- and prove that its satisfiability problem is decidable, whose proofs would indicate significant differences between the proposals of LHS- and of ordinary product logics. Although LHS and LHS- are frameworks for interactions of 2 agents, all results in the article can be easily transferred to their generalizations for settings with any n > 2 agents.
In this paper, we investigate local and global dynamic modal operators which have the ability to update the accessibility relation of a model. For the global operators, the logic of global link variations based on hybrid logic (@) is introduced, which involves global link cutting, adding and rotating simultaneously. A Hilbert-style calculus 𝖢_𝖦𝖫𝖵 is provided. By constructing families of canonical models inductively, we prove that the calculus 𝖢_𝖦𝖫𝖵 is sound and strongly complete with respect to . For the local operators, we extended the logic (@,↓ ) of link deletion introduced in [12] to , which is based on the hybrid logic (,↓ ) and involves local definable link cutting, adding and rotating. By defining local named dynamic operators and providing recursion axioms for them, we obtain a sound and strongly complete calculus 𝖢_𝖫𝖫𝖵 for . Moreover, we show that for an arbitrary set X of global and local dynamic operators, the calculus 𝖢_𝖦𝖫𝖵(X) and 𝖢_𝖫𝖫𝖵(X) are still sound and strongly complete w.r.t the logic (X) and (X) , respectively.
Belief revision and causality play an important role in many applications, typically, in the study of database update mechanisms and data dependence. New contributions on causal reasoning are continuously added to the pioneering works by Pearl, Halpern and others. Though there is a long tradition of modeling belief revision in philosophical logic, the entanglement between belief revision and causal reasoning has not yet been fully studied from a logical view. In this paper, we propose a new formal logic for doxastic causal reasoning. With examples, we illustrate that our framework explains the rational way of belief revision based on causal reasoning. We further study the general properties of the logic. A complete axiomatization, as well as a decidability result, will be given. In addition, we believe our work will shed light on understanding the relation between qualitative and quantitative approaches toward (causal) dependence in general.
