A Non-deterministic View on Non-classical Negations

We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ⁺, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is based on non-deterministic four-valued or three-valued structures, and prove soundness and completeness for all of them. We show that the role of each rule is to reduce the degree of non-determinism in the corresponding systems. We also show that all the systems considered are decidable, and our semantics can be used for the corresponding decision procedures. Most of the extensions of LJ⁺ (with or without ff) are shown to be conservative over the underlying logic, and it is determined which of them are not.     

Algebraization, Parametrized Local Deduction Theorem and Interpolation for Substructural Logics over FL

Substructural logics have received a lot of attention in recent years from the communities of both logic and algebra. We discuss the algebraization of substructural logics over the full Lambek calculus and their connections to residuated lattices, and establish a weak form of the deduction theorem that is known as parametrized local deduction theorem. Finally, we study certain interpolation properties and explain how they imply the amalgamation property for certain varieties of residuated lattices. Dedicated to the memory of Willem Johannes Blok     

Decomposition Proof Systems for Gödel-Dummett Logics

The main goal of the paper is to suggest some analytic proof systems for LC and its finite-valued counterparts which are suitable for proof-search. This goal is achieved through following the general Rasiowa-Sikorski methodology for constructing analytic proof systems for semantically-defined logics. All the systems presented here are terminating, contraction-free, and based on invertible rules, which have a local character and at most two premises.     

Restricted Arrow

In this paper I present a range of substructural logics for a conditional connective ↦. This connective was original introduced semantically via restriction on the ternary accessibility relation R for a relevant conditional. I give sound and complete proof systems for a number of variations of this semantic definition. The completeness result in this paper proceeds by step-by-step improvements of models, rather than by the one-step canonical model method. This gradual technique allows for the additional control, lacking in the canonical model method, that is required.     

Encoding Modal Logics in Logical Frameworks

We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics. We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed -calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO.     

Logics of public communications

Multi-modal versions of propositional logics S5 or S4—commonly accepted as logics of knowledge—are capable of describing static states of knowledge but they do not reflect how the knowledge changes after communications among agents. In the present paper (part of broader research on logics of knowledge and communications) we define extensions of the logic S5 which can deal with public communications. The logics have natural semantics. We prove some completeness, decidability and interpretability results and formulate a general method that solves certain kind of problems involving public communications—among them well known puzzles of Muddy Children and Mr. Sum & Mr. Product. As the paper gives a formal logical treatment of the operation of restriction of the universe of a Kripke model, it contributes also to investigations of semantics for modal logics. This paper was originally published as Plaza, J. A. (1989). Logics of public communications. In M. L. Emrich, M. S. Pfeifer, M. Hadzikadic, & Z.W. Ras (Eds.), Proceedings of the fourth international symposium on methodologies for intelligent systems: Poster session program (pp. 201–216). Publisher: Oak Ridge National Laboratory, ORNL/DSRD-24. Research partly supported by NSF Grant CCR-8702307 and PSC-CUNY Grant 668283.     

Realization for Causal Nondeterministic Input-Output Systems

There are two well-developed formalizations of discrete time dynamic systems that evidently share many concerns but suffer from a lack of mutual awareness. One formalization is classical systems and automata theory. The other is the logic of actions in which the situation and event calculi are the strongest representatives. Researchers in artificial intelligence are likely to be familiar with the latter but not the former. This is unfortunate, for systems and automata theory have much to offer by way of insight into problems raised in the logics of action. This paper is an outline of how the input-output view of systems and its associated solution of state realization may be applied to the formalization of dynamics that uses a situation calculus approach. In particular, because the latter usually admits incompletely specified dynamics, which induces a non-deterministic input-output system behavior, we first show that classical state realization can still be achieved if the behavior is causal. This is a novel systems-theoretic result. Then we proceed to indicate how situation calculi dynamic specifications can be understood in systems-theoretic terms, and how automata can be viewed as models of such specifications. As techniques for reasoning about automata are abundant, this will provide yet more tools for reasoning about actions.