【摘要】 tableau方法是一种具有较强的通用性和适用性的推理方法,但由于函数符号、等词等的限制,使得自动推理具有不确定性.针对tableau推理中封闭集合构造过程具有盲目性的问题,提出将强化学习用于tableau自动推理的方法.该方法将tableau推理过程中的逻辑公式与强化学习相结合,产生抽象的状态和活动.这样一方面可以通过学习方法控制自动推理的推理顺序,形成合理的封闭分枝,减少推理的盲目性;另一方面复杂的推理可以利用简单的推理结果,提高推理的效率.更多还原

【Abstract】 The tableau method is a reasoning method with high universality and applicability.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 formulae in tableau reasoning to produce 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,simple reasoning results can be reused in the complex reasoning system to improve reasoning efficiency.更多还原