| 講演名 | 1995/7/14 全ての変数が存在記号で束縛された冠頭標準形プレスブルガー文の真偽判定プログラム 森岡 澄夫, 東野 輝夫, 谷口 健一, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 加算と比較演算からなる整数上の閉論理式は,プレスブルガー文(以下P文)と呼ばれる.本稿では,全ての変数が存在記号で束縛された冠頭標準形のP文の真偽を,少ないメモリ使用量で高速に判定できるプログラムの実現と,その評価について述べる.本ルーチンでは,式中の変数を一つずつ消去して等価な式を構成していくCooperのアルゴリズムを,次のように工夫して実現した:(i)判定するP文が上述の冠頭標準形をしていることを利用し,変数消去を,式の部分ごと,再帰的に行うことにした.これにより,生じる整数係数が固定長の一語で扱えるという条件のもとで,式長の多項式オーダの領域で判定が行えるようになった.(ii)判定を高速化するため,構文木の根の近い変数から消去するなど,変数の消去順を工夫した.本ルーチンは,2000～3000シンボル程度の相当大きなP文であっても,数百キロバイト程度のメモリで,数分程度で真偽を判定できる. |
| 抄録(英) | In this paper we present an efficient implementation of a decision procedure for prenex normal form Presburger sentences bounded only by existential quantifiers. Our procedure is based on the Cooper's algorithm. We have implemented the decision algorithm using "recursive calls", so that the length of a given expression does not explode while the iteration of the quantifier elimination. For speed-up of the algorithm, we have adopted an elimination order such that a variable close to the root of the syntax tree of the expression will be deleted first. Our procedure can determine the truth of those sentences within a few minutes even if the length of the sentences is a few thousands symbols. |
| キーワード(和) | プレスブルガー算術 / Cooperのアルゴリズム / 変数消去 / 領域計算量 / 正当性検証 |
| キーワード(英) | Presburger arithmetic / Cooper's Algorithm / quantifier elimination / space complexity / verification |
| 資料番号 | |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1995/7/14(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 全ての変数が存在記号で束縛された冠頭標準形プレスブルガー文の真偽判定プログラム |
| サブタイトル（和） | |
| タイトル（英） | An Implementation of Decision Procedure for Prenex Normal Form Presburger Sentences bounded only by Existential Quantifiers |
| サブタイトル（和） | |
| キーワード(1)（和/英） | プレスブルガー算術 / Presburger arithmetic |
| キーワード(2)（和/英） | Cooperのアルゴリズム / Cooper's Algorithm |
| キーワード(3)（和/英） | 変数消去 / quantifier elimination |
| キーワード(4)（和/英） | 領域計算量 / space complexity |
| キーワード(5)（和/英） | 正当性検証 / verification |
| 第 1 著者 氏名（和/英） | 森岡 澄夫 / Sumio Morioka |
| 第 1 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 東野 輝夫 / Teruo Higashino |
| 第 2 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 第 3 著者 氏名（和/英） | 谷口 健一 / Kenichi Taniguchi |
| 第 3 著者 所属（和/英） | 大阪大学基礎工学部情報工学科 Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University |
| 発表年月日 | 1995/7/14 |
| 資料番号 | |
| 巻番号（vol） | vol.95 |
| 号番号（no） | 144 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |