Learning to Reason
  Automated theorem proving has long been a key task of artificial
intelligence. Proofs form the bedrock of rigorous scientific inquiry. Many
tools for both partially and fully automating their derivations have been
developed over the last half a century. Some examples of state-of-the-art
provers are E (Schulz, 2013), VAMPIRE (Kov\'acs & Voronkov, 2013), and Prover9
(McCune, 2005-2010). Newer theorem provers, such as E, use superposition
calculus in place of more traditional resolution and tableau based methods.
There have also been a number of past attempts to apply machine learning
methods to guiding proof search. Suttner & Ertel proposed a
multilayer-perceptron based method using hand-engineered features as far back
as 1990; Urban et al (2011) apply machine learning to tableau calculus; and
Loos et al (2017) recently proposed a method for guiding the E theorem prover
using deep nerual networks. All of this prior work, however, has one common
limitation: they all rely on the axioms of classical first-order logic. Very
little attention has been paid to automated theorem proving for non-classical
logics. One of the only recent examples is McLaughlin & Pfenning (2008) who
applied the polarized inverse method to intuitionistic propositional logic. The
literature is otherwise mostly silent. This is truly unfortunate, as there are
many reasons to desire non-classical proofs over classical.
Constructive/intuitionistic proofs should be of particular interest to computer
scientists thanks to the well-known Curry-Howard correspondence (Howard, 1980)
which tells us that all terminating programs correspond to a proof in
intuitionistic logic and vice versa. This work explores using Q-learning
(Watkins, 1989) to inform proof search for a specific system called
non-classical logic called Core Logic (Tennant, 2017).
