Presentation 2003/5/22
On constructing theorem prover based on resolution with Java
Shigeyuki OOGAMl, Hiroshi FUJITA, Ryuzo HASEGAWA,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In order to construct theorem prover based on resolution with Java, we introduce two data structures called FVar/BVar and Termlist methods.Our experience shows that the Termlist method runs faster than the FVar/BVar methods when unifying several terms except deep nested terms. We also implement a tentative theorem prover using both methods. The prover using Termlist can prove almost problems faster than that using FVar/BVar does.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) theorem proving / unification / resolution / Java
Paper # AI2003-6
Date of Issue

Conference Information
Committee AI
Conference Date 2003/5/22(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) On constructing theorem prover based on resolution with Java
Sub Title (in English)
Keyword(1) theorem proving
Keyword(2) unification
Keyword(3) resolution
Keyword(4) Java
1st Author's Name Shigeyuki OOGAMl
1st Author's Affiliation Graduate School of Information Science and Electrical Engineering, Kyushu University()
2nd Author's Name Hiroshi FUJITA
2nd Author's Affiliation Graduate School of Information Science and Electrical Engineering, Kyushu University
3rd Author's Name Ryuzo HASEGAWA
3rd Author's Affiliation Graduate School of Information Science and Electrical Engineering, Kyushu University
Date 2003/5/22
Paper # AI2003-6
Volume (vol) vol.103
Number (no) 103
Page pp.pp.-
#Pages 6
Date of Issue