verification system because of its unique application -- to verifying
machine design, actually microcode within a computer. A micro-
code verifier was developed at IBM from about 1974 to 1980 by, Wil-
liam Carter, Daniel Brand, William Joyner and George Leeman
[CJ1]. Although (semi)automated verification is under active
investigation for use by some government agencies and contrac-
tors, this use will be limited by the tremendous effort needed to
prepare precise specifications of the process to be verified and
then to bludgeon the proofs from the provers. There is still much
manual work needed to use the semi-automated verifiers.
Program synthesis has been pursued using theorem proving
techniques (e.g., see Manna and Waldinger [MWl] and Bibel [Bi2]),
but this is in a very early stage of development.
We previously mentioned that theorem provers could be the
heart of many artificial intelligence (AI) endeavors such as data
base systems ("question-answerers") and robots.
surprising realization has been thrust on AI researchers, namely,
that a theorem proving system can form the basis of a
AI language. This concept was embodied in the language
Prolog in 1972 by Colmerauer and Roussel ([Ckl], [R03]), which
was used for general problems on natural language processing. At
this time, Prolog was mainly a theorem prover based upon SL-
resolution, with draconian restrictions to shrink the search space.
In fact these restrictions were equivalent to the use of Hom-
clauses, discussed later by Kowalski in [Ko1] and [Ko3]. Kowalski
emphasized the importance of separation of program logic and
control and the value of a subset of logic called Horn clause logic,
and, together with Van Emden, he determined the formal seman-
tics of Prolog-like languages [KVl]. Prolog is now viewed by many
as the most powerful existing language for implementing many
designs of natural language systems, data base systems,