...comment.
1999 note: The ideas of Prolog are similar to a subset of the ideas of Microplanner. However, Prolog was designed systematically and has survived, while Microplanner didn't. The key permanent idea of Prolog is that a certain subset of logic (Horn clauses) are executable as programs doing backtracking search. It seems to me that this discovery has as much permanent importance as the ideas behind Lisp.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...powerful.
1999: Only the part about standardization happened.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...forthcoming)
1999: The 1981 ideas have been combined with other ideas, e.g. about speech acts, and elaborated. See [McC96]. The Elephant idea referred to was to avoid data structures by allowing direct reference to the past.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...1980).
1999: That textbook didn't appear, mainly because of a difference of opinion among the authors about the most appropriate proof formalism
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...compiler.
1999: FOL was succeeded in the Lisp course by Jussi Ketonen's EKL prover, but the proposed integrated system hasn't happened.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...HREF="footnode.html#60">gif
1999: NQTHM (aka the Boyer-Moore prover) was used by Shankar when he taught the course. This prover is designed to use induction to prove properties of total Lisp functions. Using the Eval function of the logic and the representation of function definitions as Sexpressions properties of partial functions can also be proved. NQTHM has evolved into ACL2 which supports a large applicative subset of Common Lisp and is programmed almost entirely within that subset. [see http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html]
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...programs.
1999: Ian Mason's thesis[Mas86] gave some principles for reasoning about first-order Lisp including rplacx.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...computations.
1999: Maybe this is still the case.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...informally.
1999: A logic for reasoning about Lisp-Scheme-ML like programs with functions and mutable data structures has been developed by Mason and Talcott [HMST95]. This logic has a relatively complete axiomatization of primitives for mutable data as well as a variety of induction principles and methods for proving properties of programs.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...se).
1999: An example is Maude [Gro99, CDE tex2html_wrap_inline188 98], a language based on Rewriting Logic. In Maude, actions and effects are expressed in a declarative manner, and using the reflective capability, Maude programs and computations can be represented, reasoned about, modified and executed in Maude.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...1962.
1999: I thank Carolyn Talcott for additonal references.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

John McCarthy
Mon Mar 22 17:10:06 PST 1999