
Authors:
Yuichi KOMORI
Title:On Komori Algebras
Pages:6770
File:bibtex
Abstract ( + )
Humberstone has defined the notion of a Komori algebra. The present author feels that he would not violate property rights if he broadened the notion of a Komori algebra yet further. The aim of this paper is to do just that and then prove a generalization of Humberstone's result.

Authors:
Marcus KRACHT and Tomasz KOWALSKI
Title:Atomic Incompleteness or how to Kill One Bird with Two Stones
Pages:7178
File:bibtex
Abstract ( + )
We construct a variety of tense algebras that is not generated by its atomic members. Then we lift this result to the case of modal algebras.

Authors:
Motohiko MOURI
Title:Theorem Provers with Countermodels and xpe
Pages:7987
File:bibtex
Abstract ( + )
Xpe is a grammar editor that facilitates typesetting proof trees with TeX. Theorem provers can be called from within xpe, which provides an integrated environment for proof searching and editing, valuable for educational purposes.

Authors:
Yasusi HASIMOTO
Title:Finite Model Property for Some Intuitionistic Modal Logics
Pages:8797
File:bibtex
Abstract ( + )
In this paper, we will show some logic has the finite model property by using filtration method. Although the filtration method for classical modal logics has been studied comprehensively, the method is not completely applied to intuitionistic modal logics yet.

Authors:
Kazuyo INOI
Title:Subframe Formulas for S4type Intuitionistic Modal Logic
Pages:99105
File:bibtex
Abstract ( + )
Subframe formulas for S4type intuitionistic modal logic L_{0} is introduced. It is shown that the logic L_{0}+Y+bw_{n}^{R} with subframe formulas Y has the finite model property, where the formula bw_{n}^{R} means that a given frame is of width < n with respect to the accessibility relation R.

Authors:
Tatsuya SHIMURA
Title:Kripke Completeness of Predicate Extensions of Cofinal Subframe Logics
Pages:107114
File:bibtex
Abstract ( + )
Predicate Extensions of Cofinal Subframe Logics Let BF be the Barcan formula and T(K) the McKinseyTarski translation of Kuroda's formula. We give a class of finite Kripke frames C with the following properties:
1. For any subset {M_{i}} < C, QS4+{α(M_{i},\perp)}+BF+T(K) is strongly Kripke complete.
2. For M \not\in C, QS4+α(M,\perp)+BF+T(K) is Kripke incomplete.

Authors:
Mitio TAKANO
Title:A Modified Subformula Property for K5 and K5D
Pages:115122
File:bibtex
Abstract ( + )
The sequent calculus GK5 (GK5D) for the modal propositional logic K5 (K5D) is presented, and it is shown that, every provable sequent Γ  Θ in GK5 (GK5D) has a GK5proof (GK5Dproof) such that every formula occurring in it is either a subformula of some formulas in Γ, Θ, or the formula LLB or LB, where LB occurs in the scope of some occurrence of L in some formulas of Γ, Θ. Some corollaries including the interpolation property for K5 (K5D) follow from this.