Greetings once again from PLANETQUANTUM.COM. Below are a couple screen shots of my "early stage" Quantum Theorem Prover:

And

While nothing much of importance is going on here (yet), this is an existence proof that the Quantum Theorem Prover exists. I'd like to say that I owe a great debt of gratitude to the following book:

• Boyer, Robert S. and Moore, J. Strother (1979), A Computational Logic, Academic Press, Inc., New York.

Currently, I'm concentrating attention on a few items:

• Improved Mixed Integer Linear Programming (MILP) decision procedure (maybe I should say "MILP+" where "+" means "a little more")
• Multivariate Chinese Remainder Theorem
• Application of Hopcroft and Ullman's Theorem 2.4 to termination proofs of mutually recursive functions ("Theorem 2.4  If L is accepted by a DFA, then L is denoted by a regular expression")
• "Programming by Contract" (aka "Design by Contract"™) as exhibited by, for example, the programming language Eiffel