A Theorem Proving System for Logic Design Verification
スポンサーリンク
概要
- 論文の詳細を見る
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.
- 一般社団法人情報処理学会の論文
- 1988-06-30
著者
-
KOBAYASHI YASUHIRO
Energy Research Laboratory, Hitachi Ltd.
-
Yamada Naoyuki
Energy Research Laboratory Hitachi Ltd.
-
KIGUCHI TAKASHI
Energy Research Laboratory, Hitachi Ltd.
-
Kobayashi Yasuhiro
Energy Research Laboratory Hitachi Ltd.
-
Kiguchi Takashi
Energy Research Laboratory Hitachi Ltd.
関連論文
- A Knowledge Compilation Method Through Conversion of Symbolic Rules and Facts into Functions
- Design Verification Based on Theorem-Proving Technique for Sequential Control Circuits with Timing Coordination
- Design Verification of Sequential Control Circuits Based on Theorem-Proving Method
- A Plant Diagnosis Method Based on the Knowledge of System Description
- A Knowledge Acquisition Method Based on a Multi-Attribute Utility Model
- A Theorem Proving System for Logic Design Verification
- A new method of startup planning for boiling water reactors.
- Logic Verification System for Power Plant Sequence Diagrams.
- Sensitivity study of fuel cost in extended burnup BWR core.
- Approach to knowledge based man-machine communication for BWR start-up guidance.
- Simple method to predict power level and core flow rate of boiling water reactors by using one-point core model.