The topic of fuzzy and relation-changing structures has been progressively explored through the authors' previous work. This paper continues to expand the range of application for these models by introducing Labeled Fuzzy Reactive Graphs. This structure admits labels in regular edges, in order to permit to describe the action of different agents. For such structures, the operations of union, intersection and threshold are presented. Subsequently, this structure is applied to model a cancer treatment protocol and it is shown how the relation-changing properties of this structure can be used to better describe the dynamics of the modeled protocol.

Abstract In this article we define a logical system called Hybrid Partial Type Theory ( $\mathcal {HPTT}$ ). The system is obtained by combining William Farmer’s partial type theory with a strong form of hybrid logic. William Farmer’s system is a version of Church’s theory of types which allows terms to be non-denoting; hybrid logic is a version of modal logic in which it is possible to name worlds and evaluate expressions with respect to particular worlds. We motivate this combination of ideas in the introduction, and devote the rest of the article to defining, axiomatising, and proving a completeness result for $\mathcal {HPTT}$ .

Switch graphs are graph-like structures characterized by embedding higher-level edges (edges that link to other edges) to describe reactive phenomena. When an edge of such structure is traversed, the accessibility relation of this graph can be changed by adding/removing edges. Relation-changing models have been used to represent phenomena in diverse fields (from Biology to Computer Science) and some modal languages were introduced recently. In this paper we introduce four-valued local information in switch graphs, and propose a paraconsistent logic to study these systems.

This special issue contains extended versions of selected papers presented at the 3rd International Workshop on Dynamic Logic: New Trends and Applications (DaLí 2020). The workshop took place on 9–10 October 2020 online due to the COVID-19 pandemic. The organization of the workshop was based at the Institute of Computer Science of the Czech Academy of Sciences in Prague, Czech Republic. The submissions to DaLí 2020 and to the special issue span across various areas including dynamic logic and dynamic algebra, dynamic logic and public announcement logic and epistemic and modal logic in general. We hope the reader will enjoy the special issue, and we offer a small appetizer in the form of an outline of its contents. In their paper The Expressivity of Quantified Group Announcements, Natasha Alechina, Hans van Ditmarsch, Tim French and Rustam Galimullin examine the expressivity of group announcement logic (GAL) and coalition announcement logic (CAL), involving the closely related logic of arbitrary public announcements (APAL). These logics are important tools for reasoning about whether groups and coalitions of agents can achieve their epistemic goals through truthful public communication. They also explore how memory impacts the dynamics between groups and coalitions.

When visiting a hospital and seeking for answers for their symptoms, many people face contradictory diagnoses given by different physicians. This may happen either because they exhibit symptoms that are common to several diseases or because the symptoms are themselves misleading. In some cases, complementary methods of diagnostic are needed for further discussion. However, sometimes, not even those are the solution for an infallible diagnosis. By resorting to multimodal hybrid logic in a setting where inconsistencies are allowed, we introduce an informal example about the path of a patient in a hospital, where we keep information about his symptoms and diagnoses until being discharged. Our goal is the establishment of a measure of inconsistency, so that one can get a sense on the quality of the treatment given to the patient. By gathering a sufficient amount of information about patients in a hospital, those measures could be of help in determining the efficiency of the hospital. This is a critical issue, as it is well-known that early diagnoses are superbly desirable and can be life-changing.

As in standard knowledge bases, hybrid knowledge bases (i.e. sets of information specified by hybrid formulas) may contain inconsistencies arising from different sources, namely from the many mechanisms used to collect relevant information. Being a fact, rather than a queer anomaly, inconsistency also needs to be addressed in the context of hybrid logic applications. This article introduces a paraconsistent version of hybrid logic which is able to accommodate inconsistencies at local points without implying global failure. A main feature of the resulting logic, crucial to our approach, is the fact that every hybrid formula has an equivalent formula in negation normal form. The article also provides a measure to quantify the inconsistency of a hybrid knowledge base, useful as a possible basis for comparing knowledge bases. Finally, the concepts of extrinsic and intrinsic inconsistency of a theory are discussed.

Abstract Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy–Milner like theorem is proved for hybridised logics.

In this paper we focus in health care knowledge, specified by hybrid formulas, representing flows of medical assistance in the care delivery process in a hospital. As in standard knowledgebases inconsistencies may arise. In fact, Medical Informatics is one field where the ability to reason with inconsistent information is crucial. Patients can receive different, and moreover contradictory, diagnoses from different physicians, and the same can happen with medical treatments: they can exhibit contradictory symptoms. We introduce a paraconsistent version of multimodal hybrid logic to help with this medical issue, specially through the diagnosis.

Modern software systems usually deal with several sorts (types) of data elements simultaneously. Some of these sorts, like integers, booleans, strings, and so on, can be seen as having an immediate, direct nature and therefore are called visible, and they are contrasted with the others, like types\nof objects (in OOP sense), which are called hidden sorts. A language used to specify such software system has to be heterogeneous. In addition, to reason about such computations, we have to consider k-tuples of formulas (for\ninstance, pairs in equational reasoning). Consequently, a consequence relation used to specify and verify the properties of those systems must relate sorted sets of k-formulas with individual k-formulas. Logics usually employed in this process are called hidden k-logics and are very general in nature: they\ncomprise several classes of logical systems, including the 2-dimensional hidden and standard equational logics, and Boolean logic. In this paper we propose a generalization of the notion of deduction-detachment system for hidden k-logics. We introduce a syntactic notion of translation, which will be used to\ndefine an equivalence relation between hidden k-logics. We show that this notion of equivalence preserves some logical properties, namely the deduction-detachment theorem and the Craig interpolation property. We also show that if a specifiable hidden k-logic admits the deduction-detachment theorem then it admits a presentation whose only inference rules are the generalized modus\nponens rules with respect to the deduction-detachment system.

This paper extends the authors' previous work on a formal approach to the specification of reconfigurable systems, introduced in [7], in which configurations are taken as local states in a suitable transition structure. The novelty is the explicit consideration that not only the realisation of a service may change from a configuration to another, but also the set of services provided and even their functionality, may themselves vary. In other words, interfaces may evolve, as well.

In this article we present methods of transition from one perspective on logic to others, and apply this in particular to obtain a coalgebraic presentation of logic. The central ingredient in this process is to view consequence relations as morphisms in a category.

Traditional notions of refinement of algebraic specifications, based on signature morphisms, are often too rigid to capture a number of relevant transformations in the context of software design, reuse and adaptation. This paper proposes an alternative notion of specification refinement, building on recent work on logic interpretation. The concept is discussed, its theory partially developed, its use illustrated through a number of examples.

Throughout this paper we consider data structures as sorted algebras endowed with a designated subset of their visible part, which represents the set of truth values. The originality of our approach is the application of the standard abstract algebraic logic theory of deductive systems to the hidden heterogeneous case. We generalize the well-known equivalence relation between finite automata, which relies on the Nerode equivalence relation between states, to k-data structures. This is obtained via the Leibniz congruence, which can be viewed as a generalization of the Nerode equi-valence in automata theory.

Object-oriented (OO) programming techniques can be applied to equational specification logics by distinguishing visible data from hidden data (that is, by distinguishing the output of methods from the objects to which the methods apply), and then focusing on the behavioural equivalence of hidden data in the sense introduced by H. Reichel in 1984. Equational specification logics structured in this way are called hidden equational logics, HELs. The central problem is how to extend the specification of a given HEL to a specification of behavioural equivalence in a computationally effective way. S. Buss and G. Roşu showed in 2000 that this is not possible in general, but much work has been done on the partial specification of behavioural equivalence for a wide class of HELs. The OO connection suggests the use of coalgebraic methods, and J. Goguen and his collaborators have developed coinductive processes that depend on an appropriate choice of a cobasis, which is a special set of contexts that generates a subset of the behavioural equivalence relation. In this paper the theoretical aspects of coinduction are investigated, specifically its role as a supplement to standard equational logic for determining behavioural equivalence. Various forms of coinduction are explored. A simple characterisation is given of those HELs that are behaviourally specifiable. Those sets of conditional equations that constitute a complete, finite cobasis for a HEL are characterised in terms of the HEL's specification. Behavioural equivalence, in the form of logical equivalence, is also an important concept for single-sorted logics, for example, sentential logics such as the classical propositional logic. The paper is an application of the methods developed through the extensive work that has been done in this area on HELs, and to a broader class of logics that encompasses both sentential logics and HELs.