LENAT@SU-SCORE.ARPA (11/02/83)
From: Doug Lenat <LENAT@SU-SCORE.ARPA>
[Reprinted from the SU-SCORE bboard.]
CS Colloquium, Tuesday, November 1, 4:15pm Terman Auditorium
(refreshments at 3:45 at the 3rd floor lounge of MJH)
SPEAKER: Dr. Jussi Ketonen, Stanford University CS Department
TITLE: A VIEW OF THEOREM-PROVING
I'll be discussing the possibility of developing powerful
expert systems for mathematical reasoning - a domain characterized by
highly abbreviated symbolic manipulations whose logical complexity
tends to be rather low. Of particular interest will be the proper
role of meta theory, high-order logic, logical decision procedures,
and rewriting. I will argue for a different, though equally
important, role for the widely misunderstood notion of meta theory.
Most of the discussion takes place in the context of EKL, an
interactive theorem-proving system under development at Stanford. It
has been used to prove facts about Lisp programs and combinatorial
set theory.
I'll describe some of the features of the language of EKL,
the underlying rewriting system, and the algorithms used for
high-order unification with some examples.