# Research: Programming Theorems, learning about Theorems, and applying Theorems

Wow, that title covered a bunch of stuff.  But I bet Alfred Thompson wishes he had found this system, it is an endless supply of blog article ideas.  So nice of Microsoft Research to finally quit being boring.  Wow, what was up with those years that Microsoft Research was all blah, blah, blah, it must be that new organization RISE, they are doing good stuff now!  Check out the

Kinect, Pez, Z3 and more, that is what I am talking about.  So let’s look at Z3 first, some of the superhero robots will take the helm for one minute, mainly because I bought the access to Xtranormal and have to justify it.  The serious stuff is after the video, and it will be just between the two of us since the management usually doesn’t get past the first paragraph.

You have likely heard the statement: “With faster processors and more memory, computers will begin to design themselves.”  I have heard this since the 70s, and I really wish this was true.  It is true in a certain way, but not the way that makes me rich, and the SMT is one way that you can design software automatically at the word level rather than the bit level.

The ability to move from the bit level to the word level is quite an improvement.

Simply:

• The bit level SAT is or satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.
• Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable.
• To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability.

The SMT-LIB has been set up for this, and the information about this can be found at: http://www.smtlib.org/.  Now humans might be able to easily utilize computers while at the same time computer algorithms grow more efficient.