検索結果 59件中 1-20 を表示

  • 1 / 3
  • 直観主義線形論理型言語LLPとそのコンパイラ処理系

    田村 直之 , 番原 睦則

    コンピュータソフトウェア 30(2), 83-89, 2013-04-25

    J-STAGE 参考文献18件

  • 直観主義線形論理型言語LLPとそのコンパイラ処理系

    田村 直之 , 番原 睦則

    コンピュータソフトウェア 30(2), 83-89, 2013

    機関リポジトリ DOI

  • A-001 線形論理型言語を用いた人工化学のための推論の一手法(数理モデル化と問題解決(1),A分野:モデル・アルゴリズム・プログラミング)

    古野 達也 , 冨永 和人

    … 人工化学系における分子の生成可能性を判定するために,線形論理に基づく論理型言語LLPを用いて推論を行うことを試みた.線形論理とは命題を資源に見立てる論理体系である.この論理における命題を我々の人工化学における分子と見なすことで推論を行う.本研究は,この人工化学における推論を行うためのLLPによる記述法を与えた.そしてその記述法を用い,いくつかの人工化学系に対して推論のため …

    情報科学技術フォーラム講演論文集 10(1), 129-130, 2011-09-07

  • 線形論理の誕生

    照井 一成

    數學 62(1), 115-132, 2010-01-27

    参考文献6件

  • 線形論理の誕生

    照井 一成

    数学 62(1), 115-132, 2010

    J-STAGE

  • オーソモジュラ量子論理における含意結合子の強弱について : 量子論理のモルフォロジー解析

    藤尾 光彦

    … 束のモルフォロジーはKripke意味論を介して,論理の解析に適用することができる.例えば,随伴としてのモルフォロジー演算を考察することで正規様相論理の時相化が得られる.ではさらに,直観主義論理および線形論理におけるモデル構成もモルフォロジーによる内部および閉包作用素によって記述され,様々な非古典論理にモルフォロジー解析が適用できることを示した.一方,量子論理は代数的にはオーソモジュラ束ないし …

    電子情報通信学会技術研究報告. SIS, スマートインフォメディアシステム 108(334), 109-112, 2008-11-27

    参考文献16件

  • 4-2 国際規格におけるインタロックの論理構造に関する一考察(セッション4「安全性(2)」)

    池田 博康 , 蓬原 弘一

    … 機械安全の国際規格において重要なインタロック機能の構成論理を示すため、協調作業型の人間/機械システムのインタロックモデルを対象として、その構成条件を2線形論理で表す。 …

    信頼性シンポジウム発表報文集 2008_秋季(21), 49-52, 2008-10-31

    CiNii PDF - オープンアクセス 

  • 機械的構造の情報化

    池田 博康 , 蓬原 弘一

    … 全関連情報として扱って,安全確保の技術原則を論理構造として証明するために,論理変数を用いて機械的操作を表現する.そして,複数のコンポーネントについて安全確保の論現構造を2線形論理に基づく力の伝達系として示す.さらに,これらのコンポーネントで使用される重要部品としてばねの利用が2線形論理において2値化できることを示し,ばねを用いた2線系の論理構造をインタロックモデルで示す. …

    日本信頼性学会誌 : 信頼性 = The journal of Reliability Engineering Association of Japan 30(2), 98-111, 2008-03-01

    参考文献14件

  • 線形論理の誕生(数学基礎論とその応用)

    照井 一成

    数理解析研究所講究録 1525, 94-131, 2006-11

    機関リポジトリ

  • インタラクションネット抽象機械の軽量化

    佐藤伸也 , 杉本 徹

    … インタラクションネットは,線形論理を計算的に解釈したグラフ計算体系である.簡約の影響がグラフ全体に及ぶことがなく,さらに,どの順番で相互作用を行っても同じ結果になることから,並列性を持つ計算体系であるといわれている.インタラクションネットの抽象機械も提案されており,その並列実装も実際に行われている.この抽象機械の基本原理には,グラフを項表現によって定式化した項書き換え計算が …

    情報処理学会論文誌プログラミング(PRO) 47(SIG16(PRO31)), 89-89, 2006-10-15

    情報処理学会

  • パイ計算による仕様を検証する論理体系

    竹内 泉

    … ある.各論理式はある1 個のプロセスの満たす性質を表す.様相記号はプロセスの遷移を表す.プロセスの並行合成に対応して,論理式の文法には並行合成を表す論理記号がある.それは線形論理の乗法的連言によく似た性質を持つ論理記号であり,論理規則もまた線形論理によく似たものとなっている.This presentation gives a logical system which proves the properties over process-terms of a modified variant of …

    情報処理学会論文誌プログラミング(PRO) 46(SIG11(PRO26)), 57-65, 2005-08-15

    情報処理学会

  • 古典線形論理の計算的解釈 Linear CHAM に基づく関数型言語とその並列実行モデル

    佐藤 伸也 , 杉本 徹

    経済情報学論集 20, 67-98, 2005-03-18

  • 線形論理型言語コンパイラ処理系を用いた古典命題線形論理の定理証明システム

    田村 直之 , 番原 睦則 , Naoyuki Tamura , Mutsunori Banbara , 神戸大学学術情報基盤センター , 神戸大学学術情報基盤センター , Information Science and Technology Center Kobe University , Information Science and Technology Center Kobe University

    線形論理型言語コンパイラ処理系のLLPを用いて,古典命題線形論理の論理式の証明探索を行うシステムLL2LLPについて述べる.本システムは,古典命題線形論理式を直観主義線形論理式に変換し,さらにLLPコンパイラを用いてLLP抽象機械命令にコンパイルしたのち実行することで高速な証明探索を実現している点に特徴がある.いくつかの線形論理

    コンピュータソフトウェア = Computer software 22(1), 98-103, 2005-01-26

    CiNii 外部リンク 機関リポジトリ J-STAGE 参考文献23件 被引用文献1件

  • 薬物相互作用の形式オントロジー

    米崎 直樹 , 泉 直子 , 秋山 卓見

    … 本オントロジーは1階論理の公理の集合で与えられるが、その背景となる意味は、線形論理に翻訳された反応の振る舞いにより与えられる。 …

    日本ソフトウェア科学会大会講演論文集 22(0), 460-473, 2005

    J-STAGE

  • 線形論理によるペトリネット設計の一手法とその実装

    猪股 俊光 , 高屋敷 光一

    … 本論文では,対象システムの仕様を満足するペトリネットを機械的に構成するための設計法の確立を目指し,ペトリネットの仕様記述形式としてのPNLL(線形論理の部分体系)を導入し,PN_<LL>で記述された仕様を満たすペトリネットを機械的に構成するためのアルゴリズムを考案した.そして,そのアルゴリズムに基づいた設計支援ツールを実装することにより,PN_<LL>で記述された仕様を入力することで,その仕様を満たす …

    電子情報通信学会論文誌. A, 基礎・境界 87(12), 1528-1541, 2004-12-01

    参考文献9件

  • 線形論理とはどんな論理か

    遠山 茂朗

    一橋研究 29(1), 69-78, 2004-04

    機関リポジトリ DOI

  • 線形論理型言語コンパイラ処理系を用いた古典命題線形論理の定理証明システム

    田村 直之 , 番原 睦則

    … 本論文では,古典命題線形論理の論理式を,著者らの開発した線形論理型言語上で証明探索を行うシステムについて述べる.本システムは,古典線形論理式を直観主義線形論理式に変換し,さらにLLPコンパイラを用いてLLP抽象機械命令にコンパイルしたのち実行することで高速な証明探索を実現している点に特徴がある. …

    日本ソフトウェア科学会大会講演論文集 21(0), 74-74, 2004

    J-STAGE

  • LLPTTP: 線形論理型言語コンパイラ処理系を用いた定理証明システム

    田村 直之 , 番原 睦則 , Naoyuki Tamura , Mutsunori Banbara , 神戸大学学術情報基盤センター , 神戸大学学術情報基盤センター , Information Science and Technology Center Kobe University. , Information Science and Technology Center Kobe University.

    … 一階述語論理の節形式をPrologプログラムに変換し, Prologコンパイラ処理系を用いて定理証明を行うシステムとしてPTTP (Prolog Technology Theorem Prover)が知られている.本論文では,節形式を線形論理型言語LLPのプログラムに変換し, LLPコンパイラ処理系を用いることで,より効率的な証明探索が可能になることを示す.特に,証明中のリテラルをリソースとして追加することにより, ME (model elimination)処理を高速化している点に特徴があ …

    コンピュータソフトウェア = Computer software 20(5), 502-508, 2003-09-25

    CiNii 外部リンク 機関リポジトリ 参考文献13件

  • 1 / 3
ページトップへ