Presentation 1997/11/13
Semantic Model Elimination : Toward Efficient Equality Proving : Extended Abstract
Koji Iwanuma,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In this paper, we study an extension of Loveland's Model Elimination, (ME), called semantic model elimination, which is integrated with a semantic-guide method. This variant is a straightforward but useful extension of restart model elimination, which was proposed by Baumgartner and Furbach. One of the aims of semantic model elimination is an efficient treatment of equality reasoning in a tableau framework. The second is application for an efficient hypothetical reasoning based on a sort of model checking, although this paper does not describe this issue.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) Theorem Proving / model elimination / equality / semantic guide / restart computation
Paper # AI97-24
Date of Issue

Conference Information
Committee AI
Conference Date 1997/11/13(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Vice Chair

Paper Information
Registration To Artificial Intelligence and Knowledge-Based Processing (AI)
Language ENG
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Semantic Model Elimination : Toward Efficient Equality Proving : Extended Abstract
Sub Title (in English)
Keyword(1) Theorem Proving
Keyword(2) model elimination
Keyword(3) equality
Keyword(4) semantic guide
Keyword(5) restart computation
1st Author's Name Koji Iwanuma
1st Author's Affiliation Department of Electrical Engineering and Computer Science Yamanashi University()
Date 1997/11/13
Paper # AI97-24
Volume (vol) vol.97
Number (no) 373
Page pp.pp.-
#Pages 8
Date of Issue