Introduction of Heuristics, Databases and a Website

This version of the release adds three main things: (i) more sophisticated search strategies involving simple heuristics, (ii) a SQLite database tracking lots of proof data, like tracking proven and unproven theorems, and (iii) a basic website frontend.

This version is lacking: (i) a good scheduling system which ensures user-submitted tasks are completed on time (at the moment the scheduler just selects things to do arbitrarily), (ii) neither has sophisticated heuristics, nor a sophisticated automatic conjecturer - the existing one seems to have trouble, (iii) any further types of logic.

Alpha

v0.2

Fixed another bug with `FreeVarMap`.

Alpha

This first version of the ATP is absolutely minimal, but is sufficient to prove statements. It includes:

• A rudimentary equational logic implementation
• A naive uninformed search strategy (iterative deepening search)
• A simple command line application for finding proofs

A lot of other work has been done on writing statement parsers etc.

As of yet, this version is quite inefficient, so the next main tasks are to optimise the logic code, and then implement some database functionality so we can load and save statements to help prove other statements.