Presentation 1999/3/5
Speed Up Automated Theroem Proving by Using 2-Literal Lemma
Kenichi Kishino, Koji Iwanuma,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In this paper,we discuss 2-literal lemmaizing on automated theorem proving based on Model Elimination. Lemma is used to avoid recomptations of goals, which is a problem top-down theorem proving basically held. When embedding lemmaizing into theorem provers, unit-lemma is often employed because of it's facility to implement. But,ability to eliminate recomptation of goals which unit-lemma has is limited, and non-unit lemma is needed to eliminate more recomptations of goals. So, we implemented 2-literal lemmaizing into PTTP-based theorem prover which is a limited style of non-unit lemma. We also suggest four kind of methods to use 2-literal lemma and compare them by examinations.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) 2-literal lemma / non-unit lemma / theorem provign / automated deduction / model elimination
Paper # AI98-90
Date of Issue

Conference Information
Committee AI
Conference Date 1999/3/5(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Artificial Intelligence and Knowledge-Based Processing (AI)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Speed Up Automated Theroem Proving by Using 2-Literal Lemma
Sub Title (in English)
Keyword(1) 2-literal lemma
Keyword(2) non-unit lemma
Keyword(3) theorem provign
Keyword(4) automated deduction
Keyword(5) model elimination
1st Author's Name Kenichi Kishino
1st Author's Affiliation Dept. of Computer Science and Media Engineering, Yamanashi University()
2nd Author's Name Koji Iwanuma
2nd Author's Affiliation Dept. of Computer Science and Media Engineering, Yamanashi University
Date 1999/3/5
Paper # AI98-90
Volume (vol) vol.98
Number (no) 635
Page pp.pp.-
#Pages 6
Date of Issue