著者

市川 至 蓬莱尚幸 佐伯 元司 米崎 直樹 榎本 肇

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.27, no.11, pp.1112-1128, 1986-11-15

被引用文献数

1

---

本論文では 自然言語ベースの仕様記述言語TELL/NSLにおけるシステムの静的な仕様記述から 変換により実行可能なPrologプログラムを得てテストデータによる試験を行うラピッドプロトタイピング手法について述べる.TELL/NSLの仕様記述は まずその意味となる1階述語論理式へ変換され 次にホーン節型式に変換される.さらに 述語の入出力モードを入出力依存グラフを利用して決定し その入出力モードに基づき正しい動作をするようにPrologの実行制御を考慮してリテラルや節の並べ換えを行い 実行可能なPrologプログラムに変換する.これらの変換は 段階的に適応される部分変換からなり それぞれの変換では健全性が保証され 全体の変換により得られるプログラムは元の仕様記述を満たし部分正当であることが保証される.得られたプログラムを実行しデータ試験を行うことにより 元の仕様記述において不明確な点を発見することが可能となった.

著者

萩原 茂樹 米崎 直樹

出版者

一般社団法人 日本応用数理学会

雑誌

応用数理 (ISSN:24321982)

巻号頁・発行日

vol.17, no.4, pp.291-301, 2007-12-26 (Released:2017-04-08)

参考文献数

10

---

暗号プロトコルの解析は,確率的多項式時間チューリング機械を用いる計算論的手法と,Dolev-Yaoモデルに基づく記号論的手法がそれぞれ独立に研究されてきた.記号論による解析は,抽象レベルの解析とみなせ簡潔で分かりやすい一方,記号論による解析結果と計算論による解析結果の対応が明らかでなかった.この問題に対してAbadiとRogawayは,完全な対称鍵暗号方式を前提としてメッセージの見た目の等価性を記号論的に定義し,メッセージが等価ならばそれらは計算論的に識別不可能であること,すなわち記号論によるメッセージの識別不可能性の計算論的意味づけに対する健全性を示した.さらに,MicciancioとWarinschiはその完全性を示している.本稿では,これら内容を中心に関連する研究を含め紹介を行う.

著者

秋山 卓見 泉 直子 萩原 茂樹 米崎 直樹

出版者

一般社団法人情報処理学会

雑誌

情報処理学会研究報告バイオ情報学(BIO) (ISSN:09196072)

巻号頁・発行日

vol.2007, no.21, pp.71-78, 2007-03-05

参考文献数

6

---

近年の分子生物学の進展の中において,遺伝子ノックダウン実験による遺伝子調節ネットワークの解明が進んでいる.本研究では,それらを計算論的モデルを用いて捉えなおし,形式手法を反映したかたちで解析したすなわち,化学反応の活性/抑制関係を表現した,資源の取り合いを基本概念とする意味論を持つ形式オントロジーの公理を満たす,遺伝子調節量を表す数値間の演算の代数的制約と,そのインスタンスとなる関数を提案した.また,遺伝子調節ネットワークを解析した実験結果に適用し,ダブルノックダウン実験による遺伝子調節値を推定する計算式を提案した.The gene regulatory network obtained from the gene knockdown experiment is clarified in the progress of the molecular biology. In this paper, we capture those results by using the computational model, and analyze by a formal method, i.e. we proposed a numeric model of gene regulation reflecting our formal ontology that conceptualized promoting/inhibiting relation of the chemical reactions. Moreover, we formally defined requirements for gene regulation and functions which satisfy this requirements. Finally, we estimated the numerical value of the gene regulation by the double-knockdown experiment with this model.

著者

片山 卓也 渡辺 治 佐伯 元司 米崎 直樹

出版者

東京工業大学

雑誌

一般研究(A)

巻号頁・発行日

1986

---

属性文法にもとづくソフトウェア自動合成システムの講成法についての研究を行った。このようなシステムの構成には、適切な仕様記述言語とそれで書かれた仕様からソフトウェアを生成するためのシステムが存在しなければならないが、本研究では、それらのいずれをも属性文法にもとづく形式的体系で記述しようとしたものである。元来、属性文法はプログラム言語の意味記述のために導入された形式的体系であるが、その本質は木構造上の関数的計算であり、ソフトウェアやその構成プロセス、ソフトウェアオブジェクトベースの記述には有効な形式的体系である。本研究はこのような観点にたって、ソフトウェア自動合成システムの構成に属性文法にもとづく形式的体系を用いようとしたものである。本研究で得られた主な成果は次の通りである。1.属性文法にもとづく階層的関数型言語AGとそのプログラミング環境SAGEシステムの構成、2.階層的関数型ソフトウェアプロセスモデルHFSPの提案とそのSAGEシステム上での実働化、3.オブジェクト指向属性文法OAGの提案とその評価法、およびソフトウェアデータベース記述への応用。言語AGとその環境SAGEについては、言語の仕様決定、SAGEシステムの各構成要素の設計と構成を行ったが、現在SAGEシステムは一般公開が可能な状態になっている。ソフトウェアプロセスモデルHFSPは、属性文法にもとづく階層的関数型計算モデルをソフトウェアプロセスに適用したものであり、いくつかのソフトウェアプロセスの記述およびそのSAGE上でのプロトタイプ実現を通してその有効性を確かめることが出来た。OAGはオブジェクト指向的機構を用いて属性文法に状態や自己改変概念を導入したものである。OAGの形式化、評価法およびオブジェクトベースの代表的局面の記述を通して、OAGの有効性を確認することができた。

著者

米崎 直樹

出版者

一般社団法人情報処理学会

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.30, no.6, pp.p641-650, 1989-06-15

被引用文献数

4

---

641-651

著者

吉浦 紀晃 米崎 直樹

雑誌

全国大会講演論文集

巻号頁・発行日

vol.55, pp.553-554, 1997-09-24

被引用文献数

1

---

論理の主たる目的は, 人間の行なう演繹的な推論を形式化することである。しかし, 古典論理における含意「ならば」は, 日常利用する「ならば」とは, 違和を感じる箇所もある。例えば, 古典論理では, 「2+3=5」が真であることから, 「雪は白いならば, 2+3=5」が真となる。しかし, このような推論は, 奇異に感じられる。古典論理の含意が持つこのような違和感は次のように3つに分類される。1. 関連性の違和感 A→(B→A), 2. 恒真性の違和感 (A∧¬A)→B, A→(B∨¬B), 3. 偶然性の違和感 A→((A→B)→B)。適切さの論理は, これらの違和感を除去することを目的として研究されてきた。Lewisによる関連性の違和感が除去された厳密含意の提案に始まり, 多くの適切さの論理の体系が提案されている。代表的な体系としては, ChurchやMohによる, 関連性と恒真性の違和感が除去された論理体系Rや, Ackennannによる, すべての違和感が除去された論理体系Eなどがある。関連性・恒真性の違和感は強い違和感とみなされ, ほとんどの体系で, これらは除去されている。一方, 適切さの論理では, 体系が弱いという問題がある。例えば, 自然演繹における推論規則Disjunctive syllogism (DS)が許されない。[numerical formula]この推論規則が認められない理由は, 以下のように(A∨¬A)+Bが証明可能となるためである。[numerical formula][5]では, DSが問題のある規則と見なされ, 適切さの論理では, この推論規則は除去されている。また, 違和感を含んでいない以下の式が, 適切さの論理では定理ではない。1. A→(B→(A∧B)), 2. A→(A∧(B∨¬B))。適切さの論理では, 1.が定理である場合, A→(B→A)が定理となり, また, 2.が定理である場合, A→(B∨¬B)が定理となるため, これら2つの式は定理とはならない。このように, 適切さの論理では, 違和感を除去するために, 結果として, 定理となることが自然であると考えられる式が定理とはならず, また, 自然な推論規則が成り立たない。本稿では, 関連性・恒真性の違和感が除去されており, 体系Rよりも強い論理体系ERを提案する。ERは, [4]に示されているsequentによる自然演繹の体系として与えられ, 各推論規則では, 式の属性が利用される。この属性は, 証明を制御し, 違和感を含む式の推論を防ぐために利用される。また, 属性を利用する点からみると, ERは, Labelled deductive systemの一種であるといえる。