直観主義時相線形論理における論理プログラミングについて

情報処理学会 Web Site 被引用文献3件 参考文献19件

書誌事項

タイトル別名
  • チョッカン シュギジソウ センケイ ロンリ ニ オケル ロンリ プログラミング ニ ツイテ
  • Logic Programming in an Intuitionistic Temporal Linear Logic

この論文をさがす

説明

1987年にJ．?Y．Girardによって考え出された線形論理は，環境が動的に変化するソフトウェアを表現するための論理として非常に有望である．しかしながら，線形論理では「動的に変化する環境」を表現することはできるが，「時間経過とともに動的に変化する環境」を表現しきれているとは言えない．これは線形論理には時間の概念が直接的には入っておらず，時間に依存した資源という概念を表現できないからである．そこで，本論文では，線形論理と時相論理の特徴を融合した時相線形論理の体系について述べ，さらにこの体系に基づいた論理型プログラミング言語について述べる．この時相線形論理の体系は，著者らの一人によって考えられたものであり，直観主義線形論理の演算子に加え，次の時刻に1回だけ利用可能な資源を表す様相演算子○，現在以降の任意の時刻に1回だけ利用可能な資源を表す様相演算子□，現在以降の任意の時刻に任意の回数利用可能な資源を表す様相演算子!　を含んでいる．本論文では，Millerのユニフォーム証明の考えを適用することによって，この時相線形論理の体系に対する論理型言語を設計し，HodasのI○モデルの考えを適用することによって，効率的な計算モデルを与える．

Linear logic developed by J.-Y. Girard in 1987 is very useful to describe the software in which the environment changes dynamically. Though it can represent "dynamically changing environment", it cannot naturally represent "time-dependently changing environment" because it lacks the concept of time and cannot represent time-dependent resources. In this paper, we describe a system of temporal linear logic which integrates the features of linear logic and temporal logic, and a logic programming language based on the temporal linear logic system. This system, developed by one of the authors, has a modal operator ○ which represents a resource usable only once at the next clock, a modal operator □ which represents a resource usable only once at any clock of now and after, and a modal operator ! which represents a resource usable any times at any clock of now and after. In this paper, a logic programming language based on this temporal linear logic is designed by using the idea of Miller's uniform proof, and its efficient computation model is given by using the idea of Hodas's I○ model.

収録刊行物

被引用文献 (3)*注記

もっと見る

参考文献 (19)*注記

もっと見る

キーワード

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

問題の指摘

ページトップへ