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.