Project 4: Implementing M* in Turing's World

The challenge -- perhaps the greatest challenge ever undertaken by designers of machines in Turing's World -- is to design, and them implement in Turing's World, a Turing Machine which constitutes a positive test for unsatisfiability of formulas in first-order logic. This machine is referred to as M* on page 142 of Computability and Logic, by Boolos and Jeffrey.

For a look at the algorithm-sketch of M*:

Selmer Bringsjord

Due April 25.