12日 午前の部 10:00 開始 12日 10:00 ～ 10:45 立木 秀樹（京都大学） 演題： SUDOKU coloring of a fractal 2-dimensional solid. 梗概： We present a series of self-similar 3-dimensional objects which have similarity dimension 2, and which have the same square shadows when projected along the three (x-, y-, z-) axes. Among them, the one generated from a hexagonal bipyramid is interesting in that it has square shadows when projected along 6 directions. It has nine similitudes of size 1/3, and therefore its level 2 approximation is composed of 81 hexagonal bipyramids, and when it is looked at in 6 directions, we have 3x3 squares composing a large square, and each square is also composed of 3x3 small squares. This pattern is nothing but the "SUDOKU" pattern. We assign 9 colors to the 81 hexagonal bipyramids so that each column and each row and each 9-block have all the nine colors when it is looked at in all the 6 directions. The coloring algorithm applies to any even-level approximation of this fractal solid. 12日 10:45 ～ 11:00 休憩 12日 11:00 ～ 12:00 星野直彦（京都大学） 演題： BCI、BCKからのLCAの構成とrealizability 梗概： 12日 午後の部 13:30 開始 12日 13:30 ～ 14:10 [講演] Jian-Qin LIU (National Institute of Information and Communications Technology, Kobe Advanced ICT Research Center) 演題： On topologically interacted cellular pathways by algebraic operations: an information-theoretic method for proteom-informatics 梗概： Reconstruction of pathway networks is a significant theme in proteom-informatics. However, the complexity derived from the corresponding reconstruction algorithms makes it difficult to obtain the high speed of their computation processes. A novel information-theoretic method is proposed to encode the topological interaction structure of signaling pathways in cells where algebraic operators are designed based on the spatial constraints of the cellular pathways. As a result, polynomial time complexity can be achieved from the topological interaction processes for certain kinds of phosphorylation/dephosphorylation trees where cross-talks among phosphorylation/dephosphorylation trees are described by algebraic operators. 12日 14:10 ～ 15:00 河原康雄（九州大学） 演題： Urysohn の補題の関係理論からの考察 梗概： Urysohn の補題は正規(T4)空間を特徴付けるものとして知られている。 ここでは、この補題の証明を代数的、関係理論的な観点から考察する。 12日 15:00 ～ 15:30 休憩 12日 15:30 ～ 17:00 [講演] Tadeusz Litak (JAIST) 演題： Algebraization of hybrid logic with binders and the bounded fragment of predicate logic 梗概： This paper introduces an algebraic semantics for hybrid logic with binders. It is known that this formalism is a modal counterpart of the bounded fragment of first-order logic, studied by Feferman in the 1960's (Areces, Blackburn, Marx). The algebraization process leads to an interesting class of boolean algebras with operators, called substitution-satisfaction algebras (SSA's). We prove a representation theorem for these algebras and thus provide an algebraic proof of completeness for hybrid logic. Our proof is similar to Andreka-Nemeti algebraic proof of completeness for first-order logic. The fact that the bounded fragment is a conservative reduction class for first-order logic hints that there is a connection between cylindric algebras and SSA's: we identify a subvariety of SSA's, whose term-reducts are cylindric algebras. 13日 午前の部 9:00 開始 13日 9:00 ～ 10:00 藤本 尚子，野口 真理子，鴨 浩靖，新出 尚之 （登壇は藤本） （奈良女子大学） 演題： PrologによるMakeの実装 梗概： We introduce a project to re-implement make in Prolog, called `mipl'. Since make and Prolog have a common feature that they use the backward reasoning to find out a solution, it is natural to re-implement make in Prolog. Using Prolog, we can enjoy various merits such as introducing data structures and using function definitions. In addition, unlike the case of make, we can prevent future appearance of many incompatible extensions, since new features can be added as libraries. This project aims to provide a legitimate replacement of make so that it can compile a whole operating system. In this talk, we describe our designing strategy of mipl and current status of the progress of our project. 13日 10:00 ～ 11:00 西澤弘毅（産業技術総合研究所システム検証研究センター） 演題： Weighted Kripke Structures and Refinement of Models 梗概： We consider binary relations weighted over frames to express intermediate degree of relationship. We reformulate the notions of transition systems, Kripke structures and simulations between them to formulate multi-valued model checking of modal mu-calculus. Discussion on the use of multi-valued model checking to refine models in the usual sense follows. 13日 11:00 ～ 12:00 藤尾光彦（九州工業大学情報工学部システム創成情報工学科） 演題： 正規様相論理の時相拡大について ---数理形態学の論理への応用 --- 梗概： The temporalization problem is the problem of construction and classification of temporalization for a given modal logic. A temporal logic carries two dual pairs of modal operators (F,G) and (P,H). By taking each pair of them, one obtains a normal modal logic. We refer to this situation as a strict temporalization of the normal modal logic. Under mathematical morphological investigation over non-classical logics, we showed that an adjoint pair of modal operators gives rise to a temporal logic. This result can be used to show the existence of a temporalization for a normal modal logic. By combining with canonical models, mathematical morphology illustrates the relationship between a modal logic and its temporalization. 13日 午後の部 13:30 開始 13日 13:30 ～ 14:30 [講演] 加藤有己（奈良先端大） 演題： 確率文法と生物配列解析への応用 梗概： 近年、情報科学と生命科学の融合分野であるバイオインフォマティクスの研 究が盛んに行われている。ここでは、RNA（リボ核酸）の構造を形式文法を 用いてモデル化する試みに焦点を当てる。まず、文脈自由文法（CFG）を定 義し、RNAの構造をCFGでモデル化する方法を解説する。また、CFGを確率文 脈自由文法（SCFG）と呼ばれる確率モデルに拡張し、RNAの構造解析法を説 明する。次に、シュードノットと呼ばれるCFGでは表現できない部分構造を 記述する形式文法として、多重文脈自由文法（MCFG）を紹介し、確率モデル に拡張して構造予測を行った結果を示す。 14:30 ～ 15:00 小林 聡 （こばやし さとし，京都産業大学理学部コンピュータ科学科） 演題： 極限計算可能数学のゲーム意味論 梗概：
代数，幾何，論理と情報科学（ALGI）： 高井 利憲、古澤 仁