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