Can Tau achieve a second order logic solver in 2020?
I'm still reviewing what Ohad said in the latest video but in the latest video there was a lot of emphasis on Boolean equations. This particular topic is quite esoteric and is based on "Boolean algebra" which I admittedly at this time do not know a lot about. Ohad in the video mentions several quite novel solution paths to getting a second order logic solver which is a crucial step to take to get us to the software synthesis promised for the beta.
Data can be represented as Boolean equations. The resolution method mentioned is a technique for theorem proving but is an example of one of the esoteric categories of knowledge which I myself know little about. That being said the ideal situation is for a second order logic solver to be achieved before the end of 2020. I hope by the update for next month we can see a clear example implementation of what is being discussed so that we can see from demonstration of the code whether or not this will be achieved.
Thanks for the update. Appreciate the shortness.
On one hand I am fascinated by TAU, on the other it is getting increasingly the smell of a sect, with Ohad being the guru.