Seeking Reading Recommendation on Implementing Theorem Provers

What a coincidence, I'm currently in a process of developing an inference engine that in its final version may relatively simply define Hilbert calculus (among other things), while Hilbert calculus can be used to form deductive systems you are interested in. Hilbert calculus competes with natural deduction system and sequent calculus, both of which also (I believe) may be defined in the inference engine I'm developing.

The engine is based only on implications and contexts of inference, but it is still a bit awkward to use it since different contexts are not yet hierarchically related (this update is on my to-do list). What is interesting with the engine is that its prototype implementation fits in only about 140 Javascript LOC, and I'm trying to keep the final version near this number. You can test and read about the prototype on the above GitHub link.

/r/ProgrammingLanguages Thread