WEKO3
アイテム
A Theorem Proving System for Logic Design Verification
https://ipsj.ixsq.nii.ac.jp/records/59804
https://ipsj.ixsq.nii.ac.jp/records/59804c0f5d03a-eef9-4711-b5fa-1d7f86c6be84
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JIP1102002.pdf (1.5 MB)
|
Copyright (c) 1988 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | JInfP(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1988-06-30 | |||||||
| タイトル | ||||||||
| タイトル | A Theorem Proving System for Logic Design Verification | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Theorem Proving System for Logic Design Verification | |||||||
| 言語 | ||||||||
| 言語 | eng | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| Energy Research Laboratory Hitachi Ltd. | ||||||||
| 著者所属 | ||||||||
| Energy Research Laboratory Hitachi Ltd. | ||||||||
| 著者所属 | ||||||||
| Energy Research Laboratory Hitachi Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Energy Research Laboratory, Hitachi Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Energy Research Laboratory, Hitachi Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Energy Research Laboratory, Hitachi Ltd. | ||||||||
| 著者名 |
Naoyuki, Yamada
× Naoyuki, Yamada
|
|||||||
| 著者名(英) |
Naoyuki, Yamada
× Naoyuki, Yamada
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | This paper describes a logic design verification system based on a heuristically guided theorem proving method. The system called HTPS consists of three main programs; meta-level program base-level program and control program. In the meta-level program domain specific knowledge expressed in the form of a rule is used to generate guidance for the proof procedure. According to this guidance proof is performed in the base-level program. The control program regulates these procedures. In order to facilitate this hierarchical inference mechanism a connection graph method is adopted as the proof strategy in the base-level program. HTPS was successfully applied to verification of logic circuits and its effectiveness and usefulness were clearly demonstrated. | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | This paper describes a logic design verification system based on a heuristically guided theorem proving method. The system called HTPS consists of three main programs; meta-level program, base-level program and control program. In the meta-level program, domain specific knowledge expressed in the form of a rule is used to generate guidance for the proof procedure. According to this guidance, proof is performed in the base-level program. The control program regulates these procedures. In order to facilitate this hierarchical inference mechanism, a connection graph method is adopted as the proof strategy in the base-level program. HTPS was successfully applied to verification of logic circuits and its effectiveness and usefulness were clearly demonstrated. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA00700121 | |||||||
| 書誌情報 |
Journal of Information Processing 巻 11, 号 2, p. 92-104, 発行日 1988-06-30 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-6652 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
