Art

J-GLOBAL ID：200902276670074460   Reference number：04A0386444

Specification of Sub-Herbrand Universes and Its Application to Model Generation Theorem Proving

サブエルブラン領域の特定およびモデル生成定理証明への応用

Author (6)： HE L (愛知県大 情報科学) ,  CHAO Y (名古屋産大 環境情報ビジネス) ,  KAWANA NORIMITSU (名古屋工大) ,  KATO SHOHEI (名古屋工大) ,  NAKAMURA TSUYOSHI (名古屋工大) ,  ITO HIDENORI (名古屋工大)
Material： 情報処理学会論文誌  (IPSJ Journal)
Volume： 45  Issue： 5  Page： 1335-1344  Publication year： May. 15, 2004 
JST Material Number： Z0778A  ISSN： 0387-5806  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *theorem proving ,...
Semi thesaurus term： Herbrand universe ,...

   To see more with JDream III (charged).   {{ this.onShowAbsJLink("http://jdream3.com/lp/jglobal/index.html?docNo=04A0386444&from=J-GLOBAL&jstjournalNo=Z0778A") }}

JST classification (2)： Theory of computation  (JB02000A) ,  Logic algebra  (JB03000H)

Reference (13)：

• 有川節夫. 述語論理と論理プログランミング. 1990
• BAUMGARTNER, P. Hyper Tableaux. Proc. European Workshop : Logics in Artificial Intelligence, JELIA, 1986. 1986, 1-17
• BRY, F. Positive Unit Hyper-resolution Tableaux and Their Application to Minimal Model Generation. J. of Automated Reasoning. 2000, 25, 35-82
• CHANG, C. L. Symbolic Logic and Mechanical Theorem Proving. 1973
• FUJITA, H. A Model Generation Theorem Prover in KL1 Using a Ramified-Stack Algorithm. Logic Programming : Proc. 8th International Conference, Paris, France, 1991. 1991, 535-548

Terms in the title (4)： サブ ,  モデル生成 ,  定理証明 ,  応用