Lecture Notes in Computer Science, 2007, Volume 4683/2007, 262-270, DOI: 10.1007/978-3-540-74581-5_28

An Tableau Automated Theorem Proving Method Using Logical Reinforcement Learning

Quan Liu, Yang Gao, ZhiMing Cui, WangShu Yao and ZhongWen Chen

View Related Documents

Abstract

Logical reinforcement learning (LORRL) is presented with the combination of reinforcement learning and logic programming. Tableau method based on logic reinforcement learning is provided according to the real problem of tableau automated theorem proving method that need to extend for different logic formulae and it will influence the automated theorem proving efficiency. This method takes the combination of logic formulae and expansion result as abstract state, expansion rules as actions, node closes as the aim and receives a reward. On the one hand the method is suitable for a lot of types of tableau automated theorem proving and the blindness of reasoning is reduced. On the other hand simple automated theorem proving result can be used in complicated automated theorem proving and efficiency is raised.

Keywords  logical reinforcement learning - tableau automated theorem proving - LOMDP

Fulltext Preview

Image of the first page of the fulltext document