Subject: From: AIList Moderator Kenneth Laws <AIList-REQUEST@SRI-AI>

From: [email-masked]
Date: Mon, 13 May 85 03:47:17 edt

Received: from sri-ai.arpa by csnet-relay.arpa id a009646; 12 May 85 18:05 EDT
Date: Sun 12 May 1985 14:15-PDT
Reply-to: AIList@SRI-AI
US-Mail: SRI Int., 333 Ravenswood Ave., Menlo Park, CA  94025
Phone: (415) 859-6467
Subject: AIList Digest   V3 #62
To: AIList@SRI-AI
Received: from rand-relay by vpi; Mon, 13 May 85 03:43 EST

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 <[email-masked]>
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: [email-masked] (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: [email-masked]
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 <[email-masked]>
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" <[email-masked]>
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 <[email-masked]>
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: [email-masked]
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" <[email-masked]>
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
********************