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?