TREITEL@SUMEX-AIM.ARPA (03/13/84)
From: Richard Treitel <TREITEL@SUMEX-AIM.ARPA>
[Forwarded from the Stanford bboard by Laws@SRI-AI.]
The Automatic Inference Seminar will meet on Wednesday March 14th in MJH 352
(note change of room from 301) at 1:30 p.m.
(This is tax-filing season; I'm getting slightly too many groanworthy remarks
about "automatic deduction", hence the name change).
Speaker: Richard Treitel (oh no, not again)
Subject: Theorem Proving in the Stanford Pascal Verifier
The Stanford Pascal Verifier was developed in the late 1970's for research in
program verification. Its deductive component, designed mainly by Greg Nelson
and Derek Oppen, has some features not found in many other natural deduction
systems, including a powerful method for dealing with equalities, a general
framework for combining the results of decision procedures for fragments of the
problem domain, and a control structure based on an unusual "normal form" for
expressions. I will attempt to explain these and relate them both to other
provers and to post-Oppen work on the same technology.