直観主義時相線形論理における論理プログラミングについて 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.

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 IO model.

収録刊行物

  • 情報処理学会論文誌プログラミング(PRO)  

    情報処理学会論文誌プログラミング(PRO) 41(SIG04(PRO7)), 11-23, 2000-06-15 

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

参考文献:  21件

被引用文献:  3件

各種コード

  • NII論文ID(NAID)
    110002725385
  • NII書誌ID(NCID)
    AA11464814
  • 本文言語コード
    JPN
  • 資料種別
    Article
  • ISSN
    1882-7802
  • NDL 記事登録ID
    5731772
  • NDL 請求記号
    Z74-C192
  • データ提供元
    CJP書誌  CJP引用  NDL  IPSJ 
ページトップへ