We often have to draw conclusions about states of machines in computer science and about states of knowledge and belief in artificial intelligence based on partial information. Nerode suggested using constructive logic as the language to express such deductions and also suggested designing appropriate intuitionistic Kripke frames to express the partial information. Following this program, Nerode and Wijesekera developed syntax, semantics and completeness for a system of intuitionistic dynamic logic for proving properties of concurrent programs. Like all dynamics logics, this (...) was a logic of many modalities, each expressing a program, but in intuitionistic rather than in classical logic. In that logic, both box and diamond are needed, but these two are not intuitionistically interdefinable and, worse, diamond does not distribute over ‘or’, except for sequential programs. This also happens in other contemplated computer science and AI applications, and leads outside the class of constructive logics investigated in the literature. The present paper fills this gap. We provide intuitionistic logics with independent box and diamond without assuming distribution of diamond over ‘or’. The completeness theorem is based on intuitionistic Kripke frames , but equipped with an additional, quite separate accessibility relation between worlds. In the interpretation of Nerode and Wijesekera , worlds under the partial order represent states of partial knowledge, the accessibility represents change in state of partial knowledge resulting from executing a specific program. But there are many other computer science interpretations. This formalism covers all computer science applications of which we are aware. We also give a cut elimination theorem and algebraic and topological formulations, since these present some new difficulties. Finally, these results were obtained prior to those in Nerode and Wijesekera. (shrink)

Belief revision from the point of view of doxastic logic. Logic Journal of the IGPL, 3(4), 535–553. Segerberg, K. (1995). Conditional action. In G. Crocco, L. Fariñas, & A. Herzig (Eds.), Conditionals: From philosophy to computer science, Studies ...

A history of the logic of action is outlined, beginning with St Anselm. Five modern authors are discussed in some detail: von Wright, Fitch, Kanger, Chellas and Pratt.

The paper presents an infinite hierarchy of sound and complete axiomatic systems for Two-Dimensional Modal Tense Logic with Historical Necessity, Agents and Acts. A main novelty of these logics is their capacity to represent formally (i) basic action-sentences asserting that such and such an act is performed/omitted by an agent, as well as (ii) causative action-sentences asserting that by performing/omitting a certain act, an agent causes that such and such a state-of-affairs is realized (e.g. comes about/ceases/remains/remains absent). We illustrate how (...) the formal machinery of our systems can be used to reconstruct a number of interesting ideas in the Logic of Agency and Action that have been proposed by authors like von Wright, von Kutschera, Belnap and Segerberg. (shrink)

Reasoning about change is a central issue in research on human and robot planning. We study an approach to reasoning about action and change in a dynamic logic setting and provide a solution to problems which are related to the Frame problem. Unlike most work on the frame problem the logic described in this paper is monotonic. It (implicitly) allows for the occurrence of actions of multiple agents by introducing non-stationary notions of waiting and test. The need to state a (...) large number of frame axioms is alleviated by introducing a concept of chronological preservation to dynamic logic. As a side effect, this concept permits the encoding of temporal properties in a natural way. We compare the relative merits of our approach and non-monotonic approaches as regards different aspects of the frame problem. Technically, we show that the resulting extended systems of propositional dynamic logic preserve (weak) completeness, finite model property and decidability. (shrink)

This work is divided in two papers (Part I and Part II). In Part I, we study a class of polymodal logics (herein called the class of "Rare-logics") for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability are established by faithfully translating the (...) Rare-logics into more standard modal logics. The main idea of the translation consists in eliminating the Boolean terms by taking advantage of the components construction and in using various properties of the classes of semilattices involved in the semantics. The novelty of our approach allows us to prove new decidability results (presented in Part II), in particular for information logics derived from rough set theory and we open new perspectives to define proof systems for such logics (presented also in Part II). (shrink)

In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from (...) these classes have the finite model property with respect to the class of -formulae, i.e. each -formula has a -model iff it has a finite -model. Roughly speaking, a -formula is logically equivalent to a formula in negative normal form without occurrences of modal operators with necessity force. In the proof we introduce a substantial modification of Claudio Cerrato's filtration technique that has been originally designed for graded modal logics. The main core of the proof consists in building adequate restrictions of models while preserving the semantics of the operators used to build terms indexing the modal operators. (shrink)

Esta enciclopédia abrange, de uma forma introdutória mas desejavelmente rigorosa, uma diversidade de conceitos, temas, problemas, argumentos e teorias localizados numa área relativamente recente de estudos, os quais tem sido habitual qualificar como «estudos lógico-filosóficos». De uma forma apropriadamente genérica, e apesar de o território teórico abrangido ser extenso e de contornos por vezes difusos, podemos dizer que na área se investiga um conjunto de questões fundamentais acerca da natureza da linguagem, da mente, da cognição e do raciocínio humanos, bem (...) como questões acerca das conexões destes com a realidade não mental e extralinguística. A razão daquela qualificação é a seguinte: por um lado, a investigação em questão é qualificada como filosófica em virtude do elevado grau de generalidade e abstracção das questões examinadas (entre outras coisas); por outro, a investigação é qualificada como lógica em virtude de ser uma investigação logicamente disciplinada, no sentido de nela se fazer um uso intenso de conceitos, técnicas e métodos provenientes da disciplina de lógica. O agregado de tópicos que constitui a área de estudos lógico-filosóficos é já visível, pelo menos em parte, no Tractatus Logico-Philosophicus de Ludwig Wittgenstein, uma obra publicada em 1921. E uma boa maneira de ter uma ideia sinóptica do território disciplinar abrangido por esta enciclopédia, ou pelo menos de uma porção substancial dele, é extrair do Tractatus uma lista dos tópicos mais salientes aí discutidos; a lista incluirá certamente tópicos do seguinte género, muitos dos quais se podem encontrar ao longo desta enciclopédia: factos e estados de coisas; objectos; representação; crenças e estados mentais; pensamentos; a proposição; nomes próprios; valores de verdade e bivalência; quantificação; funções de verdade; verdade lógica; identidade; tautologia; o raciocínio matemático; a natureza da inferência; o cepticismo e o solipsismo; a indução; as constantes lógicas; a negação; a forma lógica; as leis da ciência; o número. (shrink)

Situational aspects of action are discussed. The presented approach emphasizes the role of situational contexts in which actions are performed. These contexts influence the course of an action; they are determined not only by the current state of the system but also shaped by other factors as time, the previously undertaken actions and their succession, the agents of actions and so on. The distinction between states and situations is explored from the perspective of action systems. The notion of a situational (...) action system is introduced and its theory is expounded. Numerous examples illustrate the reach of the theory. (shrink)

This essay contains material which will hopefully be of interest not only to philosophers, but also to those social scientists whose research concerns the analysis of communication, verbal or non-verbal. Although most of the topics taken up here are central to issues in the philosophy of language, they are, in my opinion, indistinguishable from topics in descriptive social psychology. The essay aims to provide a conceptual framework within which various key aspects of communication can be described, and it presents a (...) formal language, using techniques from modern modal logic, in which such descriptions can themselves be formulated. It is my hope that this framework, or parts of it, might also turn out to be of value in future empirical work. There are, therefore, essentially two sides to this essay: the development of a framework of concepts, and the construction of a formal language rich enough to express the elements of which that framework is composed. The first of these two takes its point of departure in the statement quoted from Lewis (1972) on the page preceding this introduction. The distinction drawn there by Lewis is accepted as a working hypothesis, and in one sense this essay may be seen as an attempt to explore some of the consequences of that hypothesis. (shrink)

This paper presents an abstract-algebraic formulation of action facilitating reasoning about two opposing agents. Two dual nondeterministic choice operators are formulated abstract-algebraically: angelic (or user) choice and demonic (or system) choice. Iteration operators are also defined. As an application, Hoare-style correctness rules are established by means of the algebra. A negation operator is also discussed.

We present a direct reduction of dynamic epistemic logic in the spirit of [4] to propositional dynamic logic (PDL) [17, 18] by program transformation. The program transformation approach associates with every update action a transformation on PDL programs. These transformations are then employed in reduction axioms for the update actions. It follows that the logic of public announcement, the logic of group announcements, the logic of secret message passing, and so on, can all be viewed as subsystems of PDL. Moreover, (...) the program transformation approach can be used to generate the appropriate reduction axioms for these logics. Our direct reduction of dynamic epistemic logic to PDL was inspired by the reduction of dynamic epistemic logic to automata PDL of [13]. Our approach shows how the detour through automata can be avoided. (shrink)

Dynamic algebras combine the classes of Boolean (B 0) and regular (R ; *) algebras into a single finitely axiomatized variety (B R ) resembling an R-module with scalar multiplication . The basic result is that * is reflexive transitive closure, contrary to the intuition that this concept should require quantifiers for its definition. Using this result we give several examples of dynamic algebras arising naturally in connection with additive functions, binary relations, state trajectories, languages, and flowcharts. The main result (...) is that free dynamic algebras are residually finite (i.e. factor as a subdirect product of finite dynamic algebras), important because finite separable dynamic algebras are isomorphic to Kripke structures. Applications include a new completeness proof for the Segerberg axiomatization of prepositional dynamic logic, and yet another notion of regular algebra. (shrink)

This article provides an overview of development of Kripke semantics for logics determined by information systems. The proposals are made to extend the standard Kripke structures to the structures based on information systems. The underlying logics are defined and problems of their axiomatization are discussed. Several open problems connected with the logics are formulated. Logical aspects of incompleteness of information provided by information systems are considered.

This is the first paper on constructive concurrent dynamic logic . For the first time, either for concurrent or sequential dynamic logic, we give a satisfactory treatment of what statements are forced to be true by partial information about the underlying computer. Dynamic logic was developed by Pratt [V. Pratt, Semantical considerations on Floyd–Hoare logic, in: 17th Annual IEEE Symp. on Found. Comp. Sci., New York, 1976, pp. 109–121, V. Pratt, Applications of modal logic to programming, Studia Logica 39 257–274] (...) for nondeterministic sequential programs, and by Peleg [D. Peleg, Concurrent dynamic logic, Journal of the Association for Computing Machinery 34 , D. Peleg, Communication in concurrent dynamic logic, Journal of Computer and System Sciences 35 ] for concurrent programs, for the purpose of proving properties of programs such as correctness. Here we define what it means for a dynamic logic formula to be forced to be true knowing only partial information about the results of assignments and tests. This informal CCDL semantics is formalized by intuitionistic Kripke frames modeling this partial information, and each such frame is interpreted as an idealized concurrent machine . In CCDL, proofs and deductions are ω-height, ω-branching, well-founded labeled subtrees of ωω. These are a generalization of the signed tableaux of Nerode [A. Nerode, Some lectures in modal logic, Technical Report, M.S.I. Cornell University, 1989, CIME Logic and Computer Science Montecatini Volume, Springer-Verlag Lecture Notes, 1990, A. Nerode, Some lectures in intuitionistic logic, Technical Report, M.S.I. Cornell University, 1988, Marktoberdorf Logic and Computation NATO Summer School Volume, NATO Science Series, 1990 ] stemming from the prefix tableaux of Fitting [M.C. Fitting, Proof Methods for Modal and Intuitionistic Logic, Reidel, 1983]. We demonstrate the correctness of our tableau proofs, define consistency properties, prove that consistency properties yield models, construct systematic tableaux, prove that systematic tableaux yield a consistency property, and conclude that CCDL is complete. This infinitary semantics and proof procedure will be the primary guide for defining, in a sequel, the correct finitary CCDL based on induction principles. FCCDL is suitable for implementation in constructive logic software systems such as Constable’s NUPRL or Huet-Coquand’s CONSTRUCTIONS. Our goal is to develop a constructive logic programming tool for specification and modular verification of programs in any imperative concurrent language, and for the extraction of concurrent programs from constructive proofs. Subsequent papers will introduce analogous logics for declarative and functional concurrent languages. (shrink)