LAWS@SRI-AI.ARPA (08/06/85)
From: AIList Moderator Kenneth Laws <AIList-REQUEST@SRI-AI>
AIList Digest Sunday, 28 Jul 1985 Volume 3 : Issue 99
Today's Topics:
Query - Theorem Proving and Program Verification,
AI Tools - ITP & LMI Prolog,
Applications - Space Planning and Architecture,
Literature - Computational Intelligence & AI Report Vol. 2 No. 6 &
Byte AI Special Issue
----------------------------------------------------------------------
Date: Wed, 24 Jul 85 14:00:35 pdt
From: Jim Fehrle <hpda!hpindla!jef%hplabs.csnet@csnet-relay.arpa>
Subject: Theorem Proving and Program Verification
I'm looking for information on using theorem proving techniques to
prove assertions about programs, such as (for example):
o Data structure X is not modified unless the variable LOCK is true.
o The memory allocated by procedure X is always released before X
terminates.
o The variable POINTER always points to a data element of type T.
Any references to books or articles on this subject would be appreciated.
Jim Fehrle
Hewlett Packard
{ucbvax, hplabs, ihnp4!hpfcla} !hpda!jef
------------------------------
Date: 26 July 85 22:26-EDT
Date: 26 July 85 22:26-EDT
From: BYKAT%UTCVM.BITNET@Berkeley
Subject: Re: ITP, how to order it
Just to add a little to Tom Scott's note in AIList Digest V3 #98 (7/20/85):
Page 177 of the "Automated Reasoning" (Wos et al., 1984) states:
"Both LMA and ITP are in the public domain."
Yet, as Tom Scott points out, the Argonne National Lab charges $1050,
educational institution or not! (Rather a lot to cover distribution costs.)
Alex Bykat
------------------------------
Date: Fri, 26 Jul 85 21:25:06 EDT
From: George J. Carrette <GJC@MIT-MC.ARPA>
Subject: Info about Prolog for LMI-LAMBDA and 36xx
LM-Prolog is a LispMachine implementation of prolog that has been in
commercial and university distribution for both the LMI-LAMBDA and
Symbolics 36xx for over a year. The emphasis in the implementation is
on richness, maturity in datastructures (i.e. not just expressions or
lists but array's, multiple processes and other lispmachine
capabilities), the logically consistent implementation of NOT, the
error checking and handling capabilities such as occurs check and
circularity handling and performance in its database indexing and
ASSUME/RETRACT mechanism. The LMI-LAMBDA version includes a special
microcode-load. Both versions are distributed in SOURCE FORM and
require no additional hardware. The 36xx version is available for
release 5 or 6, and the LMI-LAMBDA version for release 1 or 2.
A brilliant hacker could possible port LM-PROLOG to an enviroment
such as VAX-NIL where he had sufficient lispmachine compatibility
and hooks into the compiler and kernel.
-gjc
------------------------------
Date: Fri, 26 Jul 85 09:33 EDT
From: Seth Steinberg <sas@BBN-VAX.ARPA>
Subject: Re: Space Planning
I used to work for the old Architecture Machine Group at MIT and saw a
number of programming efforts which emulated or assisted architects and
urban planners. How the human mind deals with spatial reasoning is
still a mystery but architects are given specific training in how to
deal with architectural problems. This body of knowledge is the study
of design methodology. The department head, who was from Eindhoven, was
noted for developing the SAR design methodology which involved the use
of architectural grammars. One graduate student did his thesis
on the grammar of Mediterranean hill towns while another parsed the
layout of furniture in an apartment building full of cooperating
retired people.
The SAR method looked rather theoretical to me but it was very popular
in Holland and Latin American countries with left wing governments
(read "democracies"). They encouraged user involvement in the planning
process and would actually teach factory workers how to deal with
"basic variants" at their afterwork planning sessions.
A visit to a good architecture library (e.g. Roche at MIT) should turn
up a fair bit on this subject. Obviously, architects deviate from any
particular methodology, but the guidelines are often useful to help get
started.
Actually, doing architecture is a lot like doing programming from what
I have seen. Back when Babbage was trying to raise funds there were
architects charretting (pulling all nighters). Architectural problems
and programming problems have no one right answer or right approach.
Architects tend to approach a problem vaguely until they develop an
appropriate "vocabulary" (sets of subunits, useful relationships, ...)
for dealing with the problem before they start any serious drawing just
as most programmers tend to program "middle out". Most architects are
doing detail work for office remodelling jobs just as most programmers
are updating huge Cobol programs to take the new tax laws into account.
Finally, architects, like programmers often get carried away with the
elegance of a solution and implement a bathroom with no closet space to
store an extra roll of toilet paper. (I will mention no particular
piece of software here).
Seth Steinberg
SAS @ BBN-VAX
------------------------------
Date: Mon 22 Jul 85 11:50:40-PDT
From: C.S./Math Library <LIBRARY@SU-SCORE.ARPA>
Subject: COMPUTATIONAL INTELLIGENCE--New Journal Received
[Forwarded from the Stanford bboard by Laws@SRI-AI.]
We have received number one of volume one, February 1985 of Computational
Intelligence/Intelligence Informatique. [...]
The following articles are in the first issue of this new
quarterly journal:
Plan parsing for intended response recognition in discourse by Candace Sidner
On the adequacy of predicate circumscription for closed-world reasoning by
Etherington, Mercer and Reiter.
Knowledge organization and its role in representation and interpretation for
time-varying data: the ALVEN system by John Tsotsos
Recovering from execution errors in SIPE by David Wilkins.
-- Mathematical and Computer Sciences Library. H. Llull.
------------------------------
Date: 20 Jul 1985 21:20-EST
From: leff%smu.csnet@csnet-relay.arpa
Subject: AI Report Volume 2 No. 6
o - Discussion of Darpa's strategic computing program
driverless vehicle
gallium arsenide work
MOS implementation service
parallel architectures
naval battle management
Lisp Machine on a chip (TI)
speech recognition
dataflow
wafer scale integration
benchmarking lisp machines
o - DOD Optical computer effort
nine million dollars will be allocated over three years to develop
compact optical computer
o - military expert systems
Titan systems is developing Knowledge-Based engineering System
which is optimized for expert systems related to military command and
control (it has been translated from LISP into C).
Also, they are developing a system called a "space tree" to
determine how goals are met by decisions, allocations or maneuvers.
System to select path of travel based on maps
Air/land battle simulator
o - The French Scene
Laboratoires de Marcoussis (research labs for French corporation
Compagnie Generale d'Electricite)
o - expert systems
process control
diagnosis
computer aided design
scheduling in flexible manufacturing schedules
o - natural language
system to teach UNIX
data base query
o - language development
FROG (integrates LISP and prolog), LISP, PROLOG, common lisp
o - machine optimized for both lisp and prolog
o - speech recognition
system to recognize 35 words with 98 per cent accuracy
o - Carnegie Group has changed the name of SRL+ to Knowledge Prolog
o - Artificial Intelligence Corporation is dropping plans to develop
a microcomputer version of INtellect, its natural language data
base query facility
Microrim has lowered the price of its system CLOUT to $2 50.00
o - Turing Institute has been formed in Scotland
o - review of Texas Instruments activities
o - Arthur D. Little predicts in year 20000, AI market will be 50 to
120 billion dollars [That's quite a crystal ball! -- KIL]
o - The Aeronautical and Electronic Council of Japan has recommended
that Japan look at "the Sixth Generation Computer" which would have
computers similar to the human brain!
o - fifty Japanese companies are forming a research association to look
into AI applicatons to manufacturing
o - article on Lotus activities in AI
review of:
%A William B. Gevarter
%T Intelligent Machines: An Introductory Perspective
%I Prentice-Hall
%C Englewood Cliffs
%J Third Conference on Intelligent Robots and Computer Vision
%C Cambridge, Massachussetts
%D NOV 5-8 1984
%I Society of Photo Optical Instrumentation Engineers
%A Alick Elithorn
%A Ranan Banerji
%T Artificial and Human Intelligence
%I North-Holland
------------------------------
Date: 22 Jul 1985 22:48-EST
From: leff%smu.csnet@csnet-relay.arpa
Subject: Byte AI Special Issue
definition:
D MAG1 BYTE\
%V 10\
%N 4\
%D APR 1985
citations:
%T TI's Arborist, Decision-Tree Analysis Software, Supports IBM
%J MAG1
%P 42
%X Announcement for decision-tree analyst for making decisions.
Cost is $595.00
%T Book Review
%J MAG1
%P 65
%X Reviews of Build Your Own Expert System Chris Naylor
Artificial Intelligence in Basic Mike James
The Cognitive Computer: On Language, Learning, and Artificial Intelligence
by Roger C. Schank and Peter C. Childrs
%A Roger Schank
%A Larry Hunter
%T The Quest to Understand Thinking
%J MAG1
%P 143
%K scripts natural language conceptual dependency
%X discusses natural language reading including the famous restaurant
script. Also discusses models of memory and "What is AI?"
%A John R. Anderson
%A Brian J. Reiser
%T The Lisp Tutor
%J MAG1
%P 159-175
%X discusses a tutor for people learning lisp. Uses the Goal-Restricted
Production System with 325 production rules. It is effective in
diagnosing between 45 and 80 percent of the student's errors.
They compared private human tutoring, the computer program and self-taught
methods. They compared at 11.4, 15 hours and 26.5 hours to get through
six lessons.
%A W. Lewis Johnson
%A Elliot Soloway
%T Proust
%J MAG1
%P 179-190
%K Pascal tutor frame debug T lisp
%X Describes a system for asisting beginners with debugging Pascal
programs. It is 15000 lines of T. In a set of 206 student solutions
to a small problem, PROUST understood completely 79 percent of the programs
and identified 94 percent of the bugs.
%A Michael F. Deering
%T Architectures for AI
%J MAG1
%P 193-206
%K FAIM1 lisp machine Zetalisp Franz lisp PSL hardware unification
machine vision
%X A machine coded unifier is two orders of magnitude faster than the LISP-
coded unifier.
Time for the aggregate function foo on six different processors (all times
in microseconds)
Machine Zetalisp Franz Lisp PSL
VAX 53.8 13.9 5.6
68000 65.2 43.6 5.8
68010 68.6 43.6 10.6
68020 16.1 19.9 3.1
MIT CADR 19.0
3600 6.4
It has been found that by adding features to emulate bit-field dispatch
instructions and stripping off tag bits to conventional micros, they
would be much faster for type-checking LISPS.
Parallel machines sharing a large common memory is bad because there
is not enough memory bandwidth to go around.
%A Patrick H. Winston
%T The Lisp Revolution
%J MAG1
%P 209-218
%X lisp tutorial
%A Carl Hewitt
%T The Challenge of Open Systems
%J MAG1
%P 223-242
%K parallel AI computation logic programming due process reasoning
%A Dana H. Ballard
%A Christopher M. Brown
%T Vision
%J MAG1
%P 245-261
%K MOSAIC Hough transform
%X work done by Larry Roberts on block world vision; optical flow,
vision and the abstraction hierarchy
MOSAIC that uses stereo to understand pictures of buildings,
the challenges of animal vision, Hough transformation
%A Geoffrey E. Hinton
%T Learning in Parallel Networks
%J MAG1
%P 265-273
%K Hopfield nets
%X networks that minimize their energy probablistic nets
%A Jerome A. Feldman
%T Connections
%J MAG1
%P 277-284
%K Necker cube semantic nets connectionist natural language
%A John K. Stevens
%T Reverse Egnineering the Brain
%J MAG1
%P 286-299
%X describes various neural circuit analogies with a few words about
adapting the brains circuitry for use in computers
%A Robert H. Michaelsen
%A Donald Michie
%A Albert Boulanger
%T The Technology of Expert Systems
%J MAG1
%P 303-312
%K tax advice
%X describes the basic concepts of expert systems in terms of a tax advice
system. Goes over some of the famous expert systems and expert system
shells. Also discusses the basic concepts of forward and backward chaining,
networks and frames
%A Beverly A. Thompson
%A William A. Thompson
%T Inside an Expert Systems
%J MAG1
%P 315-330
%K plant identification Pascal
%X describes the outline of a small expert system for plant identification
which could be written in Pascal
%T Artificial Intelligence at Home
%J MAG1
%P 445
%K Dynamic Master Systems TOPSI OPS-5
%X announcement for TOPSI, an OPS5 in.terpreter for Z80 based systems
%A Bruce D'Ambrosio
%T Insight - A Knowledge System
%J MAG1
%P 345-347
%X This is a 95 dollar system offering a backward-chaining inference
engine with confidence values for the IBM-PC. It is compiler based
and will handle up to 4000 rules. It does lack various debugging
facilities such as a display of the currently active rule chains.
%A William M. Raike
%T The Fifth Generation in Japan
%J MAG1
%P 401-406
%K Kazuhiro Fuchi ICOT MITI prolog ESP KL0 PSI S-810
%X discusses choice of kernel language for fifth generation effort;
decision as to whether research should be open or closed and their
supercomputers; apparently they do not know about advanced software
development tools like RATFOR and are doing their work in Fortran.
They have no optimizing FORTRAN for their supercomputer. If they
do not tweak existing code it runs no faster on the supercomputer than
on the conventional machine.
------------------------------
End of AIList Digest
********************