一階論理の形式化によるオブジェクト指向モデルの記述言語と推論系

情報処理学会

書誌事項

タイトル別名
  • A Description Language and its Reasoning System for Object-Oriented Models by First-Order Logic Formalization

この論文をさがす

抄録

近年,ソフトウェアの大規模化・複雑化にともない,C++をはじめとするオブジェクト指向言語が多用されるようになってきた.オブジェクト指向では,複数のオブジェクトが独立・並行して動作し,メッセージ通信により相互作用するものとして捉えるため,システムの分析・設計においても様々な視点からモデル化されてきた.従来より,形式的記述法として以下の言語が提案されている.(1)時間論理,ダイナミック論理.(2)E-R図,データフロー図,状態推移図.(3)代数型仕様記述言語.各言語は,固有の数学的・形式的体系,固有の記述範囲と表現能力をもつため,オブジェクト指向の分析・設計や検証・合成の過程では,いくつかの言語を組合わせる融合手法がとられる.しかしながら,それぞれの言語で表現する内容は相互に依存しており,それらの間の関係は,自然言語などの非形式的な記述により与えられる.本論文では,時間や動作,状態の推移,対象の性質や関係などの対象レベル,オブジェクト指向の抽象レベルと,検証や合成における証明過程などのメタレベルを統合的に記述できる一階論理言語とその推論系を提案する.本手法では,構成的数学における論理式の証明可能性解釈の考え方と,最近の自然言語の形式意味論であるプロパティ理論ならびに情報の論理の意味論に基づいている.そして,一階論理による推論機構を実現するため,動作に関するデフォルト推論,メタレベル推論とリフレクション,信念修正機構など,知識工学における研究成果を応用した人工知能的アプローチをとる.ここでは,論理式の意味を真理条件的・モデル論的でなく,証明可能性解釈に基づいて様相輪理の各機の意味論を一階論理により形式化している.これにより,対象世界における種々の概念の記述を統合化するとともに,効率的な推論が行なえる論理型言語を与えている.

収録刊行物

詳細情報 詳細情報について

問題の指摘

ページトップへ