Imitation Learning for Connection-Tableau Construction

Fredrik Rømming, Mantas Bakšys, Martin S. Fixman +1

An automated theorem prover builds a proof step by step, choosing at each point what to add and what to remove. We cast this construction as a policy acting in a transition system…