神戸大学学術情報基盤センター

論文一覧:  7件中 1-7 を表示

  • SATによるシステム検証(<特集>最近のSAT技術の発展)

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

    人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence 25(1), 122-129, 2010-01-01

    JSAI 参考文献31件 被引用文献5件

  • 制約最適化問題とSAT符号化(<特集>最近のSAT技術の発展)

    田村 直之 , 丹生 智也 , 番原 睦則 , Naoyuki Tamura , Tomoya Tanjo , Mutsunori Banbara , 神戸大学学術情報基盤センター , 神戸大学大学院工学研究科 , 神戸大学学術情報基盤センター , Information Science and Technology Center Kobe University , Graduate School of Engineering Kobe University , Information Science and Technology Center Kobe University

    人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence 25(1), 77-85, 2010-01-01

    JSAI 参考文献40件 被引用文献4件

  • SATソルバーの基礎(<特集>最近のSAT技術の発展)

    井上 克巳 , 田村 直之 , Katsumi Inoue , Naoyuki Tamura , 国立情報学研究所:総合研究大学院大学情報学専攻 , 神戸大学学術情報基盤センター , National Institute of Informatics:Department of Informatics The Graduate University for Advanced Studies , Information Science and Technology Center Kobe University

    人工知能学会誌 = Journal of Japanese Society for Artificial Intelligence 25(1), 57-67, 2010-01-01

    JSAI 参考文献56件 被引用文献8件

  • PrologからJavaへのトランスレータ処理系とその応用

    番原 睦則 , 田村 直之 , 井上 克巳 , Mutsunori Banbara , Naoyuki Tamura , Katsumi Inoue , 神戸大学学術情報基盤センター , 神戸大学学術情報基盤センター , 国立情報学研究所 , Information Science and Technology Center Kobe University , Information Science and Technology Center Kobe University , National Institute of Informatics

    本論文では,PrologからJavaへのトランスレータ処理系Prolog Cafeについて述べる.本システムでは,Prologプログラムは,WAMを介して,Javaプログラムに変換され,既存のJava処理系を用いてコンパイル・実行される.つまりProlog Cafeでは,項,述語などPrologの構成要素のすべてがJavaに変換される.このため,PrologCafeはJavaとの連携,拡張性に優れ …

    コンピュータソフトウェア = Computer software 24(3), 75-86, 2007-07-26

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

  • 制約条件に論理的ORを含む組合せ最適化問題に対するハイブリッド型最適化手法の実現(サイバー増大ページ論文概要,サイバー増大号)

    大西 秀志 , 田村 直之 , Shuji Ohnishi , Naoyuki Tamura , 神戸大学大学院自然科学研究科 , 神戸大学学術情報基盤センター

    コンピュータソフトウェア = Computer software 22(3), 95, 2005-07-26

    CiNii 外部リンク 機関リポジトリ

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

    田村 直之 , 番原 睦則 , 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件

  • 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コンパイラ処理系を用いることで,より効率的な証明探索が可能になることを示す.特に,証明中のリテラルをリソースとして追 …

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

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

ページトップへ