In this paper, a system called Caretta that integrates personal and shared workspaces to support face-to-face collaboration is described. We use PDAs for individual users' personal workspaces that enable them to reflect on their own idea. A shared workspace has been implemented by using a multiple-input sensing board, which allows a group of users to simultaneously manipulate physical objects. In order to raise the level of awareness among users, we have used augmented reality technologies and created an immersive environment for (...) the users' shared workspace. Users of Caretta can discuss and negotiate with each other in the shared workspace, while they individually examine their ideas in their own personal workspaces. Therefore, Caretta allows users to participate in group activities interchangeably and seamlessly by using both these workspaces. Caretta can be used for several types of group activities. In this paper, it is used for supporting a group of users in urban planning tasks by allowing the users to actually construct a town on the shared space and evaluate the town through computer simulations. User studies to evaluate Caretta were conducted. Usage logs of Caretta, video analyses, and comments from users proved that each user could utilize personal and shared space interchangeably at their own pace and without being hindered by other users. (shrink)

An evaluation method, similar to the two-valued one for the classical logic, is introduced to give a decision procedure for some of intermediate logics. The logics treated here are obtained from some logics by adding the axiom av a.

The intermediate logics have been classified into slices (cf. Hosoi [1]), but the detailed structure of slices has been studied only for the first two slices (cf. Hosoi and Ono [2]). In order to study the structure of slices, we give a method of a finer classification of slices & n (n 3). Here we treat only the third slice as an example, but the method can be extended to other slices in an obvious way. It is proved (...) that each subslice contains continuum of logics. A characterization of logics in each subslice is given in terms of the form of models. (shrink)

We give a Gentzen-type formulation GQ for the intermediate logic LQ and prove the cut-elimination theorem on it, where LQ is the propositional logic obtained from the intuitionistic propositional logic LI by adding the axioms of the form AV A.

This paper gives a new, purely semantic proof of the following theorem: if an intermediate propositional logic L has the disjunction property then a disjunction free formula is provable in L iff it is provable in intuitionistic logic. The main idea of the proof is to use the well-known semantic criterion of the disjunction property for "simulating" finite binary trees (which characterize the disjunction free fragment of intuitionistic logic) by general frames.

The simple substitution property provides a systematic and easy method for proving a theorem by an axiomatic way. The notion of the property was introduced in Hosoi [4] but without a definite name and he showed three examples of the axioms with the property. Later, the property was given it's name as above in Sasaki [7].Our main result here is that the necessary and sufficient condition for a logicL on a finite slice to have the simple substitution property is (...) thatL is finite. Here the necessity part is essentially new, for the sufficiency part has been proved in Hosoi and Sasaki [5]. Also the proof of sufficiency part is improved here. (shrink)

An example of finite tree Mo is presented such that its predicate logic (i.e. the intermediate predicate logic characterized by the class of all predicate Kripke frames based on Mo) is not finitely axiomatizable. Hence it is shown that the predicate analogue of de Jongh - McKay - Hosoi's theorem on the finite axiomatizability of every finite intermediate propositional logic is not true.

1. A. Heyting (1930) introduced an intermediate logic whose semantics is based on a pair of states (‘here’ and ‘there’). This logic was axiomatized by Hosoi (1966), using the sequence of intermedia...

A classification of commutative BCK-logics which is an analogon of Hosoi classification of intermediate logics is given in the paper.

Medvedev's intermediate logic (MV) can be defined by means of Kripke semantics as the family of Kripke frames given by finite Boolean algebras without units as partially ordered sets. The aim of this paper is to present a proof of the theorem: For every set of connectives such that the-fragment ofMV equals the fragment of intuitionistic logic. The final part of the paper brings the negative solution to the problem set forth by T. Hosoi and H. Ono, namely: is (...) an intermediate logic based on the axiom (abc) (ab)(a c) separable? (shrink)