文献

J-GLOBAL ID：201702261335360984   整理番号：17A1190145

カットなし計算自動演えきまで:有界収縮の1例【Powered by NICT】

From Cut-free Calculi to Automated Deduction: The Case of Bounded Contraction

著者 (4件)： Ciabattoni Agata (Vienna University of Technology, Austria) ,  Lellmann Bjorn (Vienna University of Technology, Austria) ,  Olarte Carlos (Universidade Federal do Rio Grande do Norte, Brazil) ,  Pimentel Elaine (Universidade Federal do Rio Grande do Norte, Brazil)
資料名： Electronic Notes in Theoretical Computer Science  (Electronic Notes in Theoretical Computer Science)
巻： 332  ページ： 75-93  発行年： 2017年 
JST資料番号： W2857A  ISSN： 1571-0661  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 交換と弱化(FL)による完全Lambek計算に結合した収縮規則の添加は証明探索のための重篤な合併症を生じる。例えば,FL_に加えこれらの規則の単純なバージョンブレーキカットアドミッシビリティ。これはこれらのルールを洗練することにより避けることができるが,本研究では,FL_+有界収縮のための「良い」証明システムは必ずしも良好な実装を誘導しないことを示した。この問題を解決するために,筆者らは,限界収縮への遅延分割方法論の拡張,集束,カット自由シーケント計算を変換終端定理証明器にかを示すことを提案した。提案システムでは,有界収縮とFL_の決定問題はEXPTIMEであることを示した。Copyright 2017 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【Powered by NICT】

シソーラス用語： *演繹 ,  定理証明 ,  決定問題
準シソーラス用語： シーケント計算 ,  *有界 , 【Automatic Indexing@JST】

著者キーワード (4件)： 証明理論 ,  部分構造論理 ,  証明探索 ,  有界収縮

分類 (2件)： 計算理論  (JB02000A) ,  論理代数  (JB03000H)

タイトルに関連する用語 (4件)： 計算 ,  演えき ,  有界 ,  収縮