- ...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">
- 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
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.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.