HTTPS SSH
MATHEMAGICIAN

 * What is it?

   Mathemagician is two things: a formal mathematical language and an automated theorem prover which
   uses this language.

 * What can the language do?

   The language specification allows for full expression of the entirety of formal mathematics. That
   means you can write out axioms, definitions, and theorems, as well as schema of the same. But
   more than traditional mathematics, it can express logical systems built on axiomatizations other
   than the standard first-order logic + ZFC.

 * What can the theorem prover do?

   In theory, if a theorem is provable in a given system, the prover will be able to find a proof,
   given enough time and memory. In practice, the prover works much better on small problems that
   can be solved concisely from known axioms, definitions and theorems due to the immensely large
   space of logical inferences. Accelerating this process with optimizations and heuristics is an
   area of active development.


BUILDING

 * Dependencies:

   - SDL 2                  On Ubuntu this comes in libsdl2-dev.

 * Simply use 'make <target>'. The important targets are:

   - all, release           Builds an object file for every major class
   - unity                  Builds the entire system at once into one object file
   - test                   Builds the test executable and links it to unity.o
   - debug unity_d test_d   Debug versions of the above
   - everything             All of the above


TODO

 * Test and use tight expressions.
 * Use raw arrays in Expression and Permutation so tight expressions can include this memory.
 * Add custom memory allocation.
 * Store tight expressions using in-order traversal to maintain locality
 * Hopscotch hash table instead of cuckoo?