Tauchain Development Update (April 2021)

Lucca has developed an interesting tool that generates logical queries automatically. We use them for testing query containment in TML. He also embarked on a small project comparing three theorem provers (Namely, Z3, Vampire and CVC4) finding out that Z3 outclassed all of them but also compares favourably with TML. We continue to work on the performance improvements for TML but it's currently more comparable with other logical solvers out there. Murisi has worked more on documenting the safe subset of datalog that TML supports implementing additional safety checking and fixing some unsafe code that was generated automatically for the interpreter.