Proof Systems for Reasoning about Computation Errors

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. Presented by Yaroslav Shramko and Heinrich Wansing     

K Altn的另一族正规扩张

Bellissima证明KAltn的正规扩张都是典范的,并且给出了一族连续统多的无有穷模型性的逻辑,本文构造出了KAltn的另一族连续统多的正规扩张,并且证明它们与Bellissima给出的颇为不同,它们要小得多,并且都具有有穷模型性。     

Matrices,primitive satisfaction and finitely based logics

We examine the notion of primitive satisfaction in logical matrices. Theorem II. 1, being the matrix counterpart of Baker's well-known result for congruently distributive varieties of algebras (cf [1], Thm. 1.5), links the notions of primitive and standard satisfaction. As a corollary we give the matrix version of Jónsson's Lemma, proved earlier in [4]. Then we investigate propositional logics with disjunction. The main result, Theorem III. 2, states a necessary and sufficient condition for such logics to be finitely based.     

A Hierarchy of Weak Double Negations

In this paper, a way of constructing many-valued paraconsistent logics with weak double negation axioms is proposed. A hierarchy of weak double negation axioms is addressed in this way. The many-valued paraconsistent logics constructed are defined as Gentzen-type sequent calculi. The completeness and cut-elimination theorems for these logics are proved in a uniform way. The logics constructed are also shown to be decidable.     

Modal translations in substructural logics

Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S40type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained with the help of cut climination for sequent formulations of our substructural logics and their modal extensions. These results are proved for systems with equality too.     

On Logics with Coimplication

This paper investigates (modal) extensions of Heyting–Brouwer logic, i.e., the logic which results when the dual of implication (alias coimplication) is added to the language of intuitionistic logic. We first develop matrix as well as Kripke style semantics for those logics. Then, by extending the Gödel-embedding of intuitionistic logic into S4 , it is shown that all (modal) extensions of Heyting–Brouwer logic can be embedded into tense logics (with additional modal operators). An extension of the Blok–Esakia-Theorem is proved for this embedding.     

Deduction theorems for RM and its extensions

In this paper logics defined by finite Sugihara matrices, as well as RM itself, are discussed both in their matrix (semantical) and in syntactical version. For each such a logic a deduction theorem is proved, and a few applications are given.     

Theory matrices (for modal logics) using alphabetical monotonicity

In this paper I give conditions under which a matrix characterisation of validity is correct for first order logics where quantifications are restricted by statements from a theory. Unfortunately the usual definition of path closure in a matrix is unsuitable and a less pleasant definition must be used. I derive the matrix theorem from syntactic analysis of a suitable tableau system, but by choosing a tableau system for restricted quantification I generalise Wallen's earlier work on modal logics. The tableau system is only correct if a new condition I call alphabetical monotonicity holds. I sketch how the result can be applied to a wide range of logics such as first order variants of many standard modal logics, including non-serial modal logics.     

Axiomatizations with Context Rules of Inference in Modal Logic

A certain type of inference rules in (multi-) modal logics, generalizing Gabbay's Irreflexivity rule, is introduced and some general completeness results about modal logics axiomatized with such rules are proved.     

Comparing Semantics of Logics for Multi-Agent Systems

We draw parallels between several closely related logics that combine — in different proportions — elements of game theory, computation tree logics, and epistemic logics to reason about agents and their abilities. These are: the coalition game logics CL and ECL introduced by Pauly 2000, the alternating-time temporal logic ATL developed by Alur, Henzinger and Kupferman between 1997 and 2002, and the alternating-time temporal epistemic logic ATEL by van der Hoek and Wooldridge (2002). In particular, we establish some subsumption and equivalence results for their semantics, as well as interpretation of the alternating-time temporal epistemic logic into ATL. The focus in this paper is on models: alternating transition systems, multi-player game models (alias concurrent game structures) and coalition effectivity models turn out to be intimately related, while alternating epistemic transition systems share much of their philosophical and formal apparatus. Our approach is constructive: we present ways to transform between different types of models and languages.     

The logics of orthoalgebras

The notion of unsharp orthoalgebra is introduced and it is proved that the category of unsharp orthoalgebras is isomorphic to the category of D-posets. A completeness theorem for some partial logics based on unsharp orthoalgebras, orthoalgebras and orthomodular posets is proved.     

Tableaus for many-valued modal logic

We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.Research partly supported by NSF Grant CCR-9104015.     

Interpolation and Amalgamation; Pushing the Limits. Part I

Continuing work initiated by Jónsson, Daigneault, Pigozzi and others; Maksimova proved that a normal modal logic (with a single unary modality) has the Craig interpolation property iff the corresponding class of algebras has the superamalgamation property (cf. [Mak 91], [Mak 79]). The aim of this paper is to extend the latter result to a large class of logics. We will prove that the characterization can be extended to all algebraizable logics containing Boolean fragment and having a certain kind of local deduction property. We also extend this characterization of the interpolation property to arbitrary logics under the condition that their algebraic counterparts are discriminator varieties. We also extend Maksimova's result to normal multi-modal logics with arbitrarily many, not necessarily unary modalities, and to not necessarily normal multi-modal logics with modalities of ranks smaller than 2, too.The problem of extending the above characterization result to no n-normal non-unary modal logics remains open.Related issues of universal algebra and of algebraic logic are discussed, too. In particular we investigate the possibility of extending the characterization of interpolability to arbitrary algebraizable logics.     

Products of modal logics and tensor products of modal algebras

One of natural combinations of Kripke complete modal logics is the product, an operation that has been extensively investigated over the last 15 years. In this paper we consider its analogue for arbitrary modal logics: to this end, we use product-like constructions on general frames and modal algebras. This operation was first introduced by Y. Hasimoto in 2000; however, his paper remained unnoticed until recently. In the present paper we quote some important Hasimoto's results, and reconstruct the product operation in an algebraic setting: the Boolean part of the resulting modal algebra is exactly the tensor product of original algebras (regarded as Boolean rings). Also, we propose a filtration technique for Kripke models based on tensor products and obtain some decidability results.     

Provability logics for natural turing progressions of arithmetical theories

Provability logics with many modal operators for progressions of theories obtained by iterating their consistency statements are introduced. The corresponding arithmetical completeness theorem is proved.     

Equivalential logics (II)

In the first section logics with an algebraic semantics are investigated. Section 2 is devoted to subdirect products of matrices. There, among others we give the matrix counterpart of a theorem of Jónsson from universal algebra. Some positive results concerning logics with, finite degrees of maximality are presented in Section 3.     

Kripke semantics for knowledge representation logics

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.     

The shortest possible length of the longest implicational axiom

A four-valued matrix is presented which validates all theorems of the implicational fragment, IF, of the classical sentential calculus in which at most two distinct sentence letters occur. The Wajsberg/Diamond-McKinsley Theorem for IF follows as a corollary: every complete set of axioms (with substitution and detachment as rules) must include at least one containing occurrences of three or more distinct sentence letters.Additionally, the matrix validates all IF theses built from nine or fewer occurrences of connectives and letters. So the classic result of Jaskovski for the full sentential calculus —that every complete axiom set must contain either two axioms of length at least nine or else one of length at least eleven—can be improved in the implicational case: every complete axiom set for IF must contain at least one axiom eleven or more characters long.Both results are best possible, and both apply as well to most subsystems of IF, e.g., the implicational fragments of the standard relevance logics, modal logics, the relatives of implicational intutionism, and logics in the ukasiewicz family.Earlier proofs of these results, utilizing a five-valued matrix built from the product matrix of C2 with itself via the method of [8], were obtained in 1988 while the author was a Visiting Research Fellow at the Automated Reasoning Project, Research School of Social Sciences, Australian National University, and were presented in [9]. The author owes thanks to the RSSS for creating the Project, and to the members of the Project generally for the stimulating atmosphere they created in turn, but especially to Robert K. Meyer for making the visit possible, and for many discussions over the years.     

Maximal and Premaximal Paraconsistency in the Framework of Three-Valued Semantics

Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain from classical logic as much as possible. In this paper we introduce the strongest possible notion of maximal paraconsistency, and investigate it in the context of logics that are based on deterministic or non-deterministic three-valued matrices. We show that all reasonable paraconsistent logics based on three-valued deterministic matrices are maximal in our strong sense. This applies to practically all three-valued paraconsistent logics that have been considered in the literature, including a large family of logics which were developed by da Costa’s school. Then we show that in contrast, paraconsistent logics based on three-valued properly nondeterministic matrices are not maximal, except for a few special cases (which are fully characterized). However, these non-deterministic matrices are useful for representing in a clear and concise way the vast variety of the (deterministic) three-valued maximally paraconsistent matrices. The corresponding weaker notion of maximality, called premaximal paraconsistency, captures the “core” of maximal paraconsistency of all possible paraconsistent determinizations of a non-deterministic matrix, thus representing what is really essential for their maximal paraconsistency.     

An Elementary Construction for a Non-elementary Procedure

We consider the problem of the product finite model property for binary products of modal logics. First we give a new proof for the product finite model property of the logic of products of Kripke frames, a result due to Shehtman. Then we modify the proof to obtain the same result for logics of products of Kripke frames satisfying any combination of seriality, reflexivity and symmetry. We do not consider the transitivity condition in isolation because it leads to infinity axioms when taking products.