LAWS@SRI-AI.ARPA (05/13/85)
From: AIList Moderator Kenneth Laws <AIList-REQUEST@SRI-AI>
AIList Digest Sunday, 12 May 1985 Volume 3 : Issue 62
Today's Topics:
Book Review - Logic Programming Bibliography,
Seminars - Proof of the Church-Rosser Theorem (UTexas) &
Mechanical Proofs in Metamathematics (SRI) &
Logic Programming Environments (Penn) &
Qualitative Causal Reasoning (MIT) &
AI in Manufacturing Design (SU),
Conferences - AI and Simulation & Law and Technology
----------------------------------------------------------------------
Date: Fri, 10 May 85 10:31:22 EST
From: Simon MacDonald <munnari!simonmac@seismo.ARPA>
Subject: Book Review - Logic Programming Bibliography
Logic Programming: a Classified Bibliography
by I. Balbin, and K. Lecot.
This exciting area in computer science is growing very
quickly; so quickly in fact, that an overview of its
origins, seminal papers, landmark treatises, pioneering
articles etc., may be forgotten, or difficult to identify
and obtain.
Now, the authors of this comprehensive bibliography of well
over 1,600 entries have brought it all together, classed the
type of each paper or monograph into one of 18 broad
categories. This is somewhat arbitrary, but very useful for
those wishing to cover a specific sub-topic. If the item
covers more than one category, it is entered in each
relevant section.
The bibliography is more than twice the size of the one
which appeared in Journal of Logic Programming, and is very
recent. It also has an author index, and subject index.
Approx. 330 pages, softcovers,laminated, burstbound.
Release date July 15, 1985. Prepublication price of A$17.95
[Australian] is valid only until June 30th, 1985.
Publisher: WILDGRASS BOOKS, 289A Smith Street, Fitzroy,
Victoria, 3065, AUSTRALIA. U.S. Distributor: Publishing
House, 210 Broad Street, Washington, NJ, 07882.
------------------------------
Date: Wed, 8 May 85 22:58:07 cdt
From: briggs@ut-sally.ARPA (Ted Briggs)
Subject: Seminar - Proof of the Church-Rosser Theorem (UTexas)
A MECHANICAL PROOF OF THE CHURCH-ROSSER THEOREM
by
N. Shankar
1 PM Friday May 10
PAI 5.60
The talk outlines a formalization and proof of the
Church-Rosser theorem that was carried out with the Boyer-Moore
theorem prover. This celebrated theorem on the Lambda Calculus
lacked a widely accepted proof for over thirty years. The
mechanical proof is based on the one due to Tait and Martin-Lof.
The proof illustrates the effective use of the Boyer-Moore
theorem prover in checking difficult metamathematical proofs.
The above proof effort led to a much clearer understanding of the
proof and brought certain representational issues to light. No
familiarity with the Boyer-Moore theorem prover or Lambda
Calculus will be assumed.
------------------------------
Date: Fri 10 May 85 17:08:40-PDT
From: WALDINGER@SRI-AI.ARPA
Subject: Seminar - Mechanical Proofs in Metamathematics (SRI)
Wednesday, May 15, 4:15, in EJ232, SRI International
This is different from Shankar's talk at Stanford.
MECHANICAL PROOFS IN METAMATHEMATICS
N. Shankar
University of Texas at Austin
Austin, Texas
Metamathematics is a source of many interesting theorems and difficult
proofs. Among these are theorems which express the soundness of
derived inference rules. The talk will describe a formalization of
first-order logic within the Boyer-Moore logic and discuss some
well-known derived inference rules that were proved to be sound using
the Boyer-Moore theorem prover. The most important of these is the
tautology theorem which states that every tautology has a proof. The
proof of the tautology theorem will be discussed in some detail. Such
proofs demonstrate a feasible way to construct sound, efficient, and
extensible proof-checking programs. No familiarity with automated
theorem-proving will be assumed.
Visitors from outside SRI should come to the Engineering building
reception, on Ravenswood Avenue opposite Pine street.
------------------------------
Date: Fri, 10 May 85 13:50 EDT
From: Tim Finin <Tim%upenn.csnet@csnet-relay.arpa>
Subject: Seminar - Logic Programming Environments (Penn)
A MODEL AND AN IMPLEMENTATION OF A LOGIC PROGRAMMING ENVIRONMENT
Henryk Jan Komorowski (Harvard)
10:30 May 17; room TBA, Moore School, Univ. of Pennsylvania
It has been claimed that logic programming offers out-
standing possibilities for new concepts in programming
environments. But with the exceptions of the pioneering
work of Shapiro on algorithmic debugging, Pereira's rational
debugging and early work on expert systems from Imperial
College, there has been little progress reported in the
field of logic programming environments. This summary
describes our current work on a generic software engineering
shell for logic programming. We use reflection and the
amalgamation of meta-level language with the object level to
express and support the INCREMENTAL character of
specifying/programming. An important facet of the shell is
that we formalize some aspects of programming methodology
and provide heuristics for avoiding errors. These heuristics
formalize what experienced programmers may already know.
The shell bears similarities to an expert system since
it has explanation mechanisms and provides programming-
knowledge acquisition. Currently, it supports single user
Prolog programming and runs in C-Prolog. The shell is gen-
eric in that it provides support for activities ranging from
artificial intelligence programming to formal specification
development.
This is a joint work with Shigeo Omori.
------------------------------
Date: 10 May 1985 22:15 EDT (Fri)
From: "Daniel S. Weld" <WELD%MIT-OZ@MIT-MC.ARPA>
Subject: Seminar - Qualitative Causal Reasoning (MIT)
[Forwarded from the MIT bboard by SASW@MIT-MC.]
AI Revolving Seminar Tues 5/14/85 4:00pm 8AI Playroom
Qualitative Causal Reasoning in Diagnosis
Benjamin Kuipers
The classical approach to diagnosis in medical AI programs has been
based on accumulating confidence scores from weighted associations
between findings and diseases. Some of the weaknesses in this
approach can be avoided by incorporating a "causal model" of the
mechanisms involved in the disease. We have developed a causal model
representation based on qualitative simulation of the structures of
physiological mechanisms to yield qualitative predictions of behavior.
The causal model elaborates the diagnostic hypothesis and derives its
evolution through time from its primary causes. We demonstrate QSIM,
an efficient, flexible algorithm for qualitative simulation. QSIM is
a qualitative abstraction of differential equations, which makes it
possible to prove some useful properties. We show some examples of
output from QSIM on significant physiological mechanisms, and we
demonstrate our progress toward integrating hypothesis evocation and
qualitative simulation into a single diagnostic system.
------------------------------
Date: Thu 9 May 85 20:33:57-PDT
From: Elliott Levinthal <LEVINTHAL@SU-SIERRA.ARPA>
Subject: Seminar - AI in Manufacturing Design (SU)
AI in Manufacturing and Design Seminar May l5, l985
2:l5 p.m. Terman 2l7
Speaker: Professor David C. Brown
Worcester Polytechnic Institute
We are investigating the structure and operation of expert systems
for the design of mechanical components by computer. As design
in general is a poorly understood activity we have chosen to limit
ourselves to a particular class of design activity, understand it
thoroughly, and built expert systems that simulate that activity
in a realistic way.
------------------------------
Date: 9 May 1985 19:24-EST
From: leff%smu.csnet@csnet-relay.arpa
Subject: Conference - AI and Simulation
Southwestern Region Simulation Council Spring Technical Meeting
Artificial Intelligence and Simulation
May 16-17 1985
At: University of Houston/Clear Lake
Bayou Building
2700 Bay Area Blvd.
Clear Lake/NASA JSC Area
Houston, Texas
HIghlights: Thursday 11:00
Dr. John Pinkston
Vice President and Chief Scientist
Micro-Electronics, Computer Technology Corp (MCC)
Austin, Texas
PROLOG Tutorial, Friday 9-11:15 AM
Dr. Ralph Huntsinger
Senior Vice PResident, SCS
Professor of Computer Science
California State University, Chico
Cost: $25.00 two days $15.00 one day students: $10.00
------------------------------
Date: 9 May 1985 16:09-EST
From: "George R. Cross" <cross%lsu.csnet@csnet-relay.arpa>
Subject: Conference - Law and Technology
========================================================
Second Annual Conference on Law and Technology
Theme: Legal Language, Computational Linguistics,
and Artificial Intelligence
Organizers:
Dr. Charles Walter, Director
Program on Law and Technology
University of Houston Law Center
Houston, Texas 77004
713-749-1422
713-749-4935
Dr. Sidney Lamb, Chairman
Department of Linguistics and Semiotics
Rice University
Houston, Texas
When: June 24-30, 1985
Where: University of Houston,
Houston, Texas
Goal: To stimulate research between jurists, linguists, and computer
scientists
Format: Tutorials, Research Presentations, and Workshops
(Tentative) Schedule
Tutorials:
June 24 A.M. Legal Language
June 24 P.M. Programming the Law in PROLOG
June 25 A.M. Natural Language Processing
June 25 P.M. Artificial Intelligence and Expert Systems
Original Research Papers:
June 26-June 28
Workshops:
June 28-30 Workshop Topics to be determined by Participants
Possible Sessions and Workshop Topics:
--viewing legal language as the interface between legal concepts and
computer code
--the language of justice and legal logic: Cardozo's methods of sociology
and philosophy
--semantics of legal situations
--viewing legal language as a computerizable process
--structural & cognitive analysis of legal language
--indeterminancy and uncertainty in legal language
--the role of language in reasoning
--linguistic & cognitive networks
--computer-human interactions
--understanding natural legal language
--legal document analysis & linguistic theory
--automatic representation of semantic relationships
--non-Von Neumann architectures
--parsing natural language
--the role of language in human reasoning.
=======================================================
Please contact Charles Walter for further information
------------------------------
End of AIList Digest
********************