A-SATCHMORE: SATCHMORE with availability checking |
| |
Authors: | Lifeng He Yuyan Chao Yuka Shimajiri Hirohisa Seki Hidenori Itoh |
| |
Affiliation: | (1) Department of AI and Computer Science, Nagoya Institute of Technology, Gokiso, Showa-ku, 466 Nagoya, Japan;(2) Department of Human Information, Nagoya University, Furouchou, Chikusa-ku, 464-01 Nagoya, Japan |
| |
Abstract: | We present an improvement of SATCHMORE, calledA-SATCHMORE, by incorporating availability checking into relevancy. Because some atoms unavailable to the further computation
are also marked relevant, SATCHMORE suffers from a potential explosion of the search space. Addressing this weakness of SATCHMORE,
we show that an atom does not need to be marked relevant unless it is available to the further computation and no non-Horn
clause needs to be selected unless all its consequent atoms are marked availably relevant, i.e., unless it is totally availably
relevant. In this way,A-SATCHMORE is able to further restrict the ues of non-Horn clauses (therefore to reduce the search space) and makes the proof
more goal-oriented. Our theorem prover,A-SATCHMORE, can be simply implemented in PROLOG based on SATCHMORE. We discuss how to incorporate availability cheeking into
relevancy, describe our improvement and present the implementation. We also prove that our theorem prover is sound and complete,
and provide examples to show the power of our availability approach.
This research is supported in part by the Japanese Ministry of Education and the Artificial Intelligence Research Promotion
Foundation.
Lifeng He, Ph.D: He received the B. E. degree from Northwest Institute of Light Industry, China, in 1982, the M. S. and Ph.D. degrees in
AI and computer science from Nagoya Institute of Technology, Japan, in 1994 and 1997, respectively. He currently works at
the Institute of Open System in Nagoya, Japan. His research interests include automated reasoning, theorem proving, logic
programming, knowledge bases, multi-agent cooperation and modal logic.
Yuyan Chao, M. S.: She received the B. E. degree from Northwest Institute of Light Industry, China, in 1984, and the M. S. degree from Nagoya
University, Japan, in 1997. She is currently a doctoral candidate in the Department of Human Information, Nagoya University.
Her research interests include image processing, graphic understanding, CAD and theorem proving.
Yuka Shimajiri, M. S.: She currently works as a Assistant Professor in Department of Artificial Intelligence and Computer Science at the Nagoya
Institute of Technology. She received her B.Eng. and M.Eng. from the Nagoya Institute of Technology in 1994 and 1996, respectively.
Her current research interests include logic programming and automated deduction. She is a member of IPSJ and JSAI.
Hirohisa Seki, Ph.D.: He received the B. E., M. E. and Ph.D degrees from the University of Tokyo in 1979, 1981 and 1991 respectively. He joined
the Central Research Laboratory of Mitsubishi Electric Corporation in 1981. From 1985 to 1989, he was with the Institute for
New Generation Computer Technology (ICOT). Since 1992, he has been an Associate Professor in the Department of AI and Computer
Science at Nagoya Institute of Technology. His current research interests include logic programming, deductive databases and
automated deduction. He is a member of ACM, IEEE, IPSJ and JSAI.
Hidenori Itoh, Ph.D.: He received the B. S. degree from Fukui University, in 1969, the M. S. degree and Ph.D degree from Nagoya University, Japan,
in 1971 and 1974, respectively. From 1974 to 1985, he worked at Nippon Telephone and Telegraph Laboratories, developing operating
systems. From 1985 to 1989, he was with the Institute for New Generation Computer Technology, developing knowledge base systems.
Since 1989, he has become a professor at the Nagoya Institute of Technology. His current research interests include image
processing, parallel computing, fuzzy logic and knowledge processing. |
| |
Keywords: | Theorem Proving SATCHMO SATCHMORE Relevancy Availability |
本文献已被 SpringerLink 等数据库收录! |
|