This paper proposes a new approach to knowledge management for systematizing expert knowledge especially biological knowledge among domain expert communities. In order to understand high-order biological phenomena, it is necessary to bridge the gap between the amount of information in the molecular level and the amount of information in the cell functional level. However, the biological knowledge in the cell functional level has not been systematized well so far. We have been seeking a method to systematically describe and understand cellular behaviors in morphogenesis and developed a biological database system called CBDB (Cell Behavior Database). CBDB is an ontology-based and community-based semantic data web on cell behaviors in the RDF format with multimedia data (e.g. texts, images and movies). In the effort, 2 biologists and their 28 students collected 1500 cell phenomena extracted from academic journals and text book for 3 years in CBDB. The fact will conduct to the result that our approach enhances efficiency of knowledge systematization of knowledge on cell behavior by professional community. In this paper, we will elaborate the CBDB and discuss the methodology for systematization of cell behavior knowledge by a domain expert community on a different level of expertise.

A logic called sequence-indexed linear logic (SLL) is proposed to appropriately formalize resource-sensitive reasoning with sequential information. The completeness and cut-elimination theorems for SLL are proved, and SLL and a fragment of SLL are shown to be undecidable and decidable, respectively. As an application of SLL, some specifications of secure password authentication systems are discussed.

This paper proposes a general framework for a system with a semantic browsing and visualization interface called Knowledge Communication, Collaboration and Creation Browser (KC3 Browser) which integrates multimedia contests and web services on the grid networks, and makes a semantic mash-up called knowledge workspace (k-workspace) with various visual gadgets according to user's contexts (e.g. their interests, purpose and computational environments). KC3 Browser also achieves a link-free browsing for seamless knowledge access by generating semantic links based on an arbitrary knowledge models such as ontology and vector space models. It assists users to look down and to figure out various social and natural events from the web contents. We have implemented a prototype of KC3 Browser and tested it to an international project on risk intelligence against natural disaster.

In this paper, we propose a method for modeling concepts in full computation-tree logic with sequence modal operators. An extended full computation-tree logic, CTLS*, is introduced as a Kripke semantics with a sequence modal operator. This logic can appropriately represent hierarchical tree structures in cases where sequence modal operators in CTLS* are applied to tree structures. We prove a theorem for embedding CTLS* into CTL*. The validity, satisfiability, and model-checking problems of CTLS* are shown to be decidable. An illustrative example of biological taxonomy is presented using CTLS* formulas. © 2011 Wiley Periodicals, Inc.

This paper proposes a general framework of for a system with a semantic browsing and visualization interface called Knowledge Communication, Collaboration and Creation Browser (KC3 Browser) integrates multimedia contests and web services on the grid networks, and makes a semantic mash-up called knowledge workspace (k-workspace) with various visual gadgets according to user's contexts (e.g. their interests, purpose and computational environments).

UML (unified modeling language) is the de facto standard model representation language in software engineering. We believe that automated contradiction detection and repair of UML become very important as UML has been widely used. In this paper, we propose a debugging system using logic programming paradigm for UML class diagram with class attributes, multiplicity, generalization relation and disjoint relation. We propose a translation method of a UML class diagram into a logic program, and using a meta-interpreter we can find (set-inclusion-based) minimal sets of rules which leads to contradiction. Then, we use a minimal hitting set algorithm developed by one of the authors to show minimal sets of deletion of rules in order to avoid contradiction