Presentation 1996/11/2
A Bidirectional Prover for Non-Range Restricted Formulae
Koji Iwanuma, Kazuhiko Oota,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In this paper, we give a theoretical investigation for a bidirectional theorem prover for non-range restricted formulae. We generalize Model Generation method which is adopted by SATCHMORE and MGTP, in order to deal with arbitrary first-order clause sets. This extension is achieved by introducing unification mechanism for maintaining model candidates.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) theorem proving / model generation / relevancy / non-range restriction / bidirectional prover / SATCHMORE
Paper # AI96-29
Date of Issue

Conference Information
Committee AI
Conference Date 1996/11/2(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) A Bidirectional Prover for Non-Range Restricted Formulae
Sub Title (in English)
Keyword(1) theorem proving
Keyword(2) model generation
Keyword(3) relevancy
Keyword(4) non-range restriction
Keyword(5) bidirectional prover
Keyword(6) SATCHMORE
1st Author's Name Koji Iwanuma
1st Author's Affiliation Dept. of Electrical Engineering and Computer Science Yamanashi University()
2nd Author's Name Kazuhiko Oota
2nd Author's Affiliation Dept. of Electrical Engineering and Computer Science Yamanashi University
Date 1996/11/2
Paper # AI96-29
Volume (vol) vol.96
Number (no) 346
Page pp.pp.-
#Pages 8
Date of Issue