反証機能付き書き換え帰納法のための補題自動生成法
スポンサーリンク
概要
- 論文の詳細を見る
- 日本ソフトウェア科学会の論文
- 2009-04-24
著者
-
草刈 圭一朗
名古屋大学大学院情報科学研究科
-
嶌津 聡志
日本電信電話株式会社NTTアクセスサービスシステム研究所
-
外山 芳人
東北大学電気通信研究所
-
青戸 等人
東北大学電気通信研究所
-
嶌津 聡志
NTTアクセスサービスシステム研究所
関連論文
- 基本対称関数に基づく節をもつCNF論理式の充足可能性判定(計算論,計算モデル)
- ビットエラー通信路におけるスケーラブルCANの動作解析
- R&Dホットコーナー ソリューション 支障移転等の切替工事で通話中確認を実現するFTTH区間通信モニタ技術
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について (ソフトウェアサイエンス)
- シャローな依存対から構成される項書換え系の停止性の決定可能性
- 基本対称関数を付加したCNF論理式の充足可能性判定
- 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序
- プレスブルガー文付き項書換え系における書換え帰納法について
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)
- 等式を規則化する変換の停止条件
- 単純型付き項書き換え系における静的依存対法とその周辺
- 動的型言語への柔らかい型付けによるエラー検出
- 対話型埋込みによる数独問題の設計ツール
- プログラム生成系GeneSysにおける等式仕様への否定の導入
- 導出木からのループ検出による論理プログラムの非停止性証明法
- 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
- 左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン
- B-6-47 FTTHにおけるサービスモニタリング方式の検討(B-6.ネットワークシステム,一般セッション)
- B-8-50 次世代アクセスサービスノードにおける高速冗長切替方式の検討(B-8.通信方式,一般セッション)
- 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み
- 帰納的定理の決定可能なクラスについて
- B-8-31 DBA情報を用いたPON-OLT省電力化方式の提案と性能評価(B-8.通信方式,一般セッション)
- 高階書換え系における引数切り落とし法と実効規則
- 項書き換えシステムの合流性自動判定
- 難解言語Malbolgeのチューリング完全性について
- A-033 S式書き換えシステムの停止性を保証するカリー化について(モデル・アルゴリズム・プログラミング,一般論文)
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について
- 木準同型写像を用いた項パターンマッチング
- 条件付き等式の変換に基づくプログラム生成
- 反証機能付き書き換え帰納法のための補題自動生成法
- 制約付き項書換え系における書換え帰納法
- プレスブルガー文付き項書換え系における書換え帰納法について
- 関数プログラムの停止性証明のための辞書式経路順序
- 高階書換え系における引数切り落とし法と実効規則
- 単純型項書換え系における定理自動証明系HOPSYS
- 新しいソフトウェアの実現 : 科研「情報学」プロジェクトA01柱を振り返って(「情報学を創る」-科研プロジェクトがめざしたもの)
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- LA-009 項書き換えシステムの合流性自動判定(モデル・アルゴリズム・プログラミング)
- 等式理論を法とするDPLL遷移系について
- 項正規表現に基づくSpi計算の機密性検証
- 等式付き書換え系の等式数を削減する変換
- ナローイング計算の停止性証明のための依存グラフ法
- 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け(基礎理論,フォーマルアプローチ論文)
- 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け
- 強計算性に基づいた単純型項書換え系の停止性証明法
- 静的依存対法による高階書換え系の停止性証明
- 強計算依存対法による高階書換え系の停止性証明
- LA-002 パターンに基づくプログラム変換における列変数の導入(A分野:モデル・アルゴリズム・プログラミング)
- A-032 多重Knuth-Bendix完備化における危険対除去手法の導入(モデル・アルゴリズム・プログラミング,一般論文)
- A-034 基底項書き換え系の合流性自動判定(モデル・アルゴリズム・プログラミング,一般論文)
- R&Dホットコーナー ソリューション 長距離伝送を可能とするGE-PONシステムの光パワーバジェット拡大技術
- 左線形シャローなどの項書換え系の停止性の決定性
- 準構成子項書換え系における停止性の決定問題
- 重なりを持つTRSにおける最外戦略の完全性について
- 修正AC単調意味論経路順序によるAC停止性
- 修正AC単調意味論経路順序によるAC停止性
- 優先順序付き書き換えの計算モデル
- 項書き換え系のパーシステント性の順序付きソートによる拡張
- Extending persistency of confluence with ordered sorts
- Top-down labelling and modularity of term rewriting systems
- Persistency of confluence
- Persistency of confluence
- GE-PONパケットキャプチャによるロケーション&データベースフリー光線路試験システム (光ファイバ応用技術)
- B-10-56 FTTHにおける適応型サービスモニタリング方式の検討(B-10.光通信システムB(光通信),一般セッション)
- 順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について
- 制約付き木オートマトンとその閉包性
- 無限項書き換えシステムにおける性質に関する考察 (代数と言語のアルゴリズムと計算理論)
- B-10-13 OAM機能を用いた光線路試験システムのロケフリーONU位置検出(B-10. 光通信システムA(光ファイバ伝送路),一般セッション)
- GE-PONパケットキャプチャによるロケーション&データベースフリー光線路試験システム(光ファイバケーブル・コード,通信用光ファイバ,光ファイバ線路構成部品,光線路保守監視・試験技術,接続・配線技術,光ファイバ測定技術,光コネクタ,ホーリーファイバ,機能性光ファイバ,光信号処理,光ファイバ型デバイス,光測定器,レーザ加工,ハイパワーレーザ光輸送,光給電,一般)
- 2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み
- 高階書換え系における引数切り落とし関数の下での実効規則について (システム数理と応用)
- 高階書換え系における引数切り落とし関数の下での実効規則について (ソフトウェアサイエンス)
- 通信モニタ技術を用いた光線路切替工事の効率化 (放送技術)
- 三値関数を実現するMalbolge命令列の発見のためのSATエンコーディング
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて
- 語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成
- 関数呼び出しを持つプログラムの非線形ループ不変式の自動生成
- 高階書換え系における引数切り落とし関数の下での実効規則について
- 高階書換え系における引数切り落とし関数の下での実効規則について
- 単純型付き項書換え系における書換え帰納法について
- 単純型付き項書換え系における書換え帰納法について
- 通信モニタ技術を用いた光線路切替工事の効率化(光アクセスシステム・次世代PON、地上・衛星放送システム、衛星通信システム、CATVシステム、イーサネット、伝送監視制御、光ファイバケーブル・コード、通信用光ファイバ、光線路保守監視・試験技術、光ファイバ測定技術、地上・衛星放送関連デバイス・機器・設備、家庭用受信デバイス・機器、ホーリーファイバ、機能性光ファイバ、光ファイバ線路構成部品、光回路部品、周波数有効利用技術、変復調技術、電磁界解析およびシミュレーション技術、無線・光伝送境界領域、光ケーブル布設技術、
- 通信モニタ技術を用いた光線路切替工事の効率化
- 通信モニタ技術を用いた光線路切替工事の効率化