二分決定グラフ(BDD)による多重文脈型真偽維持システムBMTMS

概要

論文の詳細を見る
Enabling Multiple-context type Truth Maintenance Systems such as ATMS and CMS to accept any logical (propositional) formula cannot avoid enumerating prime implicates from the set of logical formula. Since such an enumeration is an NP-complete problem, most systems accept some restricted logical formula to avoid its inefficiency. BDD(Binary Decision Diagram) is an efficient representation of Boolean formula and most its manipulations can be processed quite efficiently. In this paper, we present the BDD-based Multiple-context type Truth Maintenance System (BMTMS). BMTMS provides interfaces of three levels. Two levels are for conventional ATMS and its variants and one is to exploit full capabilities of BMTMS. QPE (Qualitative Physics Engine) is used to compare BMTMS and ATMS. BMTMS is quite efficient compared with CMS, because it processes most TMS operations without enumerating the prime implicates.
社団法人人工知能学会の論文
1996-03-01