Interactions between Reinforcement Learning and Mechanical Theorem Proving

The purpose of this research project is to examine possible interactions between the theory and use of reinforcement learning techniques and the theory and use of mechanical theorem proving techniques.

Taken in one direction, this could involve using reinforcement learning to improve the logical steps suggested during mechanical theorem proving, ideally enhancing the class of questions it is able to practically tackle.

In the other direction, one could use theorem proving to formally verify the theories underpinning reinforcement learning and ideally establish useful properties and limitations which might at this stage be unproven but only observed in practice.

It is also possible that some interaction between the two sets of methods could enhance reinforcement learning, possibly by allowing it to "believe" logical properties of its environment and apply logical rules to them, perhaps thus circumventing computational effort and time - these beliefs could be inherited by further reinforcement learning processes where applicable.