[1]L IU Quan,CU I Zhi-ming,et al.Tableau reason ing method based on logical re inforcement learn ing[J].CAAI Transactions on Intelligent Systems,2008,3(4):355-360.
Copy

Tableau reason ing method based on logical re inforcement learn ing

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 3 Number of periods: 2008 4 Page number: 355-360 Column: 学术论文—机器学习 Public date: 2008-08-25
Title:
Tableau reason ing method based on logical re inforcement learn ing
Author(s):
L IU Quan1;  2 ;  CU I Zhi-ming2 ;  GAO Yang1 ;  CHEN Dao-xu1 ;  YAO Wang-shu2
1. School of Cumputer Science of Technology, Soochow University, Suzhou 215006, China;
2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China
Keywords:
logical reinforcement learning;  tableau reasoning
CLC:
TP301
DOI:
-
Abstract:
The tableau method is a reasoning method with high universality and app licability. However, given the restrictions of function symbols and equations, there remains a great deal of uncertainty in automated reasoning. In order to remove blind reasoning in the construction of a closed set for tableau reasoning, a method was developed to introduce reinforcement learning into tableau reasoning. Reinforcement learning was combined with the logical for2 mulae in tableau reasoning to p roduce abstract states and actions. On the one hand, reasoning sequences in auto reasoning can be controlled by the learning method to form reasonable closed branches and reduce the blindness of reasoning. On the other hand, simp le reasoning results can be reused in the comp lex reasoning system to imp rove reasoning efficiency.
References:
[ 1 ]史忠植,董明楷,蒋运承,张海俊. 语义Web的逻辑基础 [ J ]. 中国科学(E辑) , 2004, 34 (10) : 112321138.
SH I Zhongzhi, DONGMingkai, J IANG Yuncheng, ZHANG Haijun. A logic foundation for the semantic web [ J ]. Sci2 ence in China ( Series E) , 2004, 34 (10) : 1123 - 1138.
[ 2 ]BLACKBURN P, BOS J. Rep resentation and inference for natural language [ C ] / / CSL I Publications, Crysmann, Berthold, 2005.
[ 3 ]BERTOSS L, SCHW IND C. Analytic tableaux and database repairs [ C ] / /Foundations of Information and Knowledge Systems. Sp ringer LNCS 2284, 2003.
[ 4 ]苏开乐,骆翔宇,吕关锋. 符号化模型检测CTL [ J ]. 计算机学报, 2005, 28 (11) : 179821806.
SU Kaile, LUO Xiangyu, LU¨Guanfeng. Symbolic model checking for CTL [ J ]. Chinese Journal of Computer, 2005, 28 (11) : 179821806.
[ 5 ] PASKEV ICH A. Connection tableauxwith lazy paramodula2 tion[C ] / / IJCAR 2006. Seattle, USA, 2005.
[ 6 ]HORV ITZ E. Machine learning, reasoning, and intelligence in daily life: directions and challenges[C ] / /Proceedings of ICML. Bled, Slovenia, 1999.
[ 7 ]BRYANT C, MUGGLETON S, OL IVER S. Combining in2 ductive logic p rogramming, active learning and robotics to discover the function of genes [ J ]. Electronic Transactions in Artificial Intelligence, 2001, 6 (12) : 1236.
?[ 8 ]CALZONE L, CHABR IER N, FAGES F. Machine learning biomolecular interactions from temporal logic p roperties [C ] / /Proceedings of CMSB 2005. Edinburgh, Scotland, 2005.
[ 9 ] TEEVAN J , HORV ITZ E. Personalizing search via automa2 ted analysis of interests and activities [ C ] / /Proceedings of SIGIR. Salvador, Brazil, 2005: 4492456.
[ 10 ] F ITTINGM. First2order logic and automated theorem p ro2 ving[M ]. New York: Sp ringer2Verlag, 1996.
[ 11 ]高　阳,陈世福,陆　鑫. 强化学习综述[ J ]. 自动化学报, 2004, 30 (1) : 862100.
GAO Yang, CHEN Shifu, LU Xin. Research on reinforce2 ment learning technology: a review [ J ]. Acta Automatica Sinica, 2004, 30 (1) : 862100.
?[ 12 ]OTTERLO M. Reinforcement learning for relationalMDPs [C ] / / Machine Learning Conference of Belgium and the Netherlands (BeNeLearn’04). [ S. l. ] , 2004: 1382145.
?[13 ]刘　全,孙吉贵. 基于Tableau的定理机器证明系统Tab2 leauTAP[J ]. 计算机工程, 2006, 32 (7) : 38245.
?L IU Quan, SUN J igui. Theorem proving system based on Tab2 leauTAP[J ]. Computer Engineering, 2006, 32 (7) : 38 - 45.
Similar References:

Memo

-

Last Update: 2009-05-18

Copyright © CAAI Transactions on Intelligent Systems