証明手続きとしてのデータ論理

• Item type: SIG Technical Reports(1)
• 公開日: 1990-01-18
• タイトル: 証明手続きとしてのデータ論理
• タイトル / 言語: en
• タイトル: Data Logic As Proof Procedures
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 産能大学経営情報学部
• 著者所属(英): en
• 著者所属(英): Department of Management and Informatics SANNO College
• 著者名: 三浦, 孝夫
• 著者名(英): Takao, Miura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿では、データ論理によるデータモデルの形式化を提案し、また導出原理による完全な証明手続きを有することを言う。データ論理は第一階述語論理を型概念を用いて拡張したもので、データモデルをその解釈とする。定数を主体に、構造を含む項を複合値に対応させ、両者を明示的な宣言により結び付る。構造項を値とする変数を導入することで、動的に定義された構造項を考えることが出来る。質問は、データベースに格納された情報を取り出すだけでなく、型付けによって計算できるものも対象とする。データ論理は形式化のみならず、証明手順としても有用であることを示す。つまり、データ論理による演繹操作のうち、ここでは導出原理による定理証明が完全であることを証明する。構造項を扱うように拡張されたエルブラン領域を用いて、スコーレム定理、エルブラン定理を証明し、単一化を拡張して導出原理が健全且つ完全であることを示す。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we present Data Logic to formalize data models with complex objects, and we show that the Resolution Principle is sound and complete. Data Logic is an extention of the typed first order theory whose interpretation is a semantic model. Constants are considered as entities (objects), structure terms as complex objects. Entities and complex objects are related by explicit declaration. All structures are not assumed to be objects but dynamically defined complex values can be defined by structure-valued variables. The Completeness of the general Resolution Principle on Data Logic presents the solid foundation of Logic Programming and Deductive Databases. To clarify the usefulness, several fundamenta properties are given such as Skolemization, Herbrand theorem as well as other basic operations like typed unifiers.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112482
• 書誌情報: 情報処理学会研究報告データベースシステム（DBS）; 巻 1990, 号 2(1989-DBS-075), p. 1-10, 発行日 1990-01-18
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会